src/ZF/ROOT.ML
changeset 90 a90653dabebc
parent 75 144ec40f2650
child 120 09287f26bfb8
     1.1 --- a/src/ZF/ROOT.ML	Thu Nov 04 10:34:49 1993 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Thu Nov 04 14:11:59 1993 +0100
     1.3 @@ -47,11 +47,11 @@
     1.4  use_thy "fixedpt";
     1.5  
     1.6  (*Inductive/co-inductive definitions*)
     1.7 -use     "ind-syntax.ML";
     1.8 -use     "intr-elim.ML";
     1.9 +use     "ind_syntax.ML";
    1.10 +use     "intr_elim.ML";
    1.11  use     "indrule.ML";
    1.12  use     "inductive.ML";
    1.13 -use     "co-inductive.ML";
    1.14 +use     "coinductive.ML";
    1.15  
    1.16  use_thy "perm";
    1.17  use_thy "trancl";