same_constTerm.same_const : term -> term -> boolConstant time equality check for constants.
In many cases, one needs to check that a constant is an instance of
the generic constant originally introduced into the signature, or that
two constants are both type instantiations of another. This can be
achieved by taking the constants apart with dest_thy_const
and comparing their name and theory. However, this is relatively
inefficient. Instead, one can invoke same_const, which
takes constant time.
Never fails.
- same_const boolSyntax.universal (rator (concl BOOL_CASES_AX));
> val it = true : bool