| changeset 39272 | 0b61951d2682 |
| parent 39159 | 0dec18004e75 |
| child 39331 | 8b1969d603c0 |
--- a/src/HOL/HOL.thy Fri Sep 10 09:56:28 2010 +0200 +++ b/src/HOL/HOL.thy Fri Sep 10 10:21:25 2010 +0200 @@ -1942,10 +1942,10 @@ (Haskell "Eq") code_const "HOL.equal" - (Haskell infixl 4 "==") + (Haskell infix 4 "==") code_const HOL.eq - (Haskell infixl 4 "==") + (Haskell infix 4 "==") text {* undefined *}