--- a/NEWS Fri Dec 17 17:08:56 2010 +0100
+++ b/NEWS Fri Dec 17 17:43:54 2010 +0100
@@ -83,6 +83,10 @@
*** Pure ***
+* Replaced command 'nonterminals' by slightly modernized version
+'nonterminal' (with 'and' separated list of arguments).
+INCOMPATIBILITY.
+
* Command 'notepad' replaces former 'example_proof' for
experimentation in Isar without any result. INCOMPATIBILITY.
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Dec 17 17:43:54 2010 +0100
@@ -723,7 +723,7 @@
text {*
\begin{matharray}{rcl}
- @{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "nonterminal"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\
@@ -731,7 +731,7 @@
\end{matharray}
\begin{rail}
- 'nonterminals' (name +)
+ 'nonterminal' (name + 'and')
;
('syntax' | 'no_syntax') mode? (constdecl +)
;
@@ -746,7 +746,7 @@
\begin{description}
- \item @{command "nonterminals"}~@{text c} declares a type
+ \item @{command "nonterminal"}~@{text c} declares a type
constructor @{text c} (without arguments) to act as purely syntactic
type: a nonterminal symbol of the inner syntax.
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Dec 17 17:08:56 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Dec 17 17:43:54 2010 +0100
@@ -742,7 +742,7 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \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}}} \\
+ \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}}} \\
\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}}} \\
\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}}} \\
\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}}} \\
@@ -750,7 +750,7 @@
\end{matharray}
\begin{rail}
- 'nonterminals' (name +)
+ 'nonterminal' (name + 'and')
;
('syntax' | 'no_syntax') mode? (constdecl +)
;
@@ -765,7 +765,7 @@
\begin{description}
- \item \hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c} declares a type
+ \item \hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}~\isa{c} declares a type
constructor \isa{c} (without arguments) to act as purely syntactic
type: a nonterminal symbol of the inner syntax.
--- a/etc/isar-keywords-ZF.el Fri Dec 17 17:08:56 2010 +0100
+++ b/etc/isar-keywords-ZF.el Fri Dec 17 17:43:54 2010 +0100
@@ -103,7 +103,7 @@
"no_syntax"
"no_translations"
"no_type_notation"
- "nonterminals"
+ "nonterminal"
"notation"
"note"
"notepad"
@@ -381,7 +381,7 @@
"no_syntax"
"no_translations"
"no_type_notation"
- "nonterminals"
+ "nonterminal"
"notation"
"notepad"
"oracle"
--- a/etc/isar-keywords.el Fri Dec 17 17:08:56 2010 +0100
+++ b/etc/isar-keywords.el Fri Dec 17 17:43:54 2010 +0100
@@ -140,7 +140,7 @@
"nominal_inductive"
"nominal_inductive2"
"nominal_primrec"
- "nonterminals"
+ "nonterminal"
"notation"
"note"
"notepad"
@@ -487,7 +487,7 @@
"no_translations"
"no_type_notation"
"nominal_datatype"
- "nonterminals"
+ "nonterminal"
"notation"
"notepad"
"oracle"
--- a/src/Cube/Cube.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/Cube/Cube.thy Fri Dec 17 17:43:54 2010 +0100
@@ -14,8 +14,7 @@
typedecl "context"
typedecl typing
-nonterminals
- context' typing'
+nonterminal context' and typing'
consts
Abs :: "[term, term => term] => term"
--- a/src/FOL/IFOL.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/FOL/IFOL.thy Fri Dec 17 17:43:54 2010 +0100
@@ -754,7 +754,7 @@
subsection {* ``Let'' declarations *}
-nonterminals letbinds letbind
+nonterminal letbinds and letbind
definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where
"Let(s, f) == f(s)"
--- a/src/HOL/Fun.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/Fun.thy Fri Dec 17 17:43:54 2010 +0100
@@ -558,8 +558,8 @@
fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
"fun_upd f a b == % x. if x=a then b else f x"
-nonterminals
- updbinds updbind
+nonterminal updbinds and updbind
+
syntax
"_updbind" :: "['a, 'a] => updbind" ("(2_ :=/ _)")
"" :: "updbind => updbinds" ("_")
--- a/src/HOL/HOL.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/HOL.thy Fri Dec 17 17:43:54 2010 +0100
@@ -103,9 +103,8 @@
notation (xsymbols)
iff (infixr "\<longleftrightarrow>" 25)
-nonterminals
- letbinds letbind
- case_syn cases_syn
+nonterminal letbinds and letbind
+nonterminal case_syn and cases_syn
syntax
"_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10)
--- a/src/HOL/HOLCF/ex/Letrec.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/HOLCF/ex/Letrec.thy Fri Dec 17 17:43:54 2010 +0100
@@ -14,8 +14,7 @@
CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
"CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
-nonterminals
- recbinds recbindt recbind
+nonterminal recbinds and recbindt and recbind
syntax
"_recbind" :: "['a, 'a] \<Rightarrow> recbind" ("(2_ =/ _)" 10)
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Dec 17 17:43:54 2010 +0100
@@ -100,8 +100,7 @@
subsection {* Case syntax *}
-nonterminals
- Case_syn Cases_syn
+nonterminal Case_syn and Cases_syn
syntax
"_Case_syntax":: "['a, Cases_syn] => 'b" ("(Case _ of/ _)" 10)
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Fri Dec 17 17:43:54 2010 +0100
@@ -56,8 +56,7 @@
"r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT CONST True THEN c END"
"r WAIT b END" \<rightleftharpoons> "r AWAIT b THEN SKIP END"
-nonterminals
- prgs
+nonterminal prgs
syntax
"_PAR" :: "prgs \<Rightarrow> 'a" ("COBEGIN//_//COEND" [57] 56)
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Fri Dec 17 17:43:54 2010 +0100
@@ -27,8 +27,7 @@
"\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT CONST True THEN c END"
"WAIT b END" \<rightleftharpoons> "AWAIT b THEN SKIP END"
-nonterminals
- prgs
+nonterminal prgs
syntax
"_PAR" :: "prgs \<Rightarrow> 'a" ("COBEGIN//_//COEND" 60)
--- a/src/HOL/Library/Monad_Syntax.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy Fri Dec 17 17:43:54 2010 +0100
@@ -37,8 +37,7 @@
notation (latex output)
bind_do (infixr "\<bind>" 54)
-nonterminals
- do_binds do_bind
+nonterminal do_binds and do_bind
syntax
"_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2 _)//}" [12] 62)
--- a/src/HOL/Library/State_Monad.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/Library/State_Monad.thy Fri Dec 17 17:43:54 2010 +0100
@@ -114,8 +114,7 @@
subsection {* Do-syntax *}
-nonterminals
- sdo_binds sdo_bind
+nonterminal sdo_binds and sdo_bind
syntax
"_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2 _)//}" [12] 62)
--- a/src/HOL/List.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/List.thy Fri Dec 17 17:43:54 2010 +0100
@@ -123,7 +123,7 @@
"list_update [] i v = []"
| "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
-nonterminals lupdbinds lupdbind
+nonterminal lupdbinds and lupdbind
syntax
"_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)")
@@ -346,7 +346,7 @@
@{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
*)
-nonterminals lc_qual lc_quals
+nonterminal lc_qual and lc_quals
syntax
"_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __")
--- a/src/HOL/Map.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/Map.thy Fri Dec 17 17:43:54 2010 +0100
@@ -50,8 +50,7 @@
map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50) where
"(m\<^isub>1 \<subseteq>\<^sub>m m\<^isub>2) = (\<forall>a \<in> dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a)"
-nonterminals
- maplets maplet
+nonterminal maplets and maplet
syntax
"_maplet" :: "['a, 'a] => maplet" ("_ /|->/ _")
--- a/src/HOL/Product_Type.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/Product_Type.thy Fri Dec 17 17:43:54 2010 +0100
@@ -173,8 +173,7 @@
abstractions.
*}
-nonterminals
- tuple_args patterns
+nonterminal tuple_args and patterns
syntax
"_tuple" :: "'a => tuple_args => 'a * 'b" ("(1'(_,/ _'))")
--- a/src/HOL/Record.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/Record.thy Fri Dec 17 17:43:54 2010 +0100
@@ -419,8 +419,15 @@
subsection {* Concrete record syntax *}
-nonterminals
- ident field_type field_types field fields field_update field_updates
+nonterminal
+ ident and
+ field_type and
+ field_types and
+ field and
+ fields and
+ field_update and
+ field_updates
+
syntax
"_constify" :: "id => ident" ("_")
"_constify" :: "longid => ident" ("_")
--- a/src/HOL/TLA/Intensional.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/HOL/TLA/Intensional.thy Fri Dec 17 17:43:54 2010 +0100
@@ -33,9 +33,7 @@
(** concrete syntax **)
-nonterminals
- lift
- liftargs
+nonterminal lift and liftargs
syntax
"" :: "id => lift" ("_")
--- a/src/Pure/Isar/isar_syn.ML Fri Dec 17 17:08:56 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Fri Dec 17 17:43:54 2010 +0100
@@ -119,8 +119,9 @@
>> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)));
val _ =
- Outer_Syntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
- Keyword.thy_decl (Scan.repeat1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
+ Outer_Syntax.command "nonterminal"
+ "declare syntactic type constructors (grammar nonterminal symbols)" Keyword.thy_decl
+ (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
val _ =
Outer_Syntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
--- a/src/Sequents/Sequents.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/Sequents/Sequents.thy Fri Dec 17 17:43:54 2010 +0100
@@ -28,9 +28,7 @@
(* concrete syntax *)
-nonterminals
- seq seqobj seqcont
-
+nonterminal seq and seqobj and seqcont
syntax
"_SeqEmp" :: seq ("")
--- a/src/ZF/ZF.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/ZF/ZF.thy Fri Dec 17 17:43:54 2010 +0100
@@ -102,7 +102,7 @@
where "A -> B == Pi(A, %_. B)"
-nonterminals "is" patterns
+nonterminal "is" and patterns
syntax
"" :: "i => is" ("_")
--- a/src/ZF/func.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/ZF/func.thy Fri Dec 17 17:43:54 2010 +0100
@@ -445,8 +445,7 @@
update :: "[i,i,i] => i" where
"update(f,a,b) == lam x: cons(a, domain(f)). if(x=a, b, f`x)"
-nonterminals
- updbinds updbind
+nonterminal updbinds and updbind
syntax