changeset 35109 | 0015a0a99ae9 |
parent 33955 | fff6f11b1f09 |
child 37139 | e0bd5934a2fb |
--- a/src/HOL/Modelcheck/MuckeSyn.thy Thu Feb 11 21:31:50 2010 +0100 +++ b/src/HOL/Modelcheck/MuckeSyn.thy Thu Feb 11 21:33:25 2010 +0100 @@ -38,7 +38,7 @@ "_idts" :: "[idt, idts] => idts" ("_,/ _" [1, 0] 0) "_tuple" :: "'a => tuple_args => 'a * 'b" ("(1_,/ _)") -(* "@pttrn" :: "[pttrn, pttrns] => pttrn" ("_,/ _" [1, 0] 0) +(* "_pttrn" :: "[pttrn, pttrns] => pttrn" ("_,/ _" [1, 0] 0) "_pattern" :: "[pttrn, patterns] => pttrn" ("_,/ _" [1, 0] 0) *) "_decl" :: "[mutype,pttrn] => decl" ("_ _")