--- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Fri Aug 31 15:04:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Fri Aug 31 15:04:03 2012 +0200
@@ -11,9 +11,9 @@
val mk_case_disc_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic
val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic
val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
- val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
+ val mk_half_disc_exclus_tac: int -> thm -> thm -> tactic
val mk_nchotomy_tac: int -> thm -> tactic
- val mk_other_half_disc_disjoint_tac: thm -> tactic
+ val mk_other_half_disc_exclus_tac: thm -> tactic
val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic
val mk_split_asm_tac: Proof.context -> thm -> tactic
end;
@@ -37,13 +37,13 @@
(rtac allI THEN' rtac exhaust THEN'
EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
-fun mk_half_disc_disjoint_tac m discD disc'_thm =
+fun mk_half_disc_exclus_tac m discD disc'_thm =
(dtac discD THEN'
REPEAT_DETERM_N m o etac exE THEN'
hyp_subst_tac THEN'
rtac disc'_thm) 1;
-fun mk_other_half_disc_disjoint_tac half_thm =
+fun mk_other_half_disc_exclus_tac half_thm =
(etac @{thm contrapos_pn} THEN' etac half_thm) 1;
fun mk_disc_exhaust_tac n exhaust discIs =