| changeset 9205 | f171fa6a0989 |
| parent 9000 | c20d58286a51 |
| child 11675 | c87d695f4adb |
--- a/src/FOL/ex/ROOT.ML Thu Jun 29 22:39:57 2000 +0200 +++ b/src/FOL/ex/ROOT.ML Thu Jun 29 22:48:08 2000 +0200 @@ -12,7 +12,7 @@ time_use_thy "Prolog"; writeln"\n** Intuitionistic examples **\n"; -time_use "int.ML"; +time_use_thy "int"; val thy = IFOL.thy and tac = IntPr.fast_tac 1; time_use "prop.ML";