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
paulson [Wed, 02 Apr 1997 15:36:32 +0200] rev 2875
Mostly converted to blast_tac
paulson [Wed, 02 Apr 1997 15:30:44 +0200] rev 2874
Datatype declarations now require theory Datatype--NOT in quotes
paulson [Wed, 02 Apr 1997 15:29:48 +0200] rev 2873
Converted back from upair.thy to ZF.thy
paulson [Wed, 02 Apr 1997 15:28:42 +0200] rev 2872
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy