mk_fthm : term list * term -> thm
Create arbitrary theorem by adding additional `false' assumption.
The call mk_fthm(asl,c) returns a theorem with conclusion c and assumption
list asl together with the special assumption _FALSITY_, which is defined
to be logically equivalent to F (false). This is the closest approach to
mk_thm that does not involve adding a new axiom and so potentially
- FAILURE CONDITIONS
Fails if any of the given terms does not have Boolean type.
# mk_fthm(,`1 = 2`);;
val it : thm = _FALSITY_ |- 1 = 2
Used for validity-checking of justification functions as a sanity check in
tactic applications: see VALID.
- SEE ALSO
CHEAT_TAC, mk_thm, new_axiom, VALID.