src/ZF/ex/ROOT.ML
changeset 515 abcc438e7c27
parent 489 0449a7f1add3
child 526 85d7ff169b9c
     1.1 --- a/src/ZF/ex/ROOT.ML	Fri Aug 12 11:13:23 1994 +0200
     1.2 +++ b/src/ZF/ex/ROOT.ML	Fri Aug 12 12:28:46 1994 +0200
     1.3 @@ -21,12 +21,12 @@
     1.4  time_use_thy "ex/Integ";
     1.5  (*Binary integer arithmetic*)
     1.6  use          "ex/twos_compl.ML";
     1.7 -time_use_thy "ex/BinFn";
     1.8 +time_use_thy "ex/Bin";
     1.9  
    1.10  (** Datatypes **)
    1.11 -time_use_thy "ex/BT_Fn";	(*binary trees*)
    1.12 -time_use_thy "ex/TermFn";	(*terms: recursion over the list functor*)
    1.13 -time_use_thy "ex/TF_Fn";	(*trees/forests: mutual recursion*)
    1.14 +time_use_thy "ex/BT";		(*binary trees*)
    1.15 +time_use_thy "ex/Term";		(*terms: recursion over the list functor*)
    1.16 +time_use_thy "ex/TF";		(*trees/forests: mutual recursion*)
    1.17  time_use_thy "ex/Ntree";	(*variable-branching trees; function demo*)
    1.18  time_use_thy "ex/Brouwer";	(*Brouwer ordinals: infinite-branching trees*)
    1.19  time_use_thy "ex/Data";		(*Sample datatype*)
    1.20 @@ -35,16 +35,14 @@
    1.21  (** Inductive definitions **)
    1.22  time_use_thy "ex/Rmap";		(*mapping a relation over a list*)
    1.23  time_use_thy "ex/PropLog";	(*completeness of propositional logic*)
    1.24 -(*two Coq examples by Ch. Paulin-Mohring*)
    1.25 +(*two Coq examples by Christine Paulin-Mohring*)
    1.26  time_use_thy "ex/ListN";
    1.27  time_use_thy "ex/Acc";
    1.28 -time_use_thy "ex/Contract0";	(*Contraction relation for combinatory logic*)
    1.29 -time_use_thy "ex/ParContract";	(*Diamond property for combinatory logic*)
    1.30 -time_use_thy "ex/Primrec0";
    1.31 +time_use_thy "ex/Comb";		(*Combinatory Logic example*)
    1.32 +time_use_thy "ex/Primrec";
    1.33  
    1.34  (** CoDatatypes **)
    1.35  time_use_thy "ex/LList";
    1.36 -time_use_thy "ex/LListFn";
    1.37  time_use     "ex/CoUnit.ML";
    1.38  
    1.39  maketest"END: Root file for ZF Set Theory examples";