src/HOL/Tools/function_package/lexicographic_order.ML
changeset 25545 21cd20c1ce98
parent 25538 58e8ba3b792b
child 26529 03ad378ed5f0
equal deleted inserted replaced
25544:437251bbc5ce 25545:21cd20c1ce98
   321               THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
   321               THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
   322               THEN (rtac @{thm "wf_empty"} 1)
   322               THEN (rtac @{thm "wf_empty"} 1)
   323               THEN EVERY (map prove_row clean_table))
   323               THEN EVERY (map prove_row clean_table))
   324     end
   324     end
   325 
   325 
   326 fun lexicographic_order thms ctxt = Method.SIMPLE_METHOD (FundefCommon.apply_termination_rule ctxt 1
   326 fun lexicographic_order thms ctxt = 
   327                                                          THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt)))
   327     Method.SIMPLE_METHOD (TRY (FundefCommon.apply_termination_rule ctxt 1)
       
   328                           THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt)))
   328 
   329 
   329 val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
   330 val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
   330                                  "termination prover for lexicographic orderings")]
   331                                  "termination prover for lexicographic orderings")]
   331     #> Attrib.add_attributes [("measure_function", add_sfun_attr, "declare custom measure function")]
   332     #> Attrib.add_attributes [("measure_function", add_sfun_attr, "declare custom measure function")]
   332 
   333