# HG changeset patch
# User clasohm
# Date 753456261 -3600
# Node ID 858ab9a9b04720afbad3c1cbafbea6eda2b28b92
# Parent  0a2f744e008aa18e709bce8486c15b5158e75357
made pseudo theories for all ML files;
documented dependencies between all thy and ML files

diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Arith.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Arithmetic operators and their definitions
 *)
 
-Arith = Epsilon +
+Arith = Epsilon + "simpdata" +
 consts
     rec  :: "[i, i, [i,i]=>i]=>i"
     "#*" :: "[i,i]=>i"      		(infixl 70)
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Bool.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Booleans in Zermelo-Fraenkel Set Theory 
 *)
 
-Bool = ZF +
+Bool = ZF + "simpdata" +
 consts
     "1"		::      "i"     	("1")
     bool        ::      "i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/Datatype.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Datatype.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,4 @@
+(*Dummy theory to document dependencies *)
+
+Datatype = "constructor" + "inductive" + "coinductive" + Univ + QUniv
+               (*this must be capital to avoid conflicts with ML's "datatype" *)
\ No newline at end of file
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Epsilon.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Epsilon induction and recursion
 *)
 
-Epsilon = Nat +
+Epsilon = Nat + "mono" +
 consts
     eclose,rank ::      "i=>i"
     transrec    ::      "[i, [i,i]=>i] =>i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/Fixedpt.thy
--- a/src/ZF/Fixedpt.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Fixedpt.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Least and greatest fixed points
 *)
 
-Fixedpt = ZF +
+Fixedpt = ZF + "domrange" +
 consts
   bnd_mono    :: "[i,i=>i]=>o"
   lfp, gfp    :: "[i,i=>i]=>i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/List.ML
--- a/src/ZF/List.ML	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/List.ML	Tue Nov 16 14:24:21 1993 +0100
@@ -21,6 +21,8 @@
   val type_intrs = datatype_intrs
   val type_elims = datatype_elims);
 
+store_theory "List" List.thy;
+
 val [NilI, ConsI] = List.intrs;
 
 (*An elimination rule, for type-checking*)
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/List.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/List.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+list = Univ + "Datatype" + "intr_elim"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/ListFn.thy
--- a/src/ZF/ListFn.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/ListFn.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -10,7 +10,7 @@
 although complicating its derivation.
 *)
 
-ListFn = List +
+ListFn = List + "constructor" +
 consts
   "@"	     :: "[i,i]=>i"      			(infixr 60)
   list_rec   :: "[i, i, [i,i,i]=>i] => i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Nat.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Natural numbers in Zermelo-Fraenkel Set Theory 
 *)
 
-Nat = Ord + Bool + 
+Nat = Ord + Bool + "mono" +
 consts
     nat 	::      "i"
     nat_case    ::      "[i, i=>i, i]=>i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/Ord.thy
--- a/src/ZF/Ord.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Ord.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Ordinals in Zermelo-Fraenkel Set Theory 
 *)
 
-Ord = WF +
+Ord = WF + "simpdata" + "equalities" +
 consts
   Memrel      	:: "i=>i"
   Transset,Ord  :: "i=>o"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/Pair.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Pair.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+pair = "upair"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Perm.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -9,7 +9,7 @@
   -- Lemmas for the Schroeder-Bernstein Theorem
 *)
 
-Perm = ZF +
+Perm = ZF + "mono" +
 consts
     O    	::      "[i,i]=>i"      (infixr 60)
     id  	::      "i=>i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/QPair.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -11,7 +11,7 @@
 1966.
 *)
 
-QPair = Sum +
+QPair = Sum + "simpdata" +
 consts
   QPair     :: "[i, i] => i"               	("<(_;/ _)>")
   qsplit    :: "[[i,i] => i, i] => i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/QUniv.thy
--- a/src/ZF/QUniv.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/QUniv.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 A small universe for lazy recursive types
 *)
 
-QUniv = Univ + QPair +
+QUniv = Univ + QPair + "mono" + "equalities" +
 consts
     quniv        :: "i=>i"
 
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/ROOT.ML	Tue Nov 16 14:24:21 1993 +0100
@@ -11,8 +11,6 @@
 val banner = "ZF Set Theory (in FOL)";
 writeln banner;
 
