src/HOL/Library/bnf_lfp_countable.ML
changeset 58168 6b6c41aa780b
parent 58166 86a374caeb82
child 58170 d84bab7ed89e
equal deleted inserted replaced
58167:08052d9f8050 58168:6b6c41aa780b
    21 open BNF_FP_Util
    21 open BNF_FP_Util
    22 open BNF_FP_Def_Sugar
    22 open BNF_FP_Def_Sugar
    23 
    23 
    24 fun nchotomy_tac nchotomy =
    24 fun nchotomy_tac nchotomy =
    25   HEADGOAL (rtac (nchotomy RS @{thm all_reg[rotated]}) THEN'
    25   HEADGOAL (rtac (nchotomy RS @{thm all_reg[rotated]}) THEN'
    26     REPEAT_ALL_NEW (match_tac [allI, impI]) THEN' REPEAT_ALL_NEW (ematch_tac [exE, disjE]));
    26     REPEAT_ALL_NEW (resolve_tac [allI, impI] ORELSE' eresolve_tac [exE, disjE]));
    27 
    27 
    28 fun meta_spec_mp_tac 0 = K all_tac
    28 fun meta_spec_mp_tac 0 = K all_tac
    29   | meta_spec_mp_tac depth =
    29   | meta_spec_mp_tac depth =
    30     dtac meta_spec THEN' meta_spec_mp_tac (depth - 1) THEN' dtac meta_mp THEN' atac;
    30     dtac meta_spec THEN' meta_spec_mp_tac (depth - 1) THEN' dtac meta_mp THEN' atac;
    31 
    31