# HG changeset patch
# User wenzelm
# Date 973283662 -3600
# Node ID ac1ae85a56051dd7fe65f80e023c9a11bdd6b9dd
# Parent  9dac2cad550097d381c7572ae69fcb0c9a3d7edc
tuned notation;

diff -r 9dac2cad5500 -r ac1ae85a5605 src/HOL/Library/Accessible_Part.thy
--- 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