# HG changeset patch
# User blanchet
# Date 1346418243 -7200
# Node ID a6df36ecc2a8e95981941abc91c54d46f213608d
# Parent  3510b943dd5b0bed9a172c65a77dfc5de952f707
renamed "disc_disjoint" property "disj_exclus"

diff -r 3510b943dd5b -r a6df36ecc2a8 src/HOL/Codatatype/Tools/bnf_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 15:04:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 15:04:03 2012 +0200
@@ -22,7 +22,7 @@
 val case_discsN = "case_discs"
 val casesN = "cases"
 val ctr_selsN = "ctr_sels"
-val disc_disjointN = "disc_disjoint"
+val disc_exclusN = "disc_exclus"
 val disc_exhaustN = "disc_exhaust"
 val discsN = "discs"
 val distinctN = "distinct"
@@ -251,7 +251,7 @@
             |> `transpose
           end;
 
-        val disc_disjoint_thms =
+        val disc_exclus_thms =
           let
             fun mk_goal ((_, disc), (_, disc')) =
               Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v),
@@ -265,12 +265,12 @@
             val half_thmss =
               map3 (fn [] => K (K [])
                      | [(((m, discD), _), _)] => fn disc_thm => fn [goal] =>
-                [prove (mk_half_disc_disjoint_tac m discD disc_thm) goal])
+                [prove (mk_half_disc_exclus_tac m discD disc_thm) goal])
               half_pairss (flat disc_thmss') goal_halvess;
 
             val goal_other_halvess = map (map (mk_goal o swap)) half_pairss;
             val other_half_thmss =
-              map2 (map2 (prove o mk_other_half_disc_disjoint_tac)) half_thmss goal_other_halvess;
+              map2 (map2 (prove o mk_other_half_disc_exclus_tac)) half_thmss goal_other_halvess;
           in
             interleave (flat half_thmss) (flat other_half_thmss)
           end;
@@ -369,7 +369,7 @@
            (casesN, case_thms),
            (ctr_selsN, ctr_sel_thms),
            (discsN, (flat disc_thmss)),
-           (disc_disjointN, disc_disjoint_thms),
+           (disc_exclusN, disc_exclus_thms),
            (disc_exhaustN, [disc_exhaust_thm]),
            (distinctN, distinct_thms),
            (exhaustN, [exhaust_thm]),
diff -r 3510b943dd5b -r a6df36ecc2a8 src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML
--- 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 =