src/HOL/Tools/function_package/lexicographic_order.ML
changeset 28287 c86fa4e0aedb
parent 27790 37b4e65d1dbf
child 29713 55c30d1117ef
equal deleted inserted replaced
28286:bed3865290b4 28287:c86fa4e0aedb
   217     Method.SIMPLE_METHOD (TRY (FundefCommon.apply_termination_rule ctxt 1)
   217     Method.SIMPLE_METHOD (TRY (FundefCommon.apply_termination_rule ctxt 1)
   218                           THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt)))
   218                           THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt)))
   219 
   219 
   220 val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
   220 val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
   221                                  "termination prover for lexicographic orderings")]
   221                                  "termination prover for lexicographic orderings")]
       
   222      #> Context.theory_map (FundefCommon.set_termination_prover (lexicographic_order []))
   222 
   223 
   223 end
   224 end