src/HOL/HOL.thy
changeset 9352 416b2ecd97a1
parent 9060 b0dd884b1848
child 9488 f11bece4e2db
     1.1 --- a/src/HOL/HOL.thy	Sun Jul 16 20:47:45 2000 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sun Jul 16 20:48:35 2000 +0200
     1.3 @@ -113,7 +113,6 @@
     1.4    "op &"        :: "[bool, bool] => bool"                (infixr "\\<and>" 35)
     1.5    "op |"        :: "[bool, bool] => bool"                (infixr "\\<or>" 30)
     1.6    "op -->"      :: "[bool, bool] => bool"                (infixr "\\<midarrow>\\<rightarrow>" 25)
     1.7 -  "op o"        :: "['b => 'c, 'a => 'b, 'a] => 'c"      (infixl "\\<circ>" 55)
     1.8    "op ~="       :: "['a, 'a] => bool"                    (infixl "\\<noteq>" 50)
     1.9    "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
    1.10    "ALL "        :: "[idts, bool] => bool"                ("(3\\<forall>_./ _)" [0, 10] 10)