src/ZF/Resid/Substitution.thy

--- a/src/ZF/Resid/Substitution.thy	Thu Apr 26 13:33:17 2007 +0200
+++ b/src/ZF/Resid/Substitution.thy	Thu Apr 26 14:24:08 2007 +0200
@@ -11,7 +11,7 @@
   lift_aux      :: "i=>i"
   lift          :: "i=>i"
   subst_aux     :: "i=>i"
-  "'/"          :: "[i,i]=>i"  (infixl 70)  (*subst*)
+  subst         :: "[i,i]=>i"  (infixl "'/" 70)
 
 constdefs
   lift_rec      :: "[i,i]=> i"
@@ -269,5 +269,3 @@
 by (erule Sreg.induct, simp_all add: subst_Var lift_rec_preserve_reg)
 
 end
-
-