equal
deleted
inserted
replaced
210 end |
210 end |
211 |
211 |
212 fun lexicographic_order_tac quiet ctxt = |
212 fun lexicographic_order_tac quiet ctxt = |
213 TRY (Function_Common.apply_termination_rule ctxt 1) THEN |
213 TRY (Function_Common.apply_termination_rule ctxt 1) THEN |
214 lex_order_tac quiet ctxt |
214 lex_order_tac quiet ctxt |
215 (auto_tac (map_simpset (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt)) |
215 (auto_tac (ctxt addsimps Function_Common.Termination_Simps.get ctxt)) |
216 |
216 |
217 val setup = |
217 val setup = |
218 Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false)) |
218 Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false)) |
219 |
219 |
220 end; |
220 end; |