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