mengj [Fri, 10 Mar 2006 04:02:53 +0100] rev 19229
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
huffman [Fri, 10 Mar 2006 00:53:28 +0100] rev 19228
added many simple lemmas
mengj [Thu, 09 Mar 2006 06:05:01 +0100] rev 19227
Added more functions to the signature and tidied up some functions.
wenzelm [Wed, 08 Mar 2006 21:40:46 +0100] rev 19226
tuned;
urbanc [Wed, 08 Mar 2006 18:52:43 +0100] rev 19225
tuned some proofs
wenzelm [Wed, 08 Mar 2006 18:37:31 +0100] rev 19224
select_goals: split original conjunctions;
wenzelm [Wed, 08 Mar 2006 18:37:30 +0100] rev 19223
method: goal restriction defaults to [1];
wenzelm [Wed, 08 Mar 2006 18:37:28 +0100] rev 19222
infer_derivs: avoid allocating empty MinProof;
wenzelm [Wed, 08 Mar 2006 18:37:27 +0100] rev 19221
tuned;
wenzelm [Wed, 08 Mar 2006 18:37:25 +0100] rev 19220
Isar/method: goal restriction;
wenzelm [Wed, 08 Mar 2006 18:37:24 +0100] rev 19219
constdecl: always allow 'where';
urbanc [Wed, 08 Mar 2006 18:00:00 +0100] rev 19218
deleted some proofs "on comment"
urbanc [Wed, 08 Mar 2006 17:55:51 +0100] rev 19217
tuned some proofs
urbanc [Wed, 08 Mar 2006 17:54:55 +0100] rev 19216
tuned some of the proofs about fresh_fun
haftmann [Wed, 08 Mar 2006 17:23:46 +0100] rev 19215
first running version of type classes
haftmann [Wed, 08 Mar 2006 17:03:19 +0100] rev 19214
first running version of type classes
haftmann [Wed, 08 Mar 2006 16:29:07 +0100] rev 19213
first running version of type classes
paulson [Wed, 08 Mar 2006 10:19:57 +0100] rev 19212
Frequency strategy. Revised indentation, etc.
nipkow [Wed, 08 Mar 2006 10:06:31 +0100] rev 19211
*** empty log message ***
obua [Tue, 07 Mar 2006 18:02:11 +0100] rev 19210
added ROOT.ML
paulson [Tue, 07 Mar 2006 16:50:33 +0100] rev 19209
Indentation
paulson [Tue, 07 Mar 2006 16:49:48 +0100] rev 19208
Tidying and restructuring.
paulson [Tue, 07 Mar 2006 16:49:12 +0100] rev 19207
Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.
paulson [Tue, 07 Mar 2006 16:47:51 +0100] rev 19206
Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before.
Removal of the unused err_list.
paulson [Tue, 07 Mar 2006 16:46:54 +0100] rev 19205
Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson [Tue, 07 Mar 2006 16:45:04 +0100] rev 19204
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
obua [Tue, 07 Mar 2006 16:03:31 +0100] rev 19203
Added HOL-ZF to Isabelle.
haftmann [Tue, 07 Mar 2006 14:09:48 +0100] rev 19202
substantial improvement in codegen iml
mengj [Tue, 07 Mar 2006 04:06:02 +0100] rev 19201
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
The hash table (for removing duplicate) now stores clauses as Term.term with names.
mengj [Tue, 07 Mar 2006 04:04:21 +0100] rev 19200
relevance_filter takes input axioms as Term.term.