src/HOL/Fun.thy
changeset 9352 416b2ecd97a1
parent 9340 9666f78ecfab
child 10212 33fe2d701ddd
     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