equal
deleted
inserted
replaced
9 -- Lemmas for the Schroeder-Bernstein Theorem |
9 -- Lemmas for the Schroeder-Bernstein Theorem |
10 *) |
10 *) |
11 |
11 |
12 header{*Injections, Surjections, Bijections, Composition*} |
12 header{*Injections, Surjections, Bijections, Composition*} |
13 |
13 |
14 theory Perm = func: |
14 theory Perm imports func begin |
15 |
15 |
16 constdefs |
16 constdefs |
17 |
17 |
18 (*composition of relations and functions; NOT Suppes's relative product*) |
18 (*composition of relations and functions; NOT Suppes's relative product*) |
19 comp :: "[i,i]=>i" (infixr "O" 60) |
19 comp :: "[i,i]=>i" (infixr "O" 60) |