wenzelm [Sat, 19 Nov 2005 14:21:04 +0100] rev 18207
tuned norm_hhf_protected;
wenzelm [Sat, 19 Nov 2005 14:21:03 +0100] rev 18206
removed conj_mono;
added conj_curry;
tuned;
wenzelm [Sat, 19 Nov 2005 14:21:02 +0100] rev 18205
induct: CONJUNCTS for multiple goals;
added coinduct method;
tuned;
wenzelm [Sat, 19 Nov 2005 14:21:01 +0100] rev 18204
tuned induct syntax;
wenzelm [Sat, 19 Nov 2005 14:21:00 +0100] rev 18203
FOL: -p 2;
chaieb [Fri, 18 Nov 2005 07:13:58 +0100] rev 18202
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
mengj [Fri, 18 Nov 2005 07:10:37 +0100] rev 18201
-- changed the interface of functions vampire_oracle and eprover_oracle.
mengj [Fri, 18 Nov 2005 07:10:00 +0100] rev 18200
-- terms are fully typed.
-- only the top-level boolean terms are predicates.
mengj [Fri, 18 Nov 2005 07:08:54 +0100] rev 18199
-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
mengj [Fri, 18 Nov 2005 07:08:18 +0100] rev 18198
-- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.