| 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)