replaced command 'nonterminals' by slightly modernized version 'nonterminal';
authorwenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229d797baa3d57c
parent 41228 e1fce873b814
child 41230 7cf837f1a8df
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
NEWS
doc-src/IsarRef/Thy/Inner_Syntax.thy
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Cube/Cube.thy
src/FOL/IFOL.thy
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/HOLCF/ex/Letrec.thy
src/HOL/HOLCF/ex/Pattern_Match.thy
src/HOL/Hoare_Parallel/OG_Syntax.thy
src/HOL/Hoare_Parallel/RG_Syntax.thy
src/HOL/Library/Monad_Syntax.thy
src/HOL/Library/State_Monad.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/Product_Type.thy
src/HOL/Record.thy
src/HOL/TLA/Intensional.thy
src/Pure/Isar/isar_syn.ML
src/Sequents/Sequents.thy
src/ZF/ZF.thy
src/ZF/func.thy
     1.1 --- a/NEWS	Fri Dec 17 17:08:56 2010 +0100
     1.2 +++ b/NEWS	Fri Dec 17 17:43:54 2010 +0100
     1.3 @@ -83,6 +83,10 @@
     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 +
    1.11  * Command 'notepad' replaces former 'example_proof' for
    1.12  experimentation in Isar without any result.  INCOMPATIBILITY.
    1.13  
     2.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Dec 17 17:08:56 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Dec 17 17:43:54 2010 +0100
     2.3 @@ -723,7 +723,7 @@
     2.4  
     2.5  text {*
     2.6    \begin{matharray}{rcl}
     2.7 -    @{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\
     2.8 +    @{command_def "nonterminal"} & : & @{text "theory \<rightarrow> theory"} \\
     2.9      @{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
    2.10      @{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
    2.11      @{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\
    2.12 @@ -731,7 +731,7 @@
    2.13    \end{matharray}
    2.14  
    2.15    \begin{rail}
    2.16 -    'nonterminals' (name +)
    2.17 +    'nonterminal' (name + 'and')
    2.18      ;
    2.19      ('syntax' | 'no_syntax') mode? (constdecl +)
    2.20      ;
    2.21 @@ -746,7 +746,7 @@
    2.22  
    2.23    \begin{description}
    2.24    
    2.25 -  \item @{command "nonterminals"}~@{text c} declares a type
    2.26 +  \item @{command "nonterminal"}~@{text c} declares a type
    2.27    constructor @{text c} (without arguments) to act as purely syntactic
    2.28    type: a nonterminal symbol of the inner syntax.
    2.29  
     3.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Dec 17 17:08:56 2010 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Dec 17 17:43:54 2010 +0100
     3.3 @@ -742,7 +742,7 @@
     3.4  %
     3.5  \begin{isamarkuptext}%
     3.6  \begin{matharray}{rcl}
     3.7 -    \indexdef{}{command}{nonterminals}\hypertarget{command.nonterminals}{\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
     3.8 +    \indexdef{}{command}{nonterminal}\hypertarget{command.nonterminal}{\hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
     3.9      \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
    3.10      \indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}syntax}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
    3.11      \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
    3.12 @@ -750,7 +750,7 @@
    3.13    \end{matharray}
    3.14  
    3.15    \begin{rail}
    3.16 -    'nonterminals' (name +)
    3.17 +    'nonterminal' (name + 'and')
    3.18      ;
    3.19      ('syntax' | 'no_syntax') mode? (constdecl +)
    3.20      ;
    3.21 @@ -765,7 +765,7 @@
    3.22  
    3.23    \begin{description}
    3.24    
    3.25 -  \item \hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c} declares a type
    3.26 +  \item \hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}~\isa{c} declares a type
    3.27    constructor \isa{c} (without arguments) to act as purely syntactic
    3.28    type: a nonterminal symbol of the inner syntax.
    3.29  
     4.1 --- a/etc/isar-keywords-ZF.el	Fri Dec 17 17:08:56 2010 +0100
     4.2 +++ b/etc/isar-keywords-ZF.el	Fri Dec 17 17:43:54 2010 +0100
     4.3 @@ -103,7 +103,7 @@
     4.4      "no_syntax"
     4.5      "no_translations"
     4.6      "no_type_notation"
     4.7 -    "nonterminals"
     4.8 +    "nonterminal"
     4.9      "notation"
    4.10      "note"
    4.11      "notepad"
    4.12 @@ -381,7 +381,7 @@
    4.13      "no_syntax"
    4.14      "no_translations"
    4.15      "no_type_notation"
    4.16 -    "nonterminals"
    4.17 +    "nonterminal"
    4.18      "notation"
    4.19      "notepad"
    4.20      "oracle"
     5.1 --- a/etc/isar-keywords.el	Fri Dec 17 17:08:56 2010 +0100
     5.2 +++ b/etc/isar-keywords.el	Fri Dec 17 17:43:54 2010 +0100
     5.3 @@ -140,7 +140,7 @@
     5.4      "nominal_inductive"
     5.5      "nominal_inductive2"
     5.6      "nominal_primrec"
     5.7 -    "nonterminals"
     5.8 +    "nonterminal"
     5.9      "notation"
    5.10      "note"
    5.11      "notepad"
    5.12 @@ -487,7 +487,7 @@
    5.13      "no_translations"
    5.14      "no_type_notation"
    5.15      "nominal_datatype"
    5.16 -    "nonterminals"
    5.17 +    "nonterminal"
    5.18      "notation"
    5.19      "notepad"
    5.20      "oracle"
     6.1 --- a/src/Cube/Cube.thy	Fri Dec 17 17:08:56 2010 +0100
     6.2 +++ b/src/Cube/Cube.thy	Fri Dec 17 17:43:54 2010 +0100
     6.3 @@ -14,8 +14,7 @@
     6.4  typedecl "context"
     6.5  typedecl typing
     6.6  
     6.7 -nonterminals
     6.8 -  context' typing'
     6.9 +nonterminal context' and typing'
    6.10  
    6.11  consts
    6.12    Abs :: "[term, term => term] => term"
     7.1 --- a/src/FOL/IFOL.thy	Fri Dec 17 17:08:56 2010 +0100
     7.2 +++ b/src/FOL/IFOL.thy	Fri Dec 17 17:43:54 2010 +0100
     7.3 @@ -754,7 +754,7 @@
     7.4  
     7.5  subsection {* ``Let'' declarations *}
     7.6  
     7.7 -nonterminals letbinds letbind
     7.8 +nonterminal letbinds and letbind
     7.9  
    7.10  definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where
    7.11      "Let(s, f) == f(s)"
     8.1 --- a/src/HOL/Fun.thy	Fri Dec 17 17:08:56 2010 +0100
     8.2 +++ b/src/HOL/Fun.thy	Fri Dec 17 17:43:54 2010 +0100
     8.3 @@ -558,8 +558,8 @@
     8.4    fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
     8.5    "fun_upd f a b == % x. if x=a then b else f x"
     8.6  
     8.7 -nonterminals
     8.8 -  updbinds updbind
     8.9 +nonterminal updbinds and updbind
    8.10 +
    8.11  syntax
    8.12    "_updbind" :: "['a, 'a] => updbind"             ("(2_ :=/ _)")
    8.13    ""         :: "updbind => updbinds"             ("_")
     9.1 --- a/src/HOL/HOL.thy	Fri Dec 17 17:08:56 2010 +0100
     9.2 +++ b/src/HOL/HOL.thy	Fri Dec 17 17:43:54 2010 +0100
     9.3 @@ -103,9 +103,8 @@
     9.4  notation (xsymbols)
     9.5    iff  (infixr "\<longleftrightarrow>" 25)
     9.6  
     9.7 -nonterminals
     9.8 -  letbinds  letbind
     9.9 -  case_syn  cases_syn
    9.10 +nonterminal letbinds and letbind
    9.11 +nonterminal case_syn and cases_syn
    9.12  
    9.13  syntax
    9.14    "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)
    10.1 --- a/src/HOL/HOLCF/ex/Letrec.thy	Fri Dec 17 17:08:56 2010 +0100
    10.2 +++ b/src/HOL/HOLCF/ex/Letrec.thy	Fri Dec 17 17:43:54 2010 +0100
    10.3 @@ -14,8 +14,7 @@
    10.4    CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
    10.5    "CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
    10.6  
    10.7 -nonterminals
    10.8 -  recbinds recbindt recbind
    10.9 +nonterminal recbinds and recbindt and recbind
   10.10  
   10.11  syntax
   10.12    "_recbind"  :: "['a, 'a] \<Rightarrow> recbind"               ("(2_ =/ _)" 10)
    11.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Dec 17 17:08:56 2010 +0100
    11.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Dec 17 17:43:54 2010 +0100
    11.3 @@ -100,8 +100,7 @@
    11.4  
    11.5  subsection {* Case syntax *}
    11.6  
    11.7 -nonterminals
    11.8 -  Case_syn  Cases_syn
    11.9 +nonterminal Case_syn and Cases_syn
   11.10  
   11.11  syntax
   11.12    "_Case_syntax":: "['a, Cases_syn] => 'b"               ("(Case _ of/ _)" 10)
    12.1 --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Dec 17 17:08:56 2010 +0100
    12.2 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Dec 17 17:43:54 2010 +0100
    12.3 @@ -56,8 +56,7 @@
    12.4    "r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT CONST True THEN c END"
    12.5    "r WAIT b END" \<rightleftharpoons> "r AWAIT b THEN SKIP END"
    12.6   
    12.7 -nonterminals
    12.8 -  prgs
    12.9 +nonterminal prgs
   12.10  
   12.11  syntax
   12.12    "_PAR" :: "prgs \<Rightarrow> 'a"              ("COBEGIN//_//COEND" [57] 56)
    13.1 --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Fri Dec 17 17:08:56 2010 +0100
    13.2 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Fri Dec 17 17:43:54 2010 +0100
    13.3 @@ -27,8 +27,7 @@
    13.4    "\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT CONST True THEN c END"
    13.5    "WAIT b END" \<rightleftharpoons> "AWAIT b THEN SKIP END"
    13.6  
    13.7 -nonterminals
    13.8 -  prgs
    13.9 +nonterminal prgs
   13.10  
   13.11  syntax
   13.12    "_PAR"        :: "prgs \<Rightarrow> 'a"              ("COBEGIN//_//COEND" 60)
    14.1 --- a/src/HOL/Library/Monad_Syntax.thy	Fri Dec 17 17:08:56 2010 +0100
    14.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Fri Dec 17 17:43:54 2010 +0100
    14.3 @@ -37,8 +37,7 @@
    14.4  notation (latex output)
    14.5    bind_do (infixr "\<bind>" 54)
    14.6  
    14.7 -nonterminals
    14.8 -  do_binds do_bind
    14.9 +nonterminal do_binds and do_bind
   14.10  
   14.11  syntax
   14.12    "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
    15.1 --- a/src/HOL/Library/State_Monad.thy	Fri Dec 17 17:08:56 2010 +0100
    15.2 +++ b/src/HOL/Library/State_Monad.thy	Fri Dec 17 17:43:54 2010 +0100
    15.3 @@ -114,8 +114,7 @@
    15.4  
    15.5  subsection {* Do-syntax *}
    15.6  
    15.7 -nonterminals
    15.8 -  sdo_binds sdo_bind
    15.9 +nonterminal sdo_binds and sdo_bind
   15.10  
   15.11  syntax
   15.12    "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)
    16.1 --- a/src/HOL/List.thy	Fri Dec 17 17:08:56 2010 +0100
    16.2 +++ b/src/HOL/List.thy	Fri Dec 17 17:43:54 2010 +0100
    16.3 @@ -123,7 +123,7 @@
    16.4      "list_update [] i v = []"
    16.5    | "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
    16.6  
    16.7 -nonterminals lupdbinds lupdbind
    16.8 +nonterminal lupdbinds and lupdbind
    16.9  
   16.10  syntax
   16.11    "_lupdbind":: "['a, 'a] => lupdbind"    ("(2_ :=/ _)")
   16.12 @@ -346,7 +346,7 @@
   16.13  @{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
   16.14  *)
   16.15  
   16.16 -nonterminals lc_qual lc_quals
   16.17 +nonterminal lc_qual and lc_quals
   16.18  
   16.19  syntax
   16.20  "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
    17.1 --- a/src/HOL/Map.thy	Fri Dec 17 17:08:56 2010 +0100
    17.2 +++ b/src/HOL/Map.thy	Fri Dec 17 17:43:54 2010 +0100
    17.3 @@ -50,8 +50,7 @@
    17.4    map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool"  (infix "\<subseteq>\<^sub>m" 50) where
    17.5    "(m\<^isub>1 \<subseteq>\<^sub>m m\<^isub>2) = (\<forall>a \<in> dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a)"
    17.6  
    17.7 -nonterminals
    17.8 -  maplets maplet
    17.9 +nonterminal maplets and maplet
   17.10  
   17.11  syntax
   17.12    "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
    18.1 --- a/src/HOL/Product_Type.thy	Fri Dec 17 17:08:56 2010 +0100
    18.2 +++ b/src/HOL/Product_Type.thy	Fri Dec 17 17:43:54 2010 +0100
    18.3 @@ -173,8 +173,7 @@
    18.4    abstractions.
    18.5  *}
    18.6  
    18.7 -nonterminals
    18.8 -  tuple_args patterns
    18.9 +nonterminal tuple_args and patterns
   18.10  
   18.11  syntax
   18.12    "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1'(_,/ _'))")
    19.1 --- a/src/HOL/Record.thy	Fri Dec 17 17:08:56 2010 +0100
    19.2 +++ b/src/HOL/Record.thy	Fri Dec 17 17:43:54 2010 +0100
    19.3 @@ -419,8 +419,15 @@
    19.4  
    19.5  subsection {* Concrete record syntax *}
    19.6  
    19.7 -nonterminals
    19.8 -  ident field_type field_types field fields field_update field_updates
    19.9 +nonterminal
   19.10 +  ident and
   19.11 +  field_type and
   19.12 +  field_types and
   19.13 +  field and
   19.14 +  fields and
   19.15 +  field_update and
   19.16 +  field_updates
   19.17 +
   19.18  syntax
   19.19    "_constify"           :: "id => ident"                        ("_")
   19.20    "_constify"           :: "longid => ident"                    ("_")
    20.1 --- a/src/HOL/TLA/Intensional.thy	Fri Dec 17 17:08:56 2010 +0100
    20.2 +++ b/src/HOL/TLA/Intensional.thy	Fri Dec 17 17:43:54 2010 +0100
    20.3 @@ -33,9 +33,7 @@
    20.4  
    20.5  (** concrete syntax **)
    20.6  
    20.7 -nonterminals
    20.8 -  lift
    20.9 -  liftargs
   20.10 +nonterminal lift and liftargs
   20.11  
   20.12  syntax
   20.13    ""            :: "id => lift"                          ("_")
    21.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Dec 17 17:08:56 2010 +0100
    21.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Dec 17 17:43:54 2010 +0100
    21.3 @@ -119,8 +119,9 @@
    21.4        >> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)));
    21.5  
    21.6  val _ =
    21.7 -  Outer_Syntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
    21.8 -    Keyword.thy_decl (Scan.repeat1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
    21.9 +  Outer_Syntax.command "nonterminal"
   21.10 +    "declare syntactic type constructors (grammar nonterminal symbols)" Keyword.thy_decl
   21.11 +    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
   21.12  
   21.13  val _ =
   21.14    Outer_Syntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
    22.1 --- a/src/Sequents/Sequents.thy	Fri Dec 17 17:08:56 2010 +0100
    22.2 +++ b/src/Sequents/Sequents.thy	Fri Dec 17 17:43:54 2010 +0100
    22.3 @@ -28,9 +28,7 @@
    22.4  
    22.5  (* concrete syntax *)
    22.6  
    22.7 -nonterminals
    22.8 -  seq seqobj seqcont
    22.9 -
   22.10 +nonterminal seq and seqobj and seqcont
   22.11  
   22.12  syntax
   22.13   "_SeqEmp"         :: seq                                  ("")
    23.1 --- a/src/ZF/ZF.thy	Fri Dec 17 17:08:56 2010 +0100
    23.2 +++ b/src/ZF/ZF.thy	Fri Dec 17 17:43:54 2010 +0100
    23.3 @@ -102,7 +102,7 @@
    23.4    where "A -> B == Pi(A, %_. B)"
    23.5  
    23.6  
    23.7 -nonterminals "is" patterns
    23.8 +nonterminal "is" and patterns
    23.9  
   23.10  syntax
   23.11    ""          :: "i => is"                   ("_")
    24.1 --- a/src/ZF/func.thy	Fri Dec 17 17:08:56 2010 +0100
    24.2 +++ b/src/ZF/func.thy	Fri Dec 17 17:43:54 2010 +0100
    24.3 @@ -445,8 +445,7 @@
    24.4    update  :: "[i,i,i] => i"  where
    24.5     "update(f,a,b) == lam x: cons(a, domain(f)). if(x=a, b, f`x)"
    24.6  
    24.7 -nonterminals
    24.8 -  updbinds  updbind
    24.9 +nonterminal updbinds and updbind
   24.10  
   24.11  syntax
   24.12