author | wenzelm |
Sun, 16 Jul 2000 20:56:53 +0200 | |
changeset 9368 | 415587dff134 |
parent 9367 | df7a4824111e |
child 9369 | 139fde7af7bd |
--- a/src/HOL/Modelcheck/MuckeSyn.thy Sun Jul 16 20:56:32 2000 +0200 +++ b/src/HOL/Modelcheck/MuckeSyn.thy Sun Jul 16 20:56:53 2000 +0200 @@ -39,8 +39,8 @@ "_idts" :: [idt, idts] => idts ("_,/ _" [1, 0] 0) - "@Tuple" :: "['a, args] => 'a * 'b" ("(1_,/ _)") -(* "@pttrn" :: [pttrn, pttrns] => pttrn ("_,/ _" [1, 0] 0) + "_tuple" :: "'a => tuple_args => 'a * 'b" ("(1_,/ _)") +(* "@pttrn" :: [pttrn, pttrns] => pttrn ("_,/ _" [1, 0] 0) "_pattern" :: [pttrn, patterns] => pttrn ("_,/ _" [1, 0] 0) *)