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