# HG changeset patch # User wenzelm # Date 1292604234 -3600 # Node ID d797baa3d57ca15a58e81c9d8158778f0341e7a7 # Parent e1fce873b814ee7d12413440d5fb08cc311c6afe replaced command 'nonterminals' by slightly modernized version 'nonterminal'; diff -r e1fce873b814 -r d797baa3d57c NEWS --- 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. diff -r e1fce873b814 -r d797baa3d57c doc-src/IsarRef/Thy/Inner_Syntax.thy --- 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 \ theory"} \\ + @{command_def "nonterminal"} & : & @{text "theory \ theory"} \\ @{command_def "syntax"} & : & @{text "theory \ theory"} \\ @{command_def "no_syntax"} & : & @{text "theory \ theory"} \\ @{command_def "translations"} & : & @{text "theory \ 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. diff -r e1fce873b814 -r d797baa3d57c doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- 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. diff -r e1fce873b814 -r d797baa3d57c etc/isar-keywords-ZF.el --- 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" diff -r e1fce873b814 -r d797baa3d57c etc/isar-keywords.el --- 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" diff -r e1fce873b814 -r d797baa3d57c src/Cube/Cube.thy --- 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" diff -r e1fce873b814 -r d797baa3d57c src/FOL/IFOL.thy --- 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)" diff -r e1fce873b814 -r d797baa3d57c src/HOL/Fun.thy --- 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" ("_") diff -r e1fce873b814 -r d797baa3d57c src/HOL/HOL.thy --- 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 "\" 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) diff -r e1fce873b814 -r d797baa3d57c src/HOL/HOLCF/ex/Letrec.thy --- 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 \ 'a \ 'b) \ 'b" where "CLetrec = (\ F. snd (F\(\ x. fst (F\x))))" -nonterminals - recbinds recbindt recbind +nonterminal recbinds and recbindt and recbind syntax "_recbind" :: "['a, 'a] \ recbind" ("(2_ =/ _)" 10) diff -r e1fce873b814 -r d797baa3d57c src/HOL/HOLCF/ex/Pattern_Match.thy --- 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) diff -r e1fce873b814 -r d797baa3d57c src/HOL/Hoare_Parallel/OG_Syntax.thy --- 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 \c\" \ "r AWAIT CONST True THEN c END" "r WAIT b END" \ "r AWAIT b THEN SKIP END" -nonterminals - prgs +nonterminal prgs syntax "_PAR" :: "prgs \ 'a" ("COBEGIN//_//COEND" [57] 56) diff -r e1fce873b814 -r d797baa3d57c src/HOL/Hoare_Parallel/RG_Syntax.thy --- 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 @@ "\c\" \ "AWAIT CONST True THEN c END" "WAIT b END" \ "AWAIT b THEN SKIP END" -nonterminals - prgs +nonterminal prgs syntax "_PAR" :: "prgs \ 'a" ("COBEGIN//_//COEND" 60) diff -r e1fce873b814 -r d797baa3d57c src/HOL/Library/Monad_Syntax.thy --- 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 "\" 54) -nonterminals - do_binds do_bind +nonterminal do_binds and do_bind syntax "_do_block" :: "do_binds \ 'a" ("do {//(2 _)//}" [12] 62) diff -r e1fce873b814 -r d797baa3d57c src/HOL/Library/State_Monad.thy --- 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 \ 'a" ("exec {//(2 _)//}" [12] 62) diff -r e1fce873b814 -r d797baa3d57c src/HOL/List.thy --- 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 \ v # xs | Suc j \ 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 \ z = f x y}"}. *) -nonterminals lc_qual lc_quals +nonterminal lc_qual and lc_quals syntax "_listcompr" :: "'a \ lc_qual \ lc_quals \ 'a list" ("[_ . __") diff -r e1fce873b814 -r d797baa3d57c src/HOL/Map.thy --- 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 "\\<^sub>m" 50) where "(m\<^isub>1 \\<^sub>m m\<^isub>2) = (\a \ dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a)" -nonterminals - maplets maplet +nonterminal maplets and maplet syntax "_maplet" :: "['a, 'a] => maplet" ("_ /|->/ _") diff -r e1fce873b814 -r d797baa3d57c src/HOL/Product_Type.thy --- 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'(_,/ _'))") diff -r e1fce873b814 -r d797baa3d57c src/HOL/Record.thy --- 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" ("_") diff -r e1fce873b814 -r d797baa3d57c src/HOL/TLA/Intensional.thy --- 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" ("_") diff -r e1fce873b814 -r d797baa3d57c src/Pure/Isar/isar_syn.ML --- 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 diff -r e1fce873b814 -r d797baa3d57c src/Sequents/Sequents.thy --- 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 ("") diff -r e1fce873b814 -r d797baa3d57c src/ZF/ZF.thy --- 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" ("_") diff -r e1fce873b814 -r d797baa3d57c src/ZF/func.thy --- 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