# HG changeset patch
# User wenzelm
# Date 981758930 -3600
# Node ID 3041d0347d26b8792e174cf60f8750dfe3bdb02b
# Parent  0f6f1cd500e5ae2d6f4fcb59ff1d4b5c5de6dbbd
tuned;

diff -r 0f6f1cd500e5 -r 3041d0347d26 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Fri Feb 09 23:48:33 2001 +0100
+++ b/src/HOL/Transitive_Closure.thy	Fri Feb 09 23:48:50 2001 +0100
@@ -36,13 +36,13 @@
 use "Transitive_Closure_lemmas.ML"
 
 
-lemma reflcl_trancl [simp]: "(r\<^sup>+)\<^sup>= = r\<^sup>*"
+lemma reflcl_trancl [simp]: "(r^+)^= = r^*"
   apply safe
   apply (erule trancl_into_rtrancl)
   apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
   done
 
-lemma trancl_reflcl [simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*"
+lemma trancl_reflcl [simp]: "(r^=)^+ = r^*"
   apply safe
    apply (drule trancl_into_rtrancl)
    apply simp
@@ -55,34 +55,34 @@
   apply fast
   done
 
-lemma trancl_empty [simp]: "{}\<^sup>+ = {}"
+lemma trancl_empty [simp]: "{}^+ = {}"
   by (auto elim: trancl_induct)
 
-lemma rtrancl_empty [simp]: "{}\<^sup>* = Id"
+lemma rtrancl_empty [simp]: "{}^* = Id"
   by (rule subst [OF reflcl_trancl]) simp
 
-lemma rtranclD: "(a, b) \<in> R\<^sup>* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R\<^sup>+"
+lemma rtranclD: "(a, b) \<in> R^* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R^+"
   by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
 
 
 (* should be merged with the main body of lemmas: *)
 
-lemma Domain_rtrancl [simp]: "Domain (R\<^sup>*) = UNIV"
+lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"
   by blast
 
-lemma Range_rtrancl [simp]: "Range (R\<^sup>*) = UNIV"
+lemma Range_rtrancl [simp]: "Range (R^*) = UNIV"
   by blast
 
-lemma rtrancl_Un_subset: "(R\<^sup>* \<union> S\<^sup>*) \<subseteq> (R Un S)\<^sup>*"
+lemma rtrancl_Un_subset: "(R^* \<union> S^*) \<subseteq> (R Un S)^*"
   by (rule rtrancl_Un_rtrancl [THEN subst]) fast
 
-lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* ==> x \<in> (R \<union> S)\<^sup>*"
+lemma in_rtrancl_UnI: "x \<in> R^* \<or> x \<in> S^* ==> x \<in> (R \<union> S)^*"
   by (blast intro: subsetD [OF rtrancl_Un_subset])
 
-lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r"
+lemma trancl_domain [simp]: "Domain (r^+) = Domain r"
   by (unfold Domain_def) (blast dest: tranclD)
 
-lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r"
+lemma trancl_range [simp]: "Range (r^+) = Range r"
   by (simp add: Range_def trancl_converse [symmetric])
 
 end