src/Pure/Pure.thy
changeset 66248 df85956228c2
parent 66194 8d34d42c40cb
child 66251 cd935b7cb3fb
     1.1 --- a/src/Pure/Pure.thy	Mon Jul 03 09:57:26 2017 +0200
     1.2 +++ b/src/Pure/Pure.thy	Mon Jul 03 13:51:55 2017 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    and "typedecl" "type_synonym" "nonterminal" "judgment"
     1.5      "consts" "syntax" "no_syntax" "translations" "no_translations"
     1.6      "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
     1.7 -    "no_notation" "axiomatization" "lemmas" "declare"
     1.8 +    "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
     1.9      "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    1.10    and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
    1.11    and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
    1.12 @@ -374,6 +374,16 @@
    1.13        Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
    1.14        >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
    1.15  
    1.16 +val _ =
    1.17 +  Outer_Syntax.local_theory @{command_keyword alias} "name-space alias for constant"
    1.18 +    (Parse.binding -- (Parse.!!! @{keyword =} |-- Parse.position Parse.name)
    1.19 +      >> Specification.alias_cmd);
    1.20 +
    1.21 +val _ =
    1.22 +  Outer_Syntax.local_theory @{command_keyword type_alias} "name-space alias for type constructor"
    1.23 +    (Parse.binding -- (Parse.!!! @{keyword =} |-- Parse.position Parse.name)
    1.24 +      >> Specification.type_alias_cmd);
    1.25 +
    1.26  in end\<close>
    1.27  
    1.28