- Experimental command for instantiation of locales in proof contexts:
instantiate <label>: <loc>
--- a/src/FOL/ex/ROOT.ML Fri Apr 02 17:06:15 2004 +0200
+++ b/src/FOL/ex/ROOT.ML Fri Apr 02 17:26:00 2004 +0200
@@ -13,6 +13,8 @@
time_use "foundn.ML";
time_use_thy "Prolog";
+time_use_thy "LocaleInst";
+
writeln"\n** Intuitionistic examples **\n";
time_use_thy "Intuitionistic";