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