src/ZF/Inductive.thy
changeset 12372 cd3a09c7dac9
parent 12208 5efe7b6874fd
child 13259 01fa0c8dbc92
--- a/src/ZF/Inductive.thy	Wed Dec 05 03:06:05 2001 +0100
+++ b/src/ZF/Inductive.thy	Wed Dec 05 03:07:44 2001 +0100
@@ -18,4 +18,11 @@
 setup IndCases.setup
 setup DatatypeTactics.setup
 
+
+(*belongs to theory ZF*)
+declare bspec [dest?]
+
+(*belongs to theory upair*)
+declare UnI1 [elim?]  UnI2 [elim?]
+
 end