src/HOL/Hoare_Parallel/OG_Syntax.thy
changeset 41229 d797baa3d57c
parent 35145 f132a4fd8679
child 42086 74bf78db0d87
--- 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)