equal
deleted
inserted
replaced
93 fun permanent_interpretation_cmd x = gen_permanent_interpretation read_interpretation x; |
93 fun permanent_interpretation_cmd x = gen_permanent_interpretation read_interpretation x; |
94 |
94 |
95 end; |
95 end; |
96 |
96 |
97 val _ = |
97 val _ = |
98 Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"} |
98 Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation} |
99 "prove interpretation of locale expression into named theory" |
99 "prove interpretation of locale expression into named theory" |
100 (Parse.!!! (Parse_Spec.locale_expression true) -- |
100 (Parse.!!! (Parse_Spec.locale_expression true) -- |
101 Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" |
101 Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" |
102 -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] -- |
102 -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] -- |
103 Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] |
103 Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] |