- Experimental command for instantiation of locales in proof contexts:
authorballarin
Fri, 02 Apr 2004 17:26:00 +0200
changeset 1451381d32b739a2b
parent 14512 e516d7cfa249
child 14514 15abb7d42e2e
- Experimental command for instantiation of locales in proof contexts:
instantiate <label>: <loc>
src/FOL/ex/ROOT.ML
     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