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
urbanc [Wed, 01 Mar 2006 18:24:31 +0100] rev 19168
streamlined the proof
haftmann [Wed, 01 Mar 2006 13:47:42 +0100] rev 19167
refined representation of codegen intermediate language
urbanc [Wed, 01 Mar 2006 10:37:00 +0100] rev 19166
some small tunings
urbanc [Wed, 01 Mar 2006 10:28:39 +0100] rev 19165
added fresh_fun_eqvt theorem to the theorem collection
urbanc [Wed, 01 Mar 2006 10:27:48 +0100] rev 19164
added initialisation-code for finite_guess
urbanc [Wed, 01 Mar 2006 10:27:01 +0100] rev 19163
made some small tunings in the decision-procedure
(in the order how the "small" tactics are called)
mengj [Wed, 01 Mar 2006 06:08:12 +0100] rev 19162
Added setup for "atpset" (a rule set for ATPs).
mengj [Wed, 01 Mar 2006 06:06:16 +0100] rev 19161
Added file Tools/res_atpset.ML.
mengj [Wed, 01 Mar 2006 06:05:25 +0100] rev 19160
Merged HOL and FOL clauses and combined some functions.