1.1 --- a/NEWS	Fri Dec 17 17:48:05 2010 +0100
     1.2 +++ b/NEWS	Fri Dec 17 18:10:37 2010 +0100
     1.3 @@ -83,9 +83,12 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 -* Replaced command 'nonterminals' by slightly modernized version
     1.8 -'nonterminal' (with 'and' separated list of arguments).
     1.9 -INCOMPATIBILITY.
    1.10 +* Command 'type_synonym' (with single argument) replaces somewhat
    1.11 +outdated 'types', which is still available as legacy feature for some
    1.12 +time.
    1.13 +
    1.14 +* Command 'nonterminal' (with 'and' separated list of arguments)
    1.15 +replaces somewhat outdated 'nonterminals'.  INCOMPATIBILITY.
    1.16  
    1.17  * Command 'notepad' replaces former 'example_proof' for
    1.18  experimentation in Isar without any result.  INCOMPATIBILITY.

     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Fri Dec 17 17:48:05 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Dec 17 18:10:37 2010 +0100
     2.3 @@ -973,13 +973,13 @@
     2.4  
     2.5  text {*
     2.6    \begin{matharray}{rcll}
     2.7 -    @{command_def "types"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.8 +    @{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.9      @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    2.10      @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
    2.11    \end{matharray}
    2.12  
    2.13    \begin{rail}
    2.14 -    'types' (typespec '=' type mixfix? +)
    2.15 +    'type_synonym' (typespec '=' type mixfix?)
    2.16      ;
    2.17      'typedecl' typespec mixfix?
    2.18      ;
    2.19 @@ -989,12 +989,12 @@
    2.20  
    2.21    \begin{description}
    2.22  
    2.23 -  \item @{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
    2.24 -  \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type
    2.25 -  @{text "\<tau>"}.  Unlike actual type definitions, as are available in
    2.26 -  Isabelle/HOL for example, type synonyms are merely syntactic
    2.27 -  abbreviations without any logical significance.  Internally, type
    2.28 -  synonyms are fully expanded.
    2.29 +  \item @{command "type_synonym"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}
    2.30 +  introduces a \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the
    2.31 +  existing type @{text "\<tau>"}.  Unlike actual type definitions, as are
    2.32 +  available in Isabelle/HOL for example, type synonyms are merely
    2.33 +  syntactic abbreviations without any logical significance.
    2.34 +  Internally, type synonyms are fully expanded.
    2.35    
    2.36    \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
    2.37    type constructor @{text t}.  If the object-logic defines a base sort

     3.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Dec 17 17:48:05 2010 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Dec 17 18:10:37 2010 +0100
     3.3 @@ -1010,13 +1010,13 @@
     3.4  %
     3.5  \begin{isamarkuptext}%
     3.6  \begin{matharray}{rcll}
     3.7 -    \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     3.8 +    \indexdef{}{command}{type\_synonym}\hypertarget{command.type-synonym}{\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     3.9      \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
    3.10      \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\
    3.11    \end{matharray}
    3.12  
    3.13    \begin{rail}
    3.14 -    'types' (typespec '=' type mixfix? +)
    3.15 +    'type_synonym' (typespec '=' type mixfix?)
    3.16      ;
    3.17      'typedecl' typespec mixfix?
    3.18      ;
    3.19 @@ -1026,12 +1026,12 @@
    3.20  
    3.21    \begin{description}
    3.22  
    3.23 -  \item \hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} introduces a
    3.24 -  \emph{type synonym} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} for the existing type
    3.25 -  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}.  Unlike actual type definitions, as are available in
    3.26 -  Isabelle/HOL for example, type synonyms are merely syntactic
    3.27 -  abbreviations without any logical significance.  Internally, type
    3.28 -  synonyms are fully expanded.
    3.29 +  \item \hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}
    3.30 +  introduces a \emph{type synonym} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} for the
    3.31 +  existing type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}.  Unlike actual type definitions, as are
    3.32 +  available in Isabelle/HOL for example, type synonyms are merely
    3.33 +  syntactic abbreviations without any logical significance.
    3.34 +  Internally, type synonyms are fully expanded.
    3.35    
    3.36    \item \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} declares a new
    3.37    type constructor \isa{t}.  If the object-logic defines a base sort

     4.1 --- a/etc/isar-keywords-ZF.el	Fri Dec 17 17:48:05 2010 +0100
     4.2 +++ b/etc/isar-keywords-ZF.el	Fri Dec 17 18:10:37 2010 +0100
     4.3 @@ -189,6 +189,7 @@
     4.4      "txt_raw"
     4.5      "typ"
     4.6      "type_notation"
     4.7 +    "type_synonym"
     4.8      "typed_print_translation"
     4.9      "typedecl"
    4.10      "types"
    4.11 @@ -403,6 +404,7 @@
    4.12      "theorems"
    4.13      "translations"
    4.14      "type_notation"
    4.15 +    "type_synonym"
    4.16      "typed_print_translation"
    4.17      "typedecl"
    4.18      "types"

     5.1 --- a/etc/isar-keywords.el	Fri Dec 17 17:48:05 2010 +0100
     5.2 +++ b/etc/isar-keywords.el	Fri Dec 17 18:10:37 2010 +0100
     5.3 @@ -250,6 +250,7 @@
     5.4      "typ"
     5.5      "type_lifting"
     5.6      "type_notation"
     5.7 +    "type_synonym"
     5.8      "typed_print_translation"
     5.9      "typedecl"
    5.10      "typedef"
    5.11 @@ -516,6 +517,7 @@
    5.12      "theorems"
    5.13      "translations"
    5.14      "type_notation"
    5.15 +    "type_synonym"
    5.16      "typed_print_translation"
    5.17      "typedecl"
    5.18      "types"

     6.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Dec 17 17:48:05 2010 +0100
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Dec 17 18:10:37 2010 +0100
     6.3 @@ -111,12 +111,19 @@
     6.4      (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
     6.5        >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
     6.6  
     6.7 +val type_abbrev =
     6.8 +  Parse.type_args -- Parse.binding --
     6.9 +    (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'));
    6.10 +
    6.11  val _ =
    6.12    Outer_Syntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl
    6.13 -    (Scan.repeat1
    6.14 -      (Parse.type_args -- Parse.binding --
    6.15 -        (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')))
    6.16 -      >> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)));
    6.17 +    (Scan.repeat1 type_abbrev >> (fn specs => fn lthy =>
    6.18 +     (legacy_feature "Old 'types' commands -- use 'type_synonym' instead";
    6.19 +      fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs) specs lthy)));
    6.20 +
    6.21 +val _ =
    6.22 +  Outer_Syntax.local_theory "type_synonym" "declare type abbreviation" Keyword.thy_decl
    6.23 +    (type_abbrev >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
    6.24  
    6.25  val _ =
    6.26    Outer_Syntax.command "nonterminal"