equal
deleted
inserted
replaced
42 NewLocale.print_locale (Toplevel.theory_of state) show_facts name)))); |
42 NewLocale.print_locale (Toplevel.theory_of state) show_facts name)))); |
43 |
43 |
44 val _ = |
44 val _ = |
45 OuterSyntax.command "interpretation" |
45 OuterSyntax.command "interpretation" |
46 "prove interpretation of locale expression in theory" K.thy_goal |
46 "prove interpretation of locale expression in theory" K.thy_goal |
47 (P.!!! SpecParse.locale_expression |
47 (P.!!! SpecParse.locale_expression -- |
48 >> (fn expr => Toplevel.print o |
48 Scan.optional (P.$$$ "where" |-- P.and_list1 (P.alt_string >> Facts.Fact || |
49 Toplevel.theory_to_proof (Expression.interpretation_cmd expr))); |
49 P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named)) [] |
|
50 >> (fn (expr, mixin) => Toplevel.print o |
|
51 Toplevel.theory_to_proof (Expression.interpretation_cmd expr mixin))); |
50 |
52 |
51 val _ = |
53 val _ = |
52 OuterSyntax.command "interpret" |
54 OuterSyntax.command "interpret" |
53 "prove interpretation of locale expression in proof context" |
55 "prove interpretation of locale expression in proof context" |
54 (K.tag_proof K.prf_goal) |
56 (K.tag_proof K.prf_goal) |