equal
deleted
inserted
replaced
54 in |
54 in |
55 |
55 |
56 (*** Term order for commutative rings ***) |
56 (*** Term order for commutative rings ***) |
57 |
57 |
58 fun ring_ord a = |
58 fun ring_ord a = |
59 find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "Cring.ring.a_inv", |
59 find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv", |
60 "CRing.ring.minus", "Group.monoid.one", "Group.semigroup.mult"]; |
60 "CRing.minus", "Group.monoid.one", "Group.semigroup.mult"]; |
61 |
61 |
62 fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS); |
62 fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS); |
63 |
63 |
64 val cring_ss = HOL_ss settermless termless_ring; |
64 val cring_ss = HOL_ss settermless termless_ring; |
65 |
65 |