| changeset 90 | a90653dabebc |
| parent 75 | 144ec40f2650 |
| child 120 | 09287f26bfb8 |
--- a/src/ZF/ROOT.ML Thu Nov 04 10:34:49 1993 +0100 +++ b/src/ZF/ROOT.ML Thu Nov 04 14:11:59 1993 +0100 @@ -47,11 +47,11 @@ use_thy "fixedpt"; (*Inductive/co-inductive definitions*) -use "ind-syntax.ML"; -use "intr-elim.ML"; +use "ind_syntax.ML"; +use "intr_elim.ML"; use "indrule.ML"; use "inductive.ML"; -use "co-inductive.ML"; +use "coinductive.ML"; use_thy "perm"; use_thy "trancl";