-set_loadpath [".", "ex", "../FOL"];
-
 (*For Pure/tactic??  A crude way of adding structure to rules*)
 fun CHECK_SOLVED (Tactic tf) = 
   Tactic (fn state => 
@@ -29,47 +27,9 @@
 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
 
 print_depth 1;
-use_thy "zf";
 
-use     "upair.ML";
-use     "subset.ML";
-use     "pair.ML";
-use     "domrange.ML";
-use     "func.ML";
-use     "equalities.ML";
-use     "simpdata.ML";  
-
-(*further development*)
-use_thy "bool";
-use_thy "sum";
-use_thy "qpair";
-use     "mono.ML";
-use_thy "fixedpt";
-
-(*Inductive/coinductive definitions*)
-use     "ind_syntax.ML";
-use     "intr_elim.ML";
-use     "indrule.ML";
-use     "inductive.ML";
-use     "coinductive.ML";
-
-use_thy "perm";
-use_thy "trancl";
-use_thy "wf";
-use_thy "ord";
-use_thy "nat";
-use_thy "epsilon";
-use_thy "arith";
-
-(*Datatype/codatatype definitions*)
-use_thy "univ";
-use_thy "quniv";
-use     "constructor.ML";
-use     "datatype.ML";
-
-use     "fin.ML";
-use_thy "List";
-use_thy "listfn";
+use_thy "fin";
+use_thy "ListFn";
 
 (*printing functions are inherited from FOL*)
 print_depth 8;
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Sum.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -7,7 +7,7 @@
 "Part" primitive for simultaneous recursive type definitions
 *)
 
-Sum = Bool +
+Sum = Bool + "simpdata" +
 consts
     "+"    	:: "[i,i]=>i"      		(infixr 65)
     Inl,Inr     :: "i=>i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Trancl.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Transitive closure of a relation
 *)
 
-Trancl = Fixedpt + Perm + 
+Trancl = Fixedpt + Perm + "mono" +
 consts
     "rtrancl"	:: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
     "trancl"    :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Univ.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -8,7 +8,7 @@
 Standard notation for Vset(i) is V(i), but users might want V for a variable
 *)
 
-Univ = Arith + Sum +
+Univ = Arith + Sum + "mono" +
 consts
     Limit       ::      "i=>o"
     Vfrom       ::      "[i,i]=>i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/WF.thy
--- a/src/ZF/WF.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/WF.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Well-founded Recursion
 *)
 
-WF = Trancl +
+WF = Trancl + "mono" +
 consts
     wf		 ::      "i=>o"
     wftrec,wfrec ::      "[i, i, [i,i]=>i] =>i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/arith.thy
--- a/src/ZF/arith.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/arith.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Arithmetic operators and their definitions
 *)
 
-Arith = Epsilon +
+Arith = Epsilon + "simpdata" +
 consts
     rec  :: "[i, i, [i,i]=>i]=>i"
     "#*" :: "[i,i]=>i"      		(infixl 70)
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/bool.thy
--- a/src/ZF/bool.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/bool.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Booleans in Zermelo-Fraenkel Set Theory 
 *)
 
-Bool = ZF +
+Bool = ZF + "simpdata" +
 consts
     "1"		::      "i"     	("1")
     bool        ::      "i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/coinductive.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/coinductive.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+coinductive = "ind_syntax" + "intr_elim"
\ No newline at end of file
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/constructor.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/constructor.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+constructor = "ind_syntax"
\ No newline at end of file
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/datatype.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/datatype.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,4 @@
+(*Dummy theory to document dependencies *)
+
+Datatype = "constructor" + "inductive" + "coinductive" + Univ + QUniv
+               (*this must be capital to avoid conflicts with ML's "datatype" *)
\ No newline at end of file
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/domrange.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/domrange.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+domrange = "pair" + "subset"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/epsilon.thy
--- a/src/ZF/epsilon.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/epsilon.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Epsilon induction and recursion
 *)
 
-Epsilon = Nat +
+Epsilon = Nat + "mono" +
 consts
     eclose,rank ::      "i=>i"
     transrec    ::      "[i, [i,i]=>i] =>i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/equalities.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/equalities.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+equalities = "domrange"
\ No newline at end of file
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/fin.ML
--- a/src/ZF/fin.ML	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/fin.ML	Tue Nov 16 14:24:21 1993 +0100
@@ -28,6 +28,8 @@
   val type_intrs = [empty_subsetI, cons_subsetI, PowI]
   val type_elims = [make_elim PowD]);
 
+store_theory "Fin" Fin.thy;
+
 val [Fin_0I, Fin_consI] = Fin.intrs;
 
 
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/fin.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/fin.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/fixedpt.thy
--- a/src/ZF/fixedpt.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/fixedpt.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Least and greatest fixed points
 *)
 
