equal
deleted
inserted
replaced
401 val _ = |
401 val _ = |
402 OuterSyntax.command "sublocale" |
402 OuterSyntax.command "sublocale" |
403 "prove sublocale relation between a locale and a locale expression" K.thy_goal |
403 "prove sublocale relation between a locale and a locale expression" K.thy_goal |
404 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression |
404 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression |
405 >> (fn (loc, expr) => |
405 >> (fn (loc, expr) => |
406 Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd (K I) loc expr)))); |
406 Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)))); |
407 |
407 |
408 val _ = |
408 val _ = |
409 OuterSyntax.command "interpretation" |
409 OuterSyntax.command "interpretation" |
410 "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 |
411 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr |
411 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr |