adapted tuple syntax;
authorwenzelm
Sun, 16 Jul 2000 20:56:53 +0200
changeset 9368 415587dff134
parent 9367 df7a4824111e
child 9369 139fde7af7bd
adapted tuple syntax;
src/HOL/Modelcheck/MuckeSyn.thy
--- 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) *)