Create arbitrary theorem by adding additional `false' assumption.
DESCRIPTION
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
compromising soundness.
FAILURE CONDITIONS
Fails if any of the given terms does not have Boolean type.
EXAMPLE
# mk_fthm([],`1 = 2`);;
val it : thm = _FALSITY_ |- 1 = 2
USES
Used for validity-checking of justification functions as a sanity check in
tactic applications: see VALID.