syntax (symbols) "op o" moved from HOL to Fun;
authorwenzelm
Sun Jul 16 20:48:35 2000 +0200 (2000-07-16)
changeset 9352416b2ecd97a1
parent 9351 5d53e3f35152
child 9353 93cd32adc402
syntax (symbols) "op o" moved from HOL to Fun;
src/HOL/Fun.thy
src/HOL/HOL.thy
     1.1 --- a/src/HOL/Fun.thy	Sun Jul 16 20:47:45 2000 +0200
     1.2 +++ b/src/HOL/Fun.thy	Sun Jul 16 20:48:35 2000 +0200
     1.3 @@ -49,6 +49,9 @@
     1.4    inj_on :: ['a => 'b, 'a set] => bool
     1.5      "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
     1.6  
     1.7 +syntax (symbols)
     1.8 +  "op o"        :: "['b => 'c, 'a => 'b, 'a] => 'c"      (infixl "\\<circ>" 55)
     1.9 +
    1.10  syntax
    1.11    inj   :: ('a => 'b) => bool                   (*injective*)
    1.12  
     2.1 --- a/src/HOL/HOL.thy	Sun Jul 16 20:47:45 2000 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sun Jul 16 20:48:35 2000 +0200
     2.3 @@ -113,7 +113,6 @@
     2.4    "op &"        :: "[bool, bool] => bool"                (infixr "\\<and>" 35)
     2.5    "op |"        :: "[bool, bool] => bool"                (infixr "\\<or>" 30)
     2.6    "op -->"      :: "[bool, bool] => bool"                (infixr "\\<midarrow>\\<rightarrow>" 25)
     2.7 -  "op o"        :: "['b => 'c, 'a => 'b, 'a] => 'c"      (infixl "\\<circ>" 55)
     2.8    "op ~="       :: "['a, 'a] => bool"                    (infixl "\\<noteq>" 50)
     2.9    "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
    2.10    "ALL "        :: "[idts, bool] => bool"                ("(3\\<forall>_./ _)" [0, 10] 10)