--- a/src/ZF/Inductive.thy Sun Jul 14 15:11:21 2002 +0200
+++ b/src/ZF/Inductive.thy Sun Jul 14 15:14:43 2002 +0200
@@ -3,9 +3,10 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory.
*)
+header{*Inductive and Coinductive Definitions*}
+
theory Inductive = Fixedpt + mono + QPair
files
"ind_syntax.ML"
@@ -18,11 +19,4 @@
setup IndCases.setup
setup DatatypeTactics.setup
-
-(*belongs to theory ZF*)
-declare bspec [dest?]
-
-(*belongs to theory upair*)
-declare UnI1 [elim?] UnI2 [elim?]
-
end