src/HOL/Tools/function_package/auto_term.ML
changeset 25545 21cd20c1ce98
parent 22733 0b14bb35be90
child 30510 4120fc59dd85
equal deleted inserted replaced
25544:437251bbc5ce 25545:21cd20c1ce98
    24     in 
    24     in 
    25       Drule.cterm_instantiate [(Rvar, rel')] st' 
    25       Drule.cterm_instantiate [(Rvar, rel')] st' 
    26     end
    26     end
    27 
    27 
    28 fun relation_tac ctxt rel i = 
    28 fun relation_tac ctxt rel i = 
    29     FundefCommon.apply_termination_rule ctxt i 
    29     TRY (FundefCommon.apply_termination_rule ctxt i)
    30     THEN PRIMITIVE (inst_thm ctxt rel)
    30     THEN PRIMITIVE (inst_thm ctxt rel)
    31 
    31 
    32 val setup = Method.add_methods
    32 val setup = Method.add_methods
    33   [("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
    33   [("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
    34     "proves termination using a user-specified wellfounded relation")]
    34     "proves termination using a user-specified wellfounded relation")]