haftmann [Tue, 22 Nov 2005 14:32:01 +0100] rev 18221
added code generator syntax
haftmann [Tue, 22 Nov 2005 12:59:25 +0100] rev 18220
added codegenerator
haftmann [Tue, 22 Nov 2005 12:42:59 +0100] rev 18219
added code generator syntax
paulson [Tue, 22 Nov 2005 10:09:11 +0100] rev 18218
new treatment of polymorphic types, using Sign.const_typargs
haftmann [Mon, 21 Nov 2005 16:51:57 +0100] rev 18217
added codegen package
haftmann [Mon, 21 Nov 2005 15:15:32 +0100] rev 18216
added serializer
paulson [Mon, 21 Nov 2005 11:14:11 +0100] rev 18215
tweak
haftmann [Mon, 21 Nov 2005 10:44:14 +0100] rev 18214
fixed some inconveniencies in website
wenzelm [Sat, 19 Nov 2005 14:22:28 +0100] rev 18213
CONJUNCTS;
wenzelm [Sat, 19 Nov 2005 14:21:09 +0100] rev 18212
tuned;
wenzelm [Sat, 19 Nov 2005 14:21:08 +0100] rev 18211
Goal.norm_hhf_protected;
wenzelm [Sat, 19 Nov 2005 14:21:07 +0100] rev 18210
added coinduct attribute;
tuned;
wenzelm [Sat, 19 Nov 2005 14:21:06 +0100] rev 18209
added CONJUNCTS: treat conjunction as separate sub-goals;
wenzelm [Sat, 19 Nov 2005 14:21:05 +0100] rev 18208
simpset: added reorient field, set_reorient;
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.