paulson [Thu, 03 Apr 1997 10:36:54 +0200] rev 2885
Two extra commands shorten the proof time by 800 seconds...
paulson [Thu, 03 Apr 1997 10:33:33 +0200] rev 2884
More List and ListPair utilities
paulson [Thu, 03 Apr 1997 10:32:34 +0200] rev 2883
Now exports declConsts!
Temporarily erased target signature to aid debugging
paulson [Thu, 03 Apr 1997 10:30:23 +0200] rev 2882
Declares overloading for if-and-only-if
paulson [Thu, 03 Apr 1997 10:29:57 +0200] rev 2881
Declares overloading for set-theoretic constants
nipkow [Thu, 03 Apr 1997 09:46:42 +0200] rev 2880
Removed (Unit) in Prod.
Added test for ancestor Nat in datatype.
wenzelm [Wed, 02 Apr 1997 19:12:26 +0200] rev 2879
misc improvements;
wenzelm [Wed, 02 Apr 1997 17:28:27 +0200] rev 2878
changed signature of dummy goal from proto_pure to pure;
paulson [Wed, 02 Apr 1997 15:39:44 +0200] rev 2877
Converted to call blast_tac.
Proves theorems in ZF.thy to make that theory usable again
paulson [Wed, 02 Apr 1997 15:37:35 +0200] rev 2876
Uses ZF.thy again, to make that theory usable