equal
deleted
inserted
replaced
138 | ord => ord) |
138 | ord => ord) |
139 and hd_ord (f, g) = (* ~ term.ML *) |
139 and hd_ord (f, g) = (* ~ term.ML *) |
140 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord |
140 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord |
141 (dest_hd' f, dest_hd' g) |
141 (dest_hd' f, dest_hd' g) |
142 and terms_ord str pr (ts, us) = |
142 and terms_ord str pr (ts, us) = |
143 list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us); |
143 list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us); |
144 |
144 |
145 in |
145 in |
146 (* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses |
146 (* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses |
147 by (1) size_of_term: less(!) to right, size_of 'sqrt (...)' = 1 |
147 by (1) size_of_term: less(!) to right, size_of 'sqrt (...)' = 1 |
148 (2) hd_ord: greater to right, 'sqrt' < numerals < variables |
148 (2) hd_ord: greater to right, 'sqrt' < numerals < variables |