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.
mengj [Tue, 07 Mar 2006 04:01:25 +0100] rev 19199
Proof reconstruction now only takes names of theorems as input.
mengj [Tue, 07 Mar 2006 03:59:48 +0100] rev 19198
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj [Tue, 07 Mar 2006 03:58:50 +0100] rev 19197
tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
mengj [Tue, 07 Mar 2006 03:56:59 +0100] rev 19196
Added functions to retrieve local and global atpset rules.
cnf thms to Term.term format.
mengj [Tue, 07 Mar 2006 03:54:11 +0100] rev 19195
Moved the settings for ATP time limit to res_atp.ML
mengj [Tue, 07 Mar 2006 03:51:40 +0100] rev 19194
Merged res_atp_setup.ML into res_atp.ML.
HOL translation is integrated with background Isabelle-ATP linkup.
Both ATP methods and background linkup retrieve lemmas stored in claset, simpset and atpset.
mengj [Tue, 07 Mar 2006 03:49:26 +0100] rev 19193
When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
mengj [Tue, 07 Mar 2006 03:48:02 +0100] rev 19192
Merged res_atp_setup.ML into res_atp.ML.
wenzelm [Sun, 05 Mar 2006 23:56:57 +0100] rev 19191
SELECT_GOAL: fixed trivial case;
webertj [Sun, 05 Mar 2006 18:49:13 +0100] rev 19190
fixed a typo in a comment
wenzelm [Sat, 04 Mar 2006 21:39:08 +0100] rev 19189
tuned;
wenzelm [Sat, 04 Mar 2006 21:10:12 +0100] rev 19188
method: SelectGoals;
wenzelm [Sat, 04 Mar 2006 21:10:11 +0100] rev 19187
method: syntax for SelectGoals;
wenzelm [Sat, 04 Mar 2006 21:10:10 +0100] rev 19186
text: added SelectGoals;
wenzelm [Sat, 04 Mar 2006 21:10:09 +0100] rev 19185
tuned conj_curry;
wenzelm [Sat, 04 Mar 2006 21:10:08 +0100] rev 19184
added extract, retrofit;
wenzelm [Sat, 04 Mar 2006 21:10:07 +0100] rev 19183
added mk_conjunction;
tuned conj_curry;
wenzelm [Sat, 04 Mar 2006 21:10:06 +0100] rev 19182
method: restriction to first n sub-goals;
nipkow [Fri, 03 Mar 2006 19:43:46 +0100] rev 19181
minor changes
nipkow [Fri, 03 Mar 2006 19:30:30 +0100] rev 19180
more examples
nipkow [Fri, 03 Mar 2006 19:30:20 +0100] rev 19179
changed and retracted change of location of code lemmas.
nipkow [Fri, 03 Mar 2006 16:25:30 +0100] rev 19178
ignore repeated vars on lhs, cleanup
haftmann [Fri, 03 Mar 2006 08:52:39 +0100] rev 19177
improvements for nbe
paulson [Thu, 02 Mar 2006 18:51:11 +0100] rev 19176
reformatting
paulson [Thu, 02 Mar 2006 18:50:43 +0100] rev 19175
subset_refl now included using the atp attribute
paulson [Thu, 02 Mar 2006 18:49:13 +0100] rev 19174
moved the "use" directive
urbanc [Thu, 02 Mar 2006 16:01:06 +0100] rev 19173
fixed the bugs itroduced by the previous commit
urbanc [Thu, 02 Mar 2006 15:43:22 +0100] rev 19172
made some small changes to generate nicer latex-output
urbanc [Thu, 02 Mar 2006 15:05:09 +0100] rev 19171
split the files
- Iteration.thy contains the big proof of the iteration combinator
- Recursion.thy derives from Iteration the recursion combinator
- lam_substs.thy contains the examples (size, substitution and parallel substitution)
mengj [Thu, 02 Mar 2006 00:57:34 +0100] rev 19170
Added in a signature.
urbanc [Wed, 01 Mar 2006 18:26:20 +0100] rev 19169
fixed a problem where a permutation is not analysed
when the term is of the form
(pi o f) x1...xn
This was the case because the head of this term is the
constant "nominal.perm". Now an applicability predicate
decides the right behaviour of the simproc