src/HOL/Modelcheck/MuckeSyn.thy
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"             ("_ _")