# HG changeset patch
# User ballarin
# Date 1080919560 -7200
# Node ID 81d32b739a2b9e4010f169e49c4bc1c0e15996e0
# Parent  e516d7cfa24918dbf542bed941af25086e4c2b8e
  - Experimental command for instantiation of locales in proof contexts:
        instantiate <label>: <loc>

diff -r e516d7cfa249 -r 81d32b739a2b src/FOL/ex/ROOT.ML
--- 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";