made pseudo theories for all ML files;
authorclasohm
Tue Nov 16 14:24:21 1993 +0100 (1993-11-16 ago)
changeset 124858ab9a9b047
parent 123 0a2f744e008a
child 125 bba27d15d76e
made pseudo theories for all ML files;
documented dependencies between all thy and ML files
src/ZF/Arith.thy
src/ZF/Bool.thy
src/ZF/Datatype.thy
src/ZF/Epsilon.thy
src/ZF/Fixedpt.thy
src/ZF/List.ML
src/ZF/List.thy
src/ZF/ListFn.thy
src/ZF/Nat.thy
src/ZF/Ord.thy
src/ZF/Pair.thy
src/ZF/Perm.thy
src/ZF/QPair.thy
src/ZF/QUniv.thy
src/ZF/ROOT.ML
src/ZF/Sum.thy
src/ZF/Trancl.thy
src/ZF/Univ.thy
src/ZF/WF.thy
src/ZF/arith.thy
src/ZF/bool.thy
src/ZF/coinductive.thy
src/ZF/constructor.thy
src/ZF/datatype.thy
src/ZF/domrange.thy
src/ZF/epsilon.thy
src/ZF/equalities.thy
src/ZF/fin.ML
src/ZF/fin.thy
src/ZF/fixedpt.thy
src/ZF/func.thy
src/ZF/ind_syntax.thy
src/ZF/indrule.thy
src/ZF/inductive.thy
src/ZF/intr_elim.thy
src/ZF/list.ML
src/ZF/list.thy
src/ZF/listfn.thy
src/ZF/mono.thy
src/ZF/nat.thy
src/ZF/ord.thy
src/ZF/pair.thy
src/ZF/perm.thy
src/ZF/qpair.thy
src/ZF/quniv.thy
src/ZF/simpdata.thy
src/ZF/subset.thy
src/ZF/sum.thy
src/ZF/trancl.thy
src/ZF/univ.thy
src/ZF/upair.thy
src/ZF/wf.thy
     1.1 --- a/src/ZF/Arith.thy	Tue Nov 16 14:23:19 1993 +0100
     1.2 +++ b/src/ZF/Arith.thy	Tue Nov 16 14:24:21 1993 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Arithmetic operators and their definitions
     1.5  *)
     1.6  
     1.7 -Arith = Epsilon +
     1.8 +Arith = Epsilon + "simpdata" +
     1.9  consts
    1.10      rec  :: "[i, i, [i,i]=>i]=>i"
    1.11      "#*" :: "[i,i]=>i"      		(infixl 70)
     2.1 --- a/src/ZF/Bool.thy	Tue Nov 16 14:23:19 1993 +0100
     2.2 +++ b/src/ZF/Bool.thy	Tue Nov 16 14:24:21 1993 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  Booleans in Zermelo-Fraenkel Set Theory 
     2.5  *)
     2.6  
     2.7 -Bool = ZF +
     2.8 +Bool = ZF + "simpdata" +
     2.9  consts
    2.10      "1"		::      "i"     	("1")
    2.11      bool        ::      "i"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/Datatype.thy	Tue Nov 16 14:24:21 1993 +0100
     3.3 @@ -0,0 +1,4 @@
     3.4 +(*Dummy theory to document dependencies *)
     3.5 +
     3.6 +Datatype = "constructor" + "inductive" + "coinductive" + Univ + QUniv
     3.7 +               (*this must be capital to avoid conflicts with ML's "datatype" *)
     3.8 \ No newline at end of file
     4.1 --- a/src/ZF/Epsilon.thy	Tue Nov 16 14:23:19 1993 +0100
     4.2 +++ b/src/ZF/Epsilon.thy	Tue Nov 16 14:24:21 1993 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  Epsilon induction and recursion
     4.5  *)
     4.6  
     4.7 -Epsilon = Nat +
     4.8 +Epsilon = Nat + "mono" +
     4.9  consts
    4.10      eclose,rank ::      "i=>i"
    4.11      transrec    ::      "[i, [i,i]=>i] =>i"
     5.1 --- a/src/ZF/Fixedpt.thy	Tue Nov 16 14:23:19 1993 +0100
     5.2 +++ b/src/ZF/Fixedpt.thy	Tue Nov 16 14:24:21 1993 +0100
     5.3 @@ -6,7 +6,7 @@
     5.4  Least and greatest fixed points
     5.5  *)
     5.6  
     5.7 -Fixedpt = ZF +
     5.8 +Fixedpt = ZF + "domrange" +
     5.9  consts
    5.10    bnd_mono    :: "[i,i=>i]=>o"
    5.11    lfp, gfp    :: "[i,i=>i]=>i"
     6.1 --- a/src/ZF/List.ML	Tue Nov 16 14:23:19 1993 +0100
     6.2 +++ b/src/ZF/List.ML	Tue Nov 16 14:24:21 1993 +0100
     6.3 @@ -21,6 +21,8 @@
     6.4    val type_intrs = datatype_intrs
     6.5    val type_elims = datatype_elims);
     6.6  
     6.7 +store_theory "List" List.thy;
     6.8 +
     6.9  val [NilI, ConsI] = List.intrs;
    6.10  
    6.11  (*An elimination rule, for type-checking*)
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/ZF/List.thy	Tue Nov 16 14:24:21 1993 +0100
     7.3 @@ -0,0 +1,3 @@
     7.4 +(*Dummy theory to document dependencies *)
     7.5 +
     7.6 +list = Univ + "Datatype" + "intr_elim"
     8.1 --- a/src/ZF/ListFn.thy	Tue Nov 16 14:23:19 1993 +0100
     8.2 +++ b/src/ZF/ListFn.thy	Tue Nov 16 14:24:21 1993 +0100
     8.3 @@ -10,7 +10,7 @@
     8.4  although complicating its derivation.
     8.5  *)
     8.6  
     8.7 -ListFn = List +
     8.8 +ListFn = List + "constructor" +
     8.9  consts
    8.10    "@"	     :: "[i,i]=>i"      			(infixr 60)
    8.11    list_rec   :: "[i, i, [i,i,i]=>i] => i"
     9.1 --- a/src/ZF/Nat.thy	Tue Nov 16 14:23:19 1993 +0100
     9.2 +++ b/src/ZF/Nat.thy	Tue Nov 16 14:24:21 1993 +0100
     9.3 @@ -6,7 +6,7 @@
     9.4  Natural numbers in Zermelo-Fraenkel Set Theory 
     9.5  *)
     9.6  
     9.7 -Nat = Ord + Bool + 
     9.8 +Nat = Ord + Bool + "mono" +
     9.9  consts
    9.10      nat 	::      "i"
    9.11      nat_case    ::      "[i, i=>i, i]=>i"
    10.1 --- a/src/ZF/Ord.thy	Tue Nov 16 14:23:19 1993 +0100
    10.2 +++ b/src/ZF/Ord.thy	Tue Nov 16 14:24:21 1993 +0100
    10.3 @@ -6,7 +6,7 @@
    10.4  Ordinals in Zermelo-Fraenkel Set Theory 
    10.5  *)
    10.6  
    10.7 -Ord = WF +
    10.8 +Ord = WF + "simpdata" + "equalities" +
    10.9  consts
   10.10    Memrel      	:: "i=>i"
   10.11    Transset,Ord  :: "i=>o"
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/ZF/Pair.thy	Tue Nov 16 14:24:21 1993 +0100
    11.3 @@ -0,0 +1,3 @@
    11.4 +(*Dummy theory to document dependencies *)
    11.5 +
    11.6 +pair = "upair"
    12.1 --- a/src/ZF/Perm.thy	Tue Nov 16 14:23:19 1993 +0100
    12.2 +++ b/src/ZF/Perm.thy	Tue Nov 16 14:24:21 1993 +0100
    12.3 @@ -9,7 +9,7 @@
    12.4    -- Lemmas for the Schroeder-Bernstein Theorem
    12.5  *)
    12.6  
    12.7 -Perm = ZF +
    12.8 +Perm = ZF + "mono" +
    12.9  consts
   12.10      O    	::      "[i,i]=>i"      (infixr 60)
   12.11      id  	::      "i=>i"
    13.1 --- a/src/ZF/QPair.thy	Tue Nov 16 14:23:19 1993 +0100
    13.2 +++ b/src/ZF/QPair.thy	Tue Nov 16 14:24:21 1993 +0100
    13.3 @@ -11,7 +11,7 @@
    13.4  1966.
    13.5  *)
    13.6  
    13.7 -QPair = Sum +
    13.8 +QPair = Sum + "simpdata" +
    13.9  consts
   13.10    QPair     :: "[i, i] => i"               	("<(_;/ _)>")
   13.11    qsplit    :: "[[i,i] => i, i] => i"
    14.1 --- a/src/ZF/QUniv.thy	Tue Nov 16 14:23:19 1993 +0100
    14.2 +++ b/src/ZF/QUniv.thy	Tue Nov 16 14:24:21 1993 +0100
    14.3 @@ -6,7 +6,7 @@
    14.4  A small universe for lazy recursive types
    14.5  *)
    14.6  
    14.7 -QUniv = Univ + QPair +
    14.8 +QUniv = Univ + QPair + "mono" + "equalities" +
    14.9  consts
   14.10      quniv        :: "i=>i"
   14.11  
    15.1 --- a/src/ZF/ROOT.ML	Tue Nov 16 14:23:19 1993 +0100
    15.2 +++ b/src/ZF/ROOT.ML	Tue Nov 16 14:24:21 1993 +0100
    15.3 @@ -11,8 +11,6 @@
    15.4  val banner = "ZF Set Theory (in FOL)";
    15.5  writeln banner;
    15.6  
    15.7 -set_loadpath [".", "ex", "../FOL"];
    15.8 -
    15.9  (*For Pure/tactic??  A crude way of adding structure to rules*)
   15.10  fun CHECK_SOLVED (Tactic tf) = 
   15.11    Tactic (fn state => 
   15.12 @@ -29,47 +27,9 @@
   15.13  fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
   15.14  
   15.15  print_depth 1;
   15.16 -use_thy "zf";
   15.17  
   15.18 -use     "upair.ML";
   15.19 -use     "subset.ML";
   15.20 -use     "pair.ML";
   15.21 -use     "domrange.ML";
   15.22 -use     "func.ML";
   15.23 -use     "equalities.ML";
   15.24 -use     "simpdata.ML";  
   15.25 -
   15.26 -(*further development*)
   15.27 -use_thy "bool";
   15.28 -use_thy "sum";
   15.29 -use_thy "qpair";
   15.30 -use     "mono.ML";
   15.31 -use_thy "fixedpt";
   15.32 -
   15.33 -(*Inductive/coinductive definitions*)
   15.34 -use     "ind_syntax.ML";
   15.35 -use     "intr_elim.ML";
   15.36 -use     "indrule.ML";
   15.37 -use     "inductive.ML";
   15.38 -use     "coinductive.ML";
   15.39 -
   15.40 -use_thy "perm";
   15.41 -use_thy "trancl";
   15.42 -use_thy "wf";
   15.43 -use_thy "ord";
   15.44 -use_thy "nat";
   15.45 -use_thy "epsilon";
   15.46 -use_thy "arith";
   15.47 -
   15.48 -(*Datatype/codatatype definitions*)
   15.49 -use_thy "univ";
   15.50 -use_thy "quniv";
   15.51 -use     "constructor.ML";
   15.52 -use     "datatype.ML";
   15.53 -
   15.54 -use     "fin.ML";
   15.55 -use_thy "List";
   15.56 -use_thy "listfn";
   15.57 +use_thy "fin";
   15.58 +use_thy "ListFn";
   15.59  
   15.60  (*printing functions are inherited from FOL*)
   15.61  print_depth 8;
    16.1 --- a/src/ZF/Sum.thy	Tue Nov 16 14:23:19 1993 +0100
    16.2 +++ b/src/ZF/Sum.thy	Tue Nov 16 14:24:21 1993 +0100
    16.3 @@ -7,7 +7,7 @@
    16.4  "Part" primitive for simultaneous recursive type definitions
    16.5  *)
    16.6  
    16.7 -Sum = Bool +
    16.8 +Sum = Bool + "simpdata" +
    16.9  consts
   16.10      "+"    	:: "[i,i]=>i"      		(infixr 65)
   16.11      Inl,Inr     :: "i=>i"
    17.1 --- a/src/ZF/Trancl.thy	Tue Nov 16 14:23:19 1993 +0100
    17.2 +++ b/src/ZF/Trancl.thy	Tue Nov 16 14:24:21 1993 +0100
    17.3 @@ -6,7 +6,7 @@
    17.4  Transitive closure of a relation
    17.5  *)
    17.6  
    17.7 -Trancl = Fixedpt + Perm + 
    17.8 +Trancl = Fixedpt + Perm + "mono" +
    17.9  consts
   17.10      "rtrancl"	:: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
   17.11      "trancl"    :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
    18.1 --- a/src/ZF/Univ.thy	Tue Nov 16 14:23:19 1993 +0100
    18.2 +++ b/src/ZF/Univ.thy	Tue Nov 16 14:24:21 1993 +0100
    18.3 @@ -8,7 +8,7 @@
    18.4  Standard notation for Vset(i) is V(i), but users might want V for a variable
    18.5  *)
    18.6  
    18.7 -Univ = Arith + Sum +
    18.8 +Univ = Arith + Sum + "mono" +
    18.9  consts
   18.10      Limit       ::      "i=>o"
   18.11      Vfrom       ::      "[i,i]=>i"
    19.1 --- a/src/ZF/WF.thy	Tue Nov 16 14:23:19 1993 +0100
    19.2 +++ b/src/ZF/WF.thy	Tue Nov 16 14:24:21 1993 +0100
    19.3 @@ -6,7 +6,7 @@
    19.4  Well-founded Recursion
    19.5  *)
    19.6  
    19.7 -WF = Trancl +
    19.8 +WF = Trancl + "mono" +
    19.9  consts
   19.10      wf		 ::      "i=>o"
   19.11      wftrec,wfrec ::      "[i, i, [i,i]=>i] =>i"
    20.1 --- a/src/ZF/arith.thy	Tue Nov 16 14:23:19 1993 +0100
    20.2 +++ b/src/ZF/arith.thy	Tue Nov 16 14:24:21 1993 +0100
    20.3 @@ -6,7 +6,7 @@
    20.4  Arithmetic operators and their definitions
    20.5  *)
    20.6  
    20.7 -Arith = Epsilon +
    20.8 +Arith = Epsilon + "simpdata" +
    20.9  consts
   20.10      rec  :: "[i, i, [i,i]=>i]=>i"
   20.11      "#*" :: "[i,i]=>i"      		(infixl 70)
    21.1 --- a/src/ZF/bool.thy	Tue Nov 16 14:23:19 1993 +0100
    21.2 +++ b/src/ZF/bool.thy	Tue Nov 16 14:24:21 1993 +0100
    21.3 @@ -6,7 +6,7 @@
    21.4  Booleans in Zermelo-Fraenkel Set Theory 
    21.5  *)
    21.6  
    21.7 -Bool = ZF +
    21.8 +Bool = ZF + "simpdata" +
    21.9  consts
   21.10      "1"		::      "i"     	("1")
   21.11      bool        ::      "i"
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/ZF/coinductive.thy	Tue Nov 16 14:24:21 1993 +0100
    22.3 @@ -0,0 +1,3 @@
    22.4 +(*Dummy theory to document dependencies *)
    22.5 +
    22.6 +coinductive = "ind_syntax" + "intr_elim"
    22.7 \ No newline at end of file
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/src/ZF/constructor.thy	Tue Nov 16 14:24:21 1993 +0100
    23.3 @@ -0,0 +1,3 @@
    23.4 +(*Dummy theory to document dependencies *)
    23.5 +
    23.6 +constructor = "ind_syntax"
    23.7 \ No newline at end of file
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/src/ZF/datatype.thy	Tue Nov 16 14:24:21 1993 +0100
    24.3 @@ -0,0 +1,4 @@
    24.4 +(*Dummy theory to document dependencies *)
    24.5 +
    24.6 +Datatype = "constructor" + "inductive" + "coinductive" + Univ + QUniv
    24.7 +               (*this must be capital to avoid conflicts with ML's "datatype" *)
    24.8 \ No newline at end of file
    25.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.2 +++ b/src/ZF/domrange.thy	Tue Nov 16 14:24:21 1993 +0100
    25.3 @@ -0,0 +1,3 @@
    25.4 +(*Dummy theory to document dependencies *)
    25.5 +
    25.6 +domrange = "pair" + "subset"
    26.1 --- a/src/ZF/epsilon.thy	Tue Nov 16 14:23:19 1993 +0100
    26.2 +++ b/src/ZF/epsilon.thy	Tue Nov 16 14:24:21 1993 +0100
    26.3 @@ -6,7 +6,7 @@
    26.4  Epsilon induction and recursion
    26.5  *)
    26.6  
    26.7 -Epsilon = Nat +
    26.8 +Epsilon = Nat + "mono" +
    26.9  consts
   26.10      eclose,rank ::      "i=>i"
   26.11      transrec    ::      "[i, [i,i]=>i] =>i"
    27.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.2 +++ b/src/ZF/equalities.thy	Tue Nov 16 14:24:21 1993 +0100
    27.3 @@ -0,0 +1,3 @@
    27.4 +(*Dummy theory to document dependencies *)
    27.5 +
    27.6 +equalities = "domrange"
    27.7 \ No newline at end of file
    28.1 --- a/src/ZF/fin.ML	Tue Nov 16 14:23:19 1993 +0100
    28.2 +++ b/src/ZF/fin.ML	Tue Nov 16 14:24:21 1993 +0100
    28.3 @@ -28,6 +28,8 @@
    28.4    val type_intrs = [empty_subsetI, cons_subsetI, PowI]
    28.5    val type_elims = [make_elim PowD]);
    28.6  
    28.7 +store_theory "Fin" Fin.thy;
    28.8 +
    28.9  val [Fin_0I, Fin_consI] = Fin.intrs;
   28.10  
   28.11  
    29.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.2 +++ b/src/ZF/fin.thy	Tue Nov 16 14:24:21 1993 +0100
    29.3 @@ -0,0 +1,3 @@
    29.4 +(*Dummy theory to document dependencies *)
    29.5 +
    29.6 +fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities"
    30.1 --- a/src/ZF/fixedpt.thy	Tue Nov 16 14:23:19 1993 +0100
    30.2 +++ b/src/ZF/fixedpt.thy	Tue Nov 16 14:24:21 1993 +0100
    30.3 @@ -6,7 +6,7 @@
    30.4  Least and greatest fixed points
    30.5  *)
    30.6  
    30.7 -Fixedpt = ZF +
    30.8 +Fixedpt = ZF + "domrange" +
    30.9  consts
   30.10    bnd_mono    :: "[i,i=>i]=>o"
   30.11    lfp, gfp    :: "[i,i=>i]=>i"
    31.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.2 +++ b/src/ZF/func.thy	Tue Nov 16 14:24:21 1993 +0100
    31.3 @@ -0,0 +1,3 @@
    31.4 +(*Dummy theory to document dependencies *)
    31.5 +
    31.6 +func = "domrange"
    31.7 \ No newline at end of file
    32.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.2 +++ b/src/ZF/ind_syntax.thy	Tue Nov 16 14:24:21 1993 +0100
    32.3 @@ -0,0 +1,3 @@
    32.4 +(*Dummy theory to document dependencies *)
    32.5 +
    32.6 +ind_syntax = "mono"
    33.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.2 +++ b/src/ZF/indrule.thy	Tue Nov 16 14:24:21 1993 +0100
    33.3 @@ -0,0 +1,3 @@
    33.4 +(*Dummy theory to document dependencies *)
    33.5 +
    33.6 +indrule = "ind_syntax" + "intr_elim"
    34.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    34.2 +++ b/src/ZF/inductive.thy	Tue Nov 16 14:24:21 1993 +0100
    34.3 @@ -0,0 +1,3 @@
    34.4 +(*Dummy theory to document dependencies *)
    34.5 +
    34.6 +inductive = "indrule"
    35.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    35.2 +++ b/src/ZF/intr_elim.thy	Tue Nov 16 14:24:21 1993 +0100
    35.3 @@ -0,0 +1,3 @@
    35.4 +(*Dummy theory to document dependencies *)
    35.5 +
    35.6 +intr_elim = Fixedpt + "ind_syntax"
    36.1 --- a/src/ZF/list.ML	Tue Nov 16 14:23:19 1993 +0100
    36.2 +++ b/src/ZF/list.ML	Tue Nov 16 14:24:21 1993 +0100
    36.3 @@ -21,6 +21,8 @@
    36.4    val type_intrs = datatype_intrs
    36.5    val type_elims = datatype_elims);
    36.6  
    36.7 +store_theory "List" List.thy;
    36.8 +
    36.9  val [NilI, ConsI] = List.intrs;
   36.10  
   36.11  (*An elimination rule, for type-checking*)
    37.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    37.2 +++ b/src/ZF/list.thy	Tue Nov 16 14:24:21 1993 +0100
    37.3 @@ -0,0 +1,3 @@
    37.4 +(*Dummy theory to document dependencies *)
    37.5 +
    37.6 +list = Univ + "Datatype" + "intr_elim"
    38.1 --- a/src/ZF/listfn.thy	Tue Nov 16 14:23:19 1993 +0100
    38.2 +++ b/src/ZF/listfn.thy	Tue Nov 16 14:24:21 1993 +0100
    38.3 @@ -10,7 +10,7 @@
    38.4  although complicating its derivation.
    38.5  *)
    38.6  
    38.7 -ListFn = List +
    38.8 +ListFn = List + "constructor" +
    38.9  consts
   38.10    "@"	     :: "[i,i]=>i"      			(infixr 60)
   38.11    list_rec   :: "[i, i, [i,i,i]=>i] => i"
    39.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    39.2 +++ b/src/ZF/mono.thy	Tue Nov 16 14:24:21 1993 +0100
    39.3 @@ -0,0 +1,3 @@
    39.4 +(*Dummy theory to document dependencies *)
    39.5 +
    39.6 +mono = QPair + Sum
    40.1 --- a/src/ZF/nat.thy	Tue Nov 16 14:23:19 1993 +0100
    40.2 +++ b/src/ZF/nat.thy	Tue Nov 16 14:24:21 1993 +0100
    40.3 @@ -6,7 +6,7 @@
    40.4  Natural numbers in Zermelo-Fraenkel Set Theory 
    40.5  *)
    40.6  
    40.7 -Nat = Ord + Bool + 
    40.8 +Nat = Ord + Bool + "mono" +
    40.9  consts
   40.10      nat 	::      "i"
   40.11      nat_case    ::      "[i, i=>i, i]=>i"
    41.1 --- a/src/ZF/ord.thy	Tue Nov 16 14:23:19 1993 +0100
    41.2 +++ b/src/ZF/ord.thy	Tue Nov 16 14:24:21 1993 +0100
    41.3 @@ -6,7 +6,7 @@
    41.4  Ordinals in Zermelo-Fraenkel Set Theory 
    41.5  *)
    41.6  
    41.7 -Ord = WF +
    41.8 +Ord = WF + "simpdata" + "equalities" +
    41.9  consts
   41.10    Memrel      	:: "i=>i"
   41.11    Transset,Ord  :: "i=>o"
    42.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    42.2 +++ b/src/ZF/pair.thy	Tue Nov 16 14:24:21 1993 +0100
    42.3 @@ -0,0 +1,3 @@
    42.4 +(*Dummy theory to document dependencies *)
    42.5 +
    42.6 +pair = "upair"
    43.1 --- a/src/ZF/perm.thy	Tue Nov 16 14:23:19 1993 +0100
    43.2 +++ b/src/ZF/perm.thy	Tue Nov 16 14:24:21 1993 +0100
    43.3 @@ -9,7 +9,7 @@
    43.4    -- Lemmas for the Schroeder-Bernstein Theorem
    43.5  *)
    43.6  
    43.7 -Perm = ZF +
    43.8 +Perm = ZF + "mono" +
    43.9  consts
   43.10      O    	::      "[i,i]=>i"      (infixr 60)
   43.11      id  	::      "i=>i"
    44.1 --- a/src/ZF/qpair.thy	Tue Nov 16 14:23:19 1993 +0100
    44.2 +++ b/src/ZF/qpair.thy	Tue Nov 16 14:24:21 1993 +0100
    44.3 @@ -11,7 +11,7 @@
    44.4  1966.
    44.5  *)
    44.6  
    44.7 -QPair = Sum +
    44.8 +QPair = Sum + "simpdata" +
    44.9  consts
   44.10    QPair     :: "[i, i] => i"               	("<(_;/ _)>")
   44.11    qsplit    :: "[[i,i] => i, i] => i"
    45.1 --- a/src/ZF/quniv.thy	Tue Nov 16 14:23:19 1993 +0100
    45.2 +++ b/src/ZF/quniv.thy	Tue Nov 16 14:24:21 1993 +0100
    45.3 @@ -6,7 +6,7 @@
    45.4  A small universe for lazy recursive types
    45.5  *)
    45.6  
    45.7 -QUniv = Univ + QPair +
    45.8 +QUniv = Univ + QPair + "mono" + "equalities" +
    45.9  consts
   45.10      quniv        :: "i=>i"
   45.11  
    46.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    46.2 +++ b/src/ZF/simpdata.thy	Tue Nov 16 14:24:21 1993 +0100
    46.3 @@ -0,0 +1,3 @@
    46.4 +(*Dummy theory to document dependencies *)
    46.5 +
    46.6 +simpdata = "func"
    46.7 \ No newline at end of file
    47.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    47.2 +++ b/src/ZF/subset.thy	Tue Nov 16 14:24:21 1993 +0100
    47.3 @@ -0,0 +1,3 @@
    47.4 +(*Dummy theory to document dependencies *)
    47.5 +
    47.6 +subset = "upair"
    48.1 --- a/src/ZF/sum.thy	Tue Nov 16 14:23:19 1993 +0100
    48.2 +++ b/src/ZF/sum.thy	Tue Nov 16 14:24:21 1993 +0100
    48.3 @@ -7,7 +7,7 @@
    48.4  "Part" primitive for simultaneous recursive type definitions
    48.5  *)
    48.6  
    48.7 -Sum = Bool +
    48.8 +Sum = Bool + "simpdata" +
    48.9  consts
   48.10      "+"    	:: "[i,i]=>i"      		(infixr 65)
   48.11      Inl,Inr     :: "i=>i"
    49.1 --- a/src/ZF/trancl.thy	Tue Nov 16 14:23:19 1993 +0100
    49.2 +++ b/src/ZF/trancl.thy	Tue Nov 16 14:24:21 1993 +0100
    49.3 @@ -6,7 +6,7 @@
    49.4  Transitive closure of a relation
    49.5  *)
    49.6  
    49.7 -Trancl = Fixedpt + Perm + 
    49.8 +Trancl = Fixedpt + Perm + "mono" +
    49.9  consts
   49.10      "rtrancl"	:: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
   49.11      "trancl"    :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
    50.1 --- a/src/ZF/univ.thy	Tue Nov 16 14:23:19 1993 +0100
    50.2 +++ b/src/ZF/univ.thy	Tue Nov 16 14:24:21 1993 +0100
    50.3 @@ -8,7 +8,7 @@
    50.4  Standard notation for Vset(i) is V(i), but users might want V for a variable
    50.5  *)
    50.6  
    50.7 -Univ = Arith + Sum +
    50.8 +Univ = Arith + Sum + "mono" +
    50.9  consts
   50.10      Limit       ::      "i=>o"
   50.11      Vfrom       ::      "[i,i]=>i"
    51.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    51.2 +++ b/src/ZF/upair.thy	Tue Nov 16 14:24:21 1993 +0100
    51.3 @@ -0,0 +1,3 @@
    51.4 +(*Dummy theory to document dependencies *)
    51.5 +
    51.6 +upair = ZF
    52.1 --- a/src/ZF/wf.thy	Tue Nov 16 14:23:19 1993 +0100
    52.2 +++ b/src/ZF/wf.thy	Tue Nov 16 14:24:21 1993 +0100
    52.3 @@ -6,7 +6,7 @@
    52.4  Well-founded Recursion
    52.5  *)
    52.6  
    52.7 -WF = Trancl +
    52.8 +WF = Trancl + "mono" +
    52.9  consts
   52.10      wf		 ::      "i=>o"
   52.11      wftrec,wfrec ::      "[i, i, [i,i]=>i] =>i"