--- a/src/HOL/Library/Accessible_Part.thy Fri Nov 03 21:33:53 2000 +0100
+++ b/src/HOL/Library/Accessible_Part.thy Fri Nov 03 21:34:22 2000 +0100
@@ -28,7 +28,7 @@
syntax
termi :: "('a \<times> 'a) set => 'a set"
translations
- "termi r" == "acc (r^-1)"
+ "termi r" == "acc (r\<inverse>)"
subsection {* Induction rules *}
@@ -53,13 +53,13 @@
apply fast
done
-lemma acc_downwards_aux: "(b, a) \<in> r^* ==> a \<in> acc r --> b \<in> acc r"
+lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r --> b \<in> acc r"
apply (erule rtrancl_induct)
apply blast
apply (blast dest: acc_downward)
done
-theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r^* ==> b \<in> acc r"
+theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r"
apply (blast dest: acc_downwards_aux)
done