Creates an arbitrary theorem as an axiom (dangerous!)
DESCRIPTION
The function mk_thm can be used to construct an arbitrary theorem. It is
applied to a pair consisting of the desired assumption list (possibly empty)
and conclusion. All the terms therein should be of type bool.
mk_thm([`a1`;...;`an`],`c`) = ({a1,...,an} |- c)
FAILURE CONDITIONS
Fails unless all the terms provided for assumptions and conclusion are of type
bool.
EXAMPLE
The following shows how to create a simple contradiction:
#mk_thm([],`F`);;
|- F
COMMENTS
Although mk_thm can be useful for experimentation or temporarily plugging
gaps, its use should be avoided if at all possible in important proofs, because
it can be used to create theorems leading to contradictions. You can check
whether any axioms have been asserted by mk_thm or new_axiom by the call
axioms().