| Wed, 02 Apr 1997 19:12:26 +0200 | wenzelm | misc improvements; | changeset | files |
| Wed, 02 Apr 1997 17:28:27 +0200 | wenzelm | changed signature of dummy goal from proto_pure to pure; | changeset | files |
| Wed, 02 Apr 1997 15:39:44 +0200 | paulson | Converted to call blast_tac. | changeset | files |
| Wed, 02 Apr 1997 15:37:35 +0200 | paulson | Uses ZF.thy again, to make that theory usable | changeset | files |
| Wed, 02 Apr 1997 15:36:32 +0200 | paulson | Mostly converted to blast_tac | changeset | files |
| Wed, 02 Apr 1997 15:30:44 +0200 | paulson | Datatype declarations now require theory Datatype--NOT in quotes | changeset | files |
| Wed, 02 Apr 1997 15:29:48 +0200 | paulson | Converted back from upair.thy to ZF.thy | changeset | files |
| Wed, 02 Apr 1997 15:28:42 +0200 | paulson | Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy | changeset | files |