urbanc [Fri, 25 Nov 2005 14:51:39 +0100] rev 18246
added fsub.thy (poplmark challenge) to the examples
directory.
berghofe [Fri, 25 Nov 2005 14:00:22 +0100] rev 18245
Fixed problem with strong induction theorem for datatypes containing
no atom types (ind_sort was the empty sort in this case).
kleing [Fri, 25 Nov 2005 11:34:37 +0100] rev 18244
send more information with test-takes-too-long message
(which tests are still running)
wenzelm [Thu, 24 Nov 2005 12:14:56 +0100] rev 18243
fixed spelling of 'case_conclusion';
wenzelm [Thu, 24 Nov 2005 00:00:20 +0100] rev 18242
tuned induct proofs;
wenzelm [Wed, 23 Nov 2005 22:26:13 +0100] rev 18241
tuned induction proofs;
wenzelm [Wed, 23 Nov 2005 22:23:52 +0100] rev 18240
more robust revert_skolem;
tuned;
wenzelm [Wed, 23 Nov 2005 20:29:36 +0100] rev 18239
tuned;
wenzelm [Wed, 23 Nov 2005 18:52:05 +0100] rev 18238
Provers/induct: definitional insts and fixing;
wenzelm [Wed, 23 Nov 2005 18:52:04 +0100] rev 18237
consume: proper treatment of defs;
simplified case_conclusion;
wenzelm [Wed, 23 Nov 2005 18:52:03 +0100] rev 18236
added case_conclusion attribute;
wenzelm [Wed, 23 Nov 2005 18:52:02 +0100] rev 18235
(co)induct: taking;
induct set: proper treatment of defs;
wenzelm [Wed, 23 Nov 2005 18:52:01 +0100] rev 18234
RuleCases.case_conclusion;
wenzelm [Wed, 23 Nov 2005 18:52:00 +0100] rev 18233
tuned;
wenzelm [Wed, 23 Nov 2005 18:51:59 +0100] rev 18232
added case_conclusion attribute;
added coinduct method/attribute;
induct method: definsts/fixing/taking;
tuned;
haftmann [Wed, 23 Nov 2005 17:16:42 +0100] rev 18231
improved failure tracking
wenzelm [Tue, 22 Nov 2005 19:37:36 +0100] rev 18230
Datatype_Universe: hide base names only;
wenzelm [Tue, 22 Nov 2005 19:34:50 +0100] rev 18229
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
added consume rule;
support named case conclusions;
tuned interfaces;
wenzelm [Tue, 22 Nov 2005 19:34:48 +0100] rev 18228
cases_tactic;
wenzelm [Tue, 22 Nov 2005 19:34:47 +0100] rev 18227
moved multi_resolve(s) to drule.ML;
cases_tactic;
wenzelm [Tue, 22 Nov 2005 19:34:46 +0100] rev 18226
find_xxxS: term instead of thm;
wenzelm [Tue, 22 Nov 2005 19:34:44 +0100] rev 18225
export map_tags;
added multi_resolve(s) -- from Isar/method.ML;
wenzelm [Tue, 22 Nov 2005 19:34:43 +0100] rev 18224
make coinduct actually work;
moved some generic code to Pure/Isar/rule_cases.ML;
tuned;
wenzelm [Tue, 22 Nov 2005 19:34:41 +0100] rev 18223
Drule.multi_resolves;
wenzelm [Tue, 22 Nov 2005 19:34:40 +0100] rev 18222
declare coinduct rule;
tuned;
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.
mengj [Fri, 18 Nov 2005 07:07:47 +0100] rev 18197
-- added combinator reduction axioms (typed and untyped) for HOL goals.
-- combined make_nnf functions for HOL and FOL goals.
-- hypothesis of goals are now also skolemized by inference.
mengj [Fri, 18 Nov 2005 07:07:06 +0100] rev 18196
-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
mengj [Fri, 18 Nov 2005 07:06:07 +0100] rev 18195
-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
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;