changeset 12633 | ad9277743664 |
parent 12436 | a2df07fefed7 |
child 12650 | fbc17f1e746b |
--- a/src/HOL/HOL.thy Fri Jan 04 19:28:57 2002 +0100 +++ b/src/HOL/HOL.thy Fri Jan 04 19:29:30 2002 +0100 @@ -75,7 +75,7 @@ "_Let (_binds b bs) e" == "_Let b (_Let bs e)" "let x = a in e" == "Let a (%x. e)" -syntax ("" output) +syntax (output) "=" :: "['a, 'a] => bool" (infix 50) "~=" :: "['a, 'a] => bool" (infix 50)