author | huffman |
Mon, 07 Nov 2005 19:23:53 +0100 | |
changeset 18110 | 08ec4f1f116d |
parent 18109 | 94b528311e22 |
child 18111 | 2b56f74fd605 |
--- a/src/HOLCF/Fixrec.thy Mon Nov 07 19:03:02 2005 +0100 +++ b/src/HOLCF/Fixrec.thy Mon Nov 07 19:23:53 2005 +0100 @@ -171,7 +171,7 @@ "_Case1" :: "['a, 'b] => Case_syn" ("(2_ =>/ _)" 10) "" :: "Case_syn => Cases_syn" ("_") "_Case2" :: "[Case_syn, Cases_syn] => Cases_syn" ("_/ | _") - "_as_pattern" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "as" 10) + "_as_pattern" :: "[idt, 'a] \<Rightarrow> 'a" (* infixr "as" 10 *) syntax (xsymbols) "_Case1" :: "['a, 'b] => Case_syn" ("(2_ \<Rightarrow>/ _)" 10)