equal
deleted
inserted
replaced
49 |
49 |
50 text{*compatibility*} |
50 text{*compatibility*} |
51 lemmas o_def = comp_def |
51 lemmas o_def = comp_def |
52 |
52 |
53 syntax (xsymbols) |
53 syntax (xsymbols) |
|
54 comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\<circ>" 55) |
|
55 syntax (HTML output) |
54 comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\<circ>" 55) |
56 comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\<circ>" 55) |
55 |
57 |
56 |
58 |
57 constdefs |
59 constdefs |
58 inj_on :: "['a => 'b, 'a set] => bool" (*injective*) |
60 inj_on :: "['a => 'b, 'a set] => bool" (*injective*) |