equal
deleted
inserted
replaced
12 |
12 |
13 constdefs |
13 constdefs |
14 |
14 |
15 (*MOVE TO RELATION.THY??*) |
15 (*MOVE TO RELATION.THY??*) |
16 Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set" |
16 Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set" |
17 "Restrict A r == r Int (A Times UNIV)" |
17 "Restrict A r == r Int (A <*> UNIV)" |
18 |
18 |
19 lessThan :: "nat => nat set" |
19 lessThan :: "nat => nat set" |
20 "lessThan n == {i. i<n}" |
20 "lessThan n == {i. i<n}" |
21 |
21 |
22 atMost :: "nat => nat set" |
22 atMost :: "nat => nat set" |