src/FOL/ex/NewLocaleSetup.thy
changeset 29018 17538bdef546
parent 28993 829e684b02ef
child 29028 b5dad96c755a
child 29033 721529248e31
     1.1 --- a/src/FOL/ex/NewLocaleSetup.thy	Fri Dec 05 11:42:27 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleSetup.thy	Fri Dec 05 16:41:36 2008 +0100
     1.3 @@ -41,11 +41,19 @@
     1.4  
     1.5  val _ =
     1.6    OuterSyntax.command "interpretation"
     1.7 -    "prove and register interpretation of locale expression in theory" K.thy_goal
     1.8 +    "prove interpretation of locale expression in theory" K.thy_goal
     1.9      (P.!!! Expression.parse_expression
    1.10          >> (fn expr => Toplevel.print o
    1.11              Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
    1.12  
    1.13 +val _ =
    1.14 +  OuterSyntax.command "interpret"
    1.15 +    "prove interpretation of locale expression in proof context"
    1.16 +    (K.tag_proof K.prf_goal)
    1.17 +    (P.!!! Expression.parse_expression
    1.18 +        >> (fn expr => Toplevel.print o
    1.19 +            Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
    1.20 +
    1.21  end
    1.22  
    1.23  *}