1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Nov 27 10:28:27 2008 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 27 10:29:07 2008 +0100
     1.3 @@ -399,6 +399,13 @@
     1.4  val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Name.no_binding;
     1.5  
     1.6  val _ =
     1.7 +  OuterSyntax.command "sublocale"
     1.8 +    "prove sublocale relation between a locale and a locale expression" K.thy_goal
     1.9 +    (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression
    1.10 +      >> (fn (loc, expr) =>
    1.11 +        Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale (K I) loc expr))));
    1.12 +
    1.13 +val _ =
    1.14    OuterSyntax.command "interpretation"
    1.15      "prove and register interpretation of locale expression in theory or locale" K.thy_goal
    1.16      (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr