equal
deleted
inserted
replaced
8 The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a |
8 The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a |
9 subset of the lexicographic product, and therefore does not need to be defined |
9 subset of the lexicographic product, and therefore does not need to be defined |
10 separately. |
10 separately. |
11 *) |
11 *) |
12 |
12 |
13 Wellfounded_Relations = Finite + Hilbert_Choice + |
13 Wellfounded_Relations = Finite + |
14 |
14 |
15 (* logically belongs in Finite.thy, but the theorems are proved in Finite.ML *) |
15 (* logically belongs in Finite.thy, but the theorems are proved in Finite.ML *) |
16 instance unit :: finite (finite_unit) |
16 instance unit :: finite (finite_unit) |
17 instance "*" :: (finite,finite) finite (finite_Prod) |
17 instance "*" :: (finite,finite) finite (finite_Prod) |
18 |
18 |