src/HOL/Hoare_Parallel/RG_Syntax.thy
changeset 41229 d797baa3d57c
parent 35145 f132a4fd8679
child 42086 74bf78db0d87
     1.1 --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Fri Dec 17 17:08:56 2010 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Fri Dec 17 17:43:54 2010 +0100
     1.3 @@ -27,8 +27,7 @@
     1.4    "\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT CONST True THEN c END"
     1.5    "WAIT b END" \<rightleftharpoons> "AWAIT b THEN SKIP END"
     1.6  
     1.7 -nonterminals
     1.8 -  prgs
     1.9 +nonterminal prgs
    1.10  
    1.11  syntax
    1.12    "_PAR"        :: "prgs \<Rightarrow> 'a"              ("COBEGIN//_//COEND" 60)