src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
changeset 53926 9fc9a59ad579
parent 53922 6d40f6e69686
child 53929 8c5aaf557421
equal deleted inserted replaced
53925:9008c4806198 53926:9fc9a59ad579
    38   HEADGOAL (rtac refl);
    38   HEADGOAL (rtac refl);
    39 
    39 
    40 fun mk_primcorec_assumption_tac ctxt discIs =
    40 fun mk_primcorec_assumption_tac ctxt discIs =
    41   HEADGOAL (SELECT_GOAL (unfold_thms_tac ctxt
    41   HEADGOAL (SELECT_GOAL (unfold_thms_tac ctxt
    42       @{thms not_not not_False_eq_True de_Morgan_conj de_Morgan_disj} THEN
    42       @{thms not_not not_False_eq_True de_Morgan_conj de_Morgan_disj} THEN
    43     SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE'
    43     SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
    44     resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
    44     resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
    45     dresolve_tac discIs THEN' atac)))));
    45     dresolve_tac discIs THEN' atac)))));
    46 
    46 
    47 fun mk_primcorec_same_case_tac m =
    47 fun mk_primcorec_same_case_tac m =
    48   HEADGOAL (if m = 0 then rtac TrueI
    48   HEADGOAL (if m = 0 then rtac TrueI