equal
deleted
inserted
replaced
399 val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty; |
399 val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty; |
400 |
400 |
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.!!! SpecParse.locale_expression |
405 >> (fn (loc, expr) => |
405 >> (fn (loc, expr) => |
406 Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd 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" |