equal
deleted
inserted
replaced
9 |
9 |
10 |
10 |
11 (* linear orders are lattices *) |
11 (* linear orders are lattices *) |
12 |
12 |
13 instance |
13 instance |
14 lin_order < lattice (allI, exI, min_is_inf, max_is_sup) |
14 linear_order < lattice (allI, exI, min_is_inf, max_is_sup) |
15 |
15 |
16 |
16 |
17 (* complete lattices are lattices *) |
17 (* complete lattices are lattices *) |
18 |
18 |
19 instance |
19 instance |
34 instance |
34 instance |
35 dual :: (lattice) lattice (allI, exI, dual_is_inf, dual_is_sup) |
35 dual :: (lattice) lattice (allI, exI, dual_is_inf, dual_is_sup) |
36 |
36 |
37 (*FIXME bug workaround (see also OrdInsts.thy)*) |
37 (*FIXME bug workaround (see also OrdInsts.thy)*) |
38 instance |
38 instance |
39 dual :: (lin_order) lin_order (le_dual_lin) |
39 dual :: (linear_order) linear_order (le_dual_linear) |
40 |
40 |
41 end |
41 end |