author | ballarin |
Fri, 02 Apr 2004 17:26:00 +0200 | |
changeset 14513 | 81d32b739a2b |
parent 14512 | e516d7cfa249 |
child 14514 | 15abb7d42e2e |
1.1 --- a/src/FOL/ex/ROOT.ML Fri Apr 02 17:06:15 2004 +0200 1.2 +++ b/src/FOL/ex/ROOT.ML Fri Apr 02 17:26:00 2004 +0200 1.3 @@ -13,6 +13,8 @@ 1.4 time_use "foundn.ML"; 1.5 time_use_thy "Prolog"; 1.6 1.7 +time_use_thy "LocaleInst"; 1.8 + 1.9 writeln"\n** Intuitionistic examples **\n"; 1.10 time_use_thy "Intuitionistic"; 1.11