mengj [Fri, 18 Nov 2005 07:05:11 +0100] rev 18194
-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
-- added "check_is_fol_term", which is the same as "check_is_fol", but takes a "term" as input.
-- added "check_is_fol" and "check_is_fol_term" into the signature.
wenzelm [Wed, 16 Nov 2005 19:34:19 +0100] rev 18193
tuned document;
wenzelm [Wed, 16 Nov 2005 17:50:35 +0100] rev 18192
tuned;
wenzelm [Wed, 16 Nov 2005 17:49:16 +0100] rev 18191
improved induction proof: local defs/fixes;
wenzelm [Wed, 16 Nov 2005 17:45:36 +0100] rev 18190
tuned Pattern.match/unify;
tuned fold;
wenzelm [Wed, 16 Nov 2005 17:45:35 +0100] rev 18189
added deskolem;
wenzelm [Wed, 16 Nov 2005 17:45:34 +0100] rev 18188
added THEN_ALL_NEW_CASES;
Syntax.deskolem;
wenzelm [Wed, 16 Nov 2005 17:45:33 +0100] rev 18187
added revert_skolem, mk_def, add_def;
export: Goal.norm_hhf';
tuned;
wenzelm [Wed, 16 Nov 2005 17:45:32 +0100] rev 18186
ProofContext.mk_def;
wenzelm [Wed, 16 Nov 2005 17:45:31 +0100] rev 18185
Term.betapplys;