equal
deleted
inserted
replaced
11 *) |
11 *) |
12 |
12 |
13 WF_Rel = Finite + |
13 WF_Rel = Finite + |
14 |
14 |
15 (* actually belongs to Finite.thy *) |
15 (* actually belongs to Finite.thy *) |
16 instance "*" :: (finite,finite) finite (finite_Prod) |
16 instance unit :: finite (finite_unit) |
|
17 instance "*" :: (finite,finite) finite (finite_Prod) |
|
18 |
17 |
19 |
18 consts |
20 consts |
19 less_than :: "(nat*nat)set" |
21 less_than :: "(nat*nat)set" |
20 inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set" |
22 inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set" |
21 measure :: "('a => nat) => ('a * 'a)set" |
23 measure :: "('a => nat) => ('a * 'a)set" |