equal
deleted
inserted
replaced
53 |
53 |
54 fun distinct_in_prems_tac distincts = |
54 fun distinct_in_prems_tac distincts = |
55 eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac; |
55 eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac; |
56 |
56 |
57 fun mk_primcorec_nchotomy_tac ctxt disc_exhausts = |
57 fun mk_primcorec_nchotomy_tac ctxt disc_exhausts = |
58 HEADGOAL (clean_blast_tac ctxt); |
58 HEADGOAL (Method.insert_tac disc_exhausts THEN' clean_blast_tac ctxt); |
59 |
59 |
60 fun mk_primcorec_exhaust_tac ctxt frees n nchotomy = |
60 fun mk_primcorec_exhaust_tac ctxt frees n nchotomy = |
61 let val ks = 1 upto n in |
61 let val ks = 1 upto n in |
62 HEADGOAL (atac ORELSE' |
62 HEADGOAL (atac ORELSE' |
63 cut_tac nchotomy THEN' |
63 cut_tac nchotomy THEN' |