src/HOL/Transitive_Closure.thy

   trancl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^+)" [1000] 999)
   "r^+ == Collect2 (member2 r)^++"
 
 abbreviation
   reflcl :: "('a => 'a => bool) => 'a => 'a => bool"  ("(_^==)" [1000] 1000) where
-  "r^== == join r op ="
+  "r^== == sup r op ="
 
 abbreviation
   reflcl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set"  ("(_^=)" [1000] 999) where
   "r^= == r \<union> Id"
 

 subsection {* Reflexive-transitive closure *}
 
 lemma rtrancl_set_eq [pred_set_conv]: "(member2 r)^** = member2 (r^*)"
   by (simp add: rtrancl_set_def)
 
-lemma reflcl_set_eq [pred_set_conv]: "(join (member2 r) op =) = member2 (r Un Id)"
+lemma reflcl_set_eq [pred_set_conv]: "(sup (member2 r) op =) = member2 (r Un Id)"
   by (simp add: expand_fun_eq)
 
 lemmas rtrancl_refl [intro!, Pure.intro!, simp] = rtrancl_refl [to_set]
 lemmas rtrancl_into_rtrancl [Pure.intro] = rtrancl_into_rtrancl [to_set]
 

   apply (drule rtrancl_mono', simp)
   done
 
 lemmas rtrancl_subset = rtrancl_subset' [to_set]
 
-lemma rtrancl_Un_rtrancl': "(join (R^**) (S^**))^** = (join R S)^**"
+lemma rtrancl_Un_rtrancl': "(sup (R^**) (S^**))^** = (sup R S)^**"
   by (blast intro!: rtrancl_subset' intro: rtrancl_mono' [THEN predicate2D])
 
 lemmas rtrancl_Un_rtrancl = rtrancl_Un_rtrancl' [to_set]
 
 lemma rtrancl_reflcl' [simp]: "(R^==)^** = R^**"

   apply (rename_tac a b)
   apply (case_tac "a = b", blast)
   apply (blast intro!: r_into_rtrancl)
   done
 
-lemma rtrancl_r_diff_Id': "(meet r op ~=)^** = r^**"
+lemma rtrancl_r_diff_Id': "(inf r op ~=)^** = r^**"
   apply (rule sym)
   apply (rule rtrancl_subset')
   apply blast+
   done