equal
deleted
inserted
replaced
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 |