equal
deleted
inserted
replaced
117 |
117 |
118 val invokeP = |
118 val invokeP = |
119 OuterSyntax.command "invoke" |
119 OuterSyntax.command "invoke" |
120 "schematic invocation of locale expression in proof context" |
120 "schematic invocation of locale expression in proof context" |
121 (K.tag_proof K.prf_goal) |
121 (K.tag_proof K.prf_goal) |
122 (P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts -- P.for_fixes |
122 (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes |
123 >> (fn (((name, expr), insts), fixes) => |
123 >> (fn (((name, expr), insts), fixes) => |
124 Toplevel.print o Toplevel.proof' (invoke name expr insts fixes))); |
124 Toplevel.print o Toplevel.proof' (invoke name expr insts fixes))); |
125 |
125 |
126 val _ = OuterSyntax.add_parsers [invokeP]; |
126 val _ = OuterSyntax.add_parsers [invokeP]; |
127 |
127 |