Thu, 03 Apr 1997 09:46:42 +0200 Removed (Unit) in Prod.
nipkow [Thu, 03 Apr 1997 09:46:42 +0200] rev 2880
Removed (Unit) in Prod. Added test for ancestor Nat in datatype.
Wed, 02 Apr 1997 19:12:26 +0200 misc improvements;
wenzelm [Wed, 02 Apr 1997 19:12:26 +0200] rev 2879
misc improvements;
Wed, 02 Apr 1997 17:28:27 +0200 changed signature of dummy goal from proto_pure to pure;
wenzelm [Wed, 02 Apr 1997 17:28:27 +0200] rev 2878
changed signature of dummy goal from proto_pure to pure;
Wed, 02 Apr 1997 15:39:44 +0200 Converted to call blast_tac.
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
Wed, 02 Apr 1997 15:37:35 +0200 Uses ZF.thy again, to make that theory usable
paulson [Wed, 02 Apr 1997 15:37:35 +0200] rev 2876
Uses ZF.thy again, to make that theory usable
Wed, 02 Apr 1997 15:36:32 +0200 Mostly converted to blast_tac
paulson [Wed, 02 Apr 1997 15:36:32 +0200] rev 2875
Mostly converted to blast_tac
Wed, 02 Apr 1997 15:30:44 +0200 Datatype declarations now require theory Datatype--NOT in quotes
paulson [Wed, 02 Apr 1997 15:30:44 +0200] rev 2874
Datatype declarations now require theory Datatype--NOT in quotes
Wed, 02 Apr 1997 15:29:48 +0200 Converted back from upair.thy to ZF.thy
paulson [Wed, 02 Apr 1997 15:29:48 +0200] rev 2873
Converted back from upair.thy to ZF.thy
Wed, 02 Apr 1997 15:28:42 +0200 Moved definitions (binary intersection, etc.) from upair.thy back 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
Wed, 02 Apr 1997 15:26:52 +0200 Now checks for existence of theory Inductive (Fixedpt was too small)
paulson [Wed, 02 Apr 1997 15:26:52 +0200] rev 2871
Now checks for existence of theory Inductive (Fixedpt was too small)
(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip