--- a/src/FOL/ex/NewLocaleSetup.thy Wed Dec 03 15:27:41 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy Fri Dec 05 11:26:07 2008 +0100
@@ -1,5 +1,4 @@
(* Title: FOL/ex/NewLocaleSetup.thy
- ID: $Id$
Author: Clemens Ballarin, TU Muenchen
Testing environment for locale expressions --- experimental.
@@ -40,6 +39,13 @@
Toplevel.unknown_theory o Toplevel.keep (fn state =>
NewLocale.print_locale (Toplevel.theory_of state) show_facts name))));
+val _ =
+ OuterSyntax.command "interpretation"
+ "prove and register interpretation of locale expression in theory" K.thy_goal
+ (P.!!! Expression.parse_expression
+ >> (fn expr => Toplevel.print o
+ Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
+
end
*}