equal
deleted
inserted
replaced
78 Expression.read_declaration Syntax.parse_term Syntax.parse_prop Attrib.intern_src x; |
78 Expression.read_declaration Syntax.parse_term Syntax.parse_prop Attrib.intern_src x; |
79 |
79 |
80 end; |
80 end; |
81 |
81 |
82 val _ = |
82 val _ = |
83 Outer_Syntax.command "interpretation" |
83 Outer_Syntax.command @{command_spec "interpretation"} |
84 "prove interpretation of locale expression in theory" Keyword.thy_goal |
84 "prove interpretation of locale expression in theory" |
85 (Parse.!!! (Parse_Spec.locale_expression true) -- |
85 (Parse.!!! (Parse_Spec.locale_expression true) -- |
86 Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" |
86 Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" |
87 -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] -- |
87 -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] -- |
88 Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] |
88 Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] |
89 >> (fn ((expr, defs), equations) => Toplevel.print o |
89 >> (fn ((expr, defs), equations) => Toplevel.print o |