paulson [Tue, 31 May 2005 17:52:10 +0200] rev 16157
minor tidying and sml/nj compatibility
quigley [Tue, 31 May 2005 12:42:36 +0200] rev 16156
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
ruleset.
nipkow [Tue, 31 May 2005 12:36:01 +0200] rev 16155
fixed sectioning
nipkow [Tue, 31 May 2005 12:16:42 +0200] rev 16154
\nexists
nipkow [Tue, 31 May 2005 12:16:24 +0200] rev 16153
\nexists und premsise1 .. 9
wenzelm [Tue, 31 May 2005 11:53:43 +0200] rev 16152
no_tac;
wenzelm [Tue, 31 May 2005 11:53:42 +0200] rev 16151
ML Pure: name spaces have been refined;
ML Pure: cases produced by proof methods specify options, NONE means to removee bindings;
wenzelm [Tue, 31 May 2005 11:53:41 +0200] rev 16150
moved is_ident to General/symbol.ML;
wenzelm [Tue, 31 May 2005 11:53:40 +0200] rev 16149
Theory.restore_naming;
tuned fold;
wenzelm [Tue, 31 May 2005 11:53:39 +0200] rev 16148
make: T option -- actually remove undefined cases;
Logic.nth_prem;
tuned;