changeset 6027 | 9dd06eeda95c |
parent 5786 | 9a2c90bdadfe |
child 6289 | 062aa156a300 |
--- a/src/HOL/HOL.thy Fri Dec 11 17:16:23 1998 +0100 +++ b/src/HOL/HOL.thy Fri Dec 11 18:56:30 1998 +0100 @@ -141,6 +141,8 @@ "*Ex1" :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10) +syntax (xsymbols) + "op -->" :: [bool, bool] => bool (infixr "\\<longrightarrow>" 25) (** Rules and definitions **)