equal
deleted
inserted
replaced
12 |
12 |
13 theory Perm imports func begin |
13 theory Perm imports func begin |
14 |
14 |
15 definition |
15 definition |
16 (*composition of relations and functions; NOT Suppes's relative product*) |
16 (*composition of relations and functions; NOT Suppes's relative product*) |
17 comp :: "[i,i]=>i" (infixr "O" 60) where |
17 comp :: "[i,i]=>i" (infixr \<open>O\<close> 60) where |
18 "r O s == {xz \<in> domain(s)*range(r) . |
18 "r O s == {xz \<in> domain(s)*range(r) . |
19 \<exists>x y z. xz=<x,z> & <x,y>:s & <y,z>:r}" |
19 \<exists>x y z. xz=<x,z> & <x,y>:s & <y,z>:r}" |
20 |
20 |
21 definition |
21 definition |
22 (*the identity function for A*) |
22 (*the identity function for A*) |