equal
deleted
inserted
replaced
215 (*** Term order for commutative rings ***) |
215 (*** Term order for commutative rings ***) |
216 |
216 |
217 ML {* |
217 ML {* |
218 fun ring_ord (Const (a, _)) = |
218 fun ring_ord (Const (a, _)) = |
219 find_index (fn a' => a = a') |
219 find_index (fn a' => a = a') |
220 ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus", "HOL.one", "HOL.times"] |
220 [@{const_name HOL.zero}, @{const_name HOL.plus}, @{const_name HOL.uminus}, |
|
221 @{const_name HOL.minus}, @{const_name HOL.one}, @{const_name HOL.times}] |
221 | ring_ord _ = ~1; |
222 | ring_ord _ = ~1; |
222 |
223 |
223 fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS); |
224 fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS); |
224 |
225 |
225 val ring_ss = HOL_basic_ss settermless termless_ring addsimps |
226 val ring_ss = HOL_basic_ss settermless termless_ring addsimps |