equal
deleted
inserted
replaced
214 end |
214 end |
215 |
215 |
216 fun lexicographic_order_tac quiet ctxt = |
216 fun lexicographic_order_tac quiet ctxt = |
217 TRY (Function_Common.apply_termination_rule ctxt 1) THEN |
217 TRY (Function_Common.apply_termination_rule ctxt 1) THEN |
218 lex_order_tac quiet ctxt |
218 lex_order_tac quiet ctxt |
219 (auto_tac |
219 (auto_tac (map_simpset (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt)) |
220 (map_simpset_local (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt)) |
|
221 |
220 |
222 val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false |
221 val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false |
223 |
222 |
224 val setup = |
223 val setup = |
225 Method.setup @{binding lexicographic_order} |
224 Method.setup @{binding lexicographic_order} |