equal
deleted
inserted
replaced
9 *) |
9 *) |
10 |
10 |
11 Extend = Guar + |
11 Extend = Guar + |
12 |
12 |
13 constdefs |
13 constdefs |
|
14 |
|
15 (*MOVE to Relation.thy?*) |
|
16 Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set" |
|
17 "Restrict A r == r Int (A <*> UNIV)" |
14 |
18 |
15 good_map :: "['a*'b => 'c] => bool" |
19 good_map :: "['a*'b => 'c] => bool" |
16 "good_map h == surj h & (ALL x y. fst (inv h (h (x,y))) = x)" |
20 "good_map h == surj h & (ALL x y. fst (inv h (h (x,y))) = x)" |
17 (*Using the locale constant "f", this is f (h (x,y))) = x*) |
21 (*Using the locale constant "f", this is f (h (x,y))) = x*) |
18 |
22 |