358 |
358 |
359 val interpretationP = |
359 val interpretationP = |
360 OuterSyntax.command "interpretation" |
360 OuterSyntax.command "interpretation" |
361 "prove and register interpretation of locale expression in theory or locale" K.thy_goal |
361 "prove and register interpretation of locale expression in theory or locale" K.thy_goal |
362 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! P.locale_expr |
362 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! P.locale_expr |
363 >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale)) || |
363 >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) || |
364 P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts >> (fn ((x, y), z) => |
364 P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts >> (fn ((x, y), z) => |
365 Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation x y z))); |
365 Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation I x y z))); |
366 |
366 |
367 val interpretP = |
367 val interpretP = |
368 OuterSyntax.command "interpret" |
368 OuterSyntax.command "interpret" |
369 "prove and register interpretation of locale expression in proof context" |
369 "prove and register interpretation of locale expression in proof context" |
370 (K.tag_proof K.prf_goal) |
370 (K.tag_proof K.prf_goal) |
371 (P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts >> (fn ((x, y), z) => |
371 (P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts >> (fn ((x, y), z) => |
372 Toplevel.print o Toplevel.proof' (Locale.interpret x y z))); |
372 Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single x y z))); |
373 |
373 |
374 |
374 |
375 |
375 |
376 (** proof commands **) |
376 (** proof commands **) |
377 |
377 |