equal
deleted
inserted
replaced
77 fun interpretation_cmd x = gen_interpretation Expression.read_goal_expression |
77 fun interpretation_cmd x = gen_interpretation Expression.read_goal_expression |
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 definesK = "defines"; |
|
83 val _ = Keyword.keyword definesK; |
|
84 |
|
85 val _ = |
82 val _ = |
86 Outer_Syntax.command "interpretation" |
83 Outer_Syntax.command "interpretation" |
87 "prove interpretation of locale expression in theory" Keyword.thy_goal |
84 "prove interpretation of locale expression in theory" Keyword.thy_goal |
88 (Parse.!!! (Parse_Spec.locale_expression true) -- |
85 (Parse.!!! (Parse_Spec.locale_expression true) -- |
89 Scan.optional (Parse.$$$ definesK |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" |
86 Scan.optional (Parse.$$$ "defines" |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" |
90 -- ((Parse.binding -- Parse.opt_mixfix') --| Parse.$$$ "is" -- Parse.term))) [] -- |
87 -- ((Parse.binding -- Parse.opt_mixfix') --| Parse.$$$ "is" -- Parse.term))) [] -- |
91 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)) [] |
92 >> (fn ((expr, defs), equations) => Toplevel.print o |
89 >> (fn ((expr, defs), equations) => Toplevel.print o |
93 Toplevel.theory_to_proof (interpretation_cmd expr defs equations))); |
90 Toplevel.theory_to_proof (interpretation_cmd expr defs equations))); |
94 |
91 |