| changeset 35724 | 178ad68f93ed |
| parent 35301 | 90e42f9ba4d1 |
| child 36008 | 23dfa8678c7c |
| 35723:b6cf98f25c3f | 35724:178ad68f93ed |
|---|---|
41 lemmas mult_left_idem = times.left_idem |
41 lemmas mult_left_idem = times.left_idem |
42 |
42 |
43 end |
43 end |
44 |
44 |
45 |
45 |
46 subsection {* Conrete lattices *} |
46 subsection {* Concrete lattices *} |
47 |
47 |
48 notation |
48 notation |
49 less_eq (infix "\<sqsubseteq>" 50) and |
49 less_eq (infix "\<sqsubseteq>" 50) and |
50 less (infix "\<sqsubset>" 50) and |
50 less (infix "\<sqsubset>" 50) and |
51 top ("\<top>") and |
51 top ("\<top>") and |