equal
deleted
inserted
replaced
397 (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin))); |
397 (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin))); |
398 |
398 |
399 val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Name.no_binding; |
399 val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Name.no_binding; |
400 |
400 |
401 val _ = |
401 val _ = |
|
402 OuterSyntax.command "sublocale" |
|
403 "prove sublocale relation between a locale and a locale expression" K.thy_goal |
|
404 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression |
|
405 >> (fn (loc, expr) => |
|
406 Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale (K I) loc expr)))); |
|
407 |
|
408 val _ = |
402 OuterSyntax.command "interpretation" |
409 OuterSyntax.command "interpretation" |
403 "prove and register interpretation of locale expression in theory or locale" K.thy_goal |
410 "prove and register interpretation of locale expression in theory or locale" K.thy_goal |
404 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr |
411 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr |
405 >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) || |
412 >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) || |
406 opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts |
413 opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts |