equal
deleted
inserted
replaced
113 |
113 |
114 (* concrete syntax *) |
114 (* concrete syntax *) |
115 |
115 |
116 local structure P = OuterParse and K = OuterKeyword in |
116 local structure P = OuterParse and K = OuterKeyword in |
117 |
117 |
118 val invokeP = |
118 val _ = |
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 (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.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]; |
|
127 |
|
128 end; |
126 end; |
129 |
127 |
130 end; |
128 end; |