-Fixedpt = ZF +
+Fixedpt = ZF + "domrange" +
 consts
   bnd_mono    :: "[i,i=>i]=>o"
   lfp, gfp    :: "[i,i=>i]=>i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/func.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/func.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+func = "domrange"
\ No newline at end of file
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/ind_syntax.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ind_syntax.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+ind_syntax = "mono"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/indrule.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/indrule.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+indrule = "ind_syntax" + "intr_elim"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/inductive.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/inductive.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+inductive = "indrule"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/intr_elim.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/intr_elim.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+intr_elim = Fixedpt + "ind_syntax"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/list.ML
--- a/src/ZF/list.ML	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/list.ML	Tue Nov 16 14:24:21 1993 +0100
@@ -21,6 +21,8 @@
   val type_intrs = datatype_intrs
   val type_elims = datatype_elims);
 
+store_theory "List" List.thy;
+
 val [NilI, ConsI] = List.intrs;
 
 (*An elimination rule, for type-checking*)
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/list.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/list.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+list = Univ + "Datatype" + "intr_elim"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/listfn.thy
--- a/src/ZF/listfn.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/listfn.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -10,7 +10,7 @@
 although complicating its derivation.
 *)
 
-ListFn = List +
+ListFn = List + "constructor" +
 consts
   "@"	     :: "[i,i]=>i"      			(infixr 60)
   list_rec   :: "[i, i, [i,i,i]=>i] => i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/mono.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/mono.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+mono = QPair + Sum
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/nat.thy
--- a/src/ZF/nat.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/nat.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Natural numbers in Zermelo-Fraenkel Set Theory 
 *)
 
-Nat = Ord + Bool + 
+Nat = Ord + Bool + "mono" +
 consts
     nat 	::      "i"
     nat_case    ::      "[i, i=>i, i]=>i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/ord.thy
--- a/src/ZF/ord.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/ord.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Ordinals in Zermelo-Fraenkel Set Theory 
 *)
 
-Ord = WF +
+Ord = WF + "simpdata" + "equalities" +
 consts
   Memrel      	:: "i=>i"
   Transset,Ord  :: "i=>o"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/pair.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/pair.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+pair = "upair"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/perm.thy
--- a/src/ZF/perm.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/perm.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -9,7 +9,7 @@
   -- Lemmas for the Schroeder-Bernstein Theorem
 *)
 
-Perm = ZF +
+Perm = ZF + "mono" +
 consts
     O    	::      "[i,i]=>i"      (infixr 60)
     id  	::      "i=>i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/qpair.thy
--- a/src/ZF/qpair.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/qpair.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -11,7 +11,7 @@
 1966.
 *)
 
-QPair = Sum +
+QPair = Sum + "simpdata" +
 consts
   QPair     :: "[i, i] => i"               	("<(_;/ _)>")
   qsplit    :: "[[i,i] => i, i] => i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/quniv.thy
--- a/src/ZF/quniv.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/quniv.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 A small universe for lazy recursive types
 *)
 
-QUniv = Univ + QPair +
+QUniv = Univ + QPair + "mono" + "equalities" +
 consts
     quniv        :: "i=>i"
 
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/simpdata.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/simpdata.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+simpdata = "func"
\ No newline at end of file
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/subset.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/subset.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+subset = "upair"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/sum.thy
--- a/src/ZF/sum.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/sum.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -7,7 +7,7 @@
 "Part" primitive for simultaneous recursive type definitions
 *)
 
-Sum = Bool +
+Sum = Bool + "simpdata" +
 consts
     "+"    	:: "[i,i]=>i"      		(infixr 65)
     Inl,Inr     :: "i=>i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/trancl.thy
--- a/src/ZF/trancl.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/trancl.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Transitive closure of a relation
 *)
 
-Trancl = Fixedpt + Perm + 
+Trancl = Fixedpt + Perm + "mono" +
 consts
     "rtrancl"	:: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
     "trancl"    :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/univ.thy
--- a/src/ZF/univ.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/univ.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -8,7 +8,7 @@
 Standard notation for Vset(i) is V(i), but users might want V for a variable
 *)
 
-Univ = Arith + Sum +
+Univ = Arith + Sum + "mono" +
 consts
     Limit       ::      "i=>o"
     Vfrom       ::      "[i,i]=>i"
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/upair.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/upair.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+upair = ZF
diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/wf.thy
--- a/src/ZF/wf.thy	Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/wf.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
 Well-founded Recursion
 *)
 
-WF = Trancl +
+WF = Trancl + "mono" +
 consts
     wf		 ::      "i=>o"
     wftrec,wfrec ::      "[i, i, [i,i]=>i] =>i"