src/HOL/HOL.thy
changeset 5305 513925de8962
parent 5186 439e292b5b87
child 5492 d9fc3457554e
     1.1 --- a/src/HOL/HOL.thy	Wed Aug 12 16:21:18 1998 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Aug 12 16:23:25 1998 +0200
     1.3 @@ -47,7 +47,6 @@
     1.4  
     1.5    (* Infixes *)
     1.6  
     1.7 -  o             :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
     1.8    "="           :: ['a, 'a] => bool                 (infixl 50)
     1.9    "&"           :: [bool, bool] => bool             (infixr 35)
    1.10    "|"           :: [bool, bool] => bool             (infixr 30)
    1.11 @@ -180,7 +179,6 @@
    1.12  defs
    1.13    (*misc definitions*)
    1.14    Let_def       "Let s f == f(s)"
    1.15 -  o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
    1.16    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
    1.17  
    1.18    (*arbitrary is completely unspecified, but is made to appear as a