src/ZF/Resid/Reduction.thy
changeset 22808 a7daa74e2980
parent 16417 9bc16273c2d4
child 24892 c663e675e177
     1.1 --- a/src/ZF/Resid/Reduction.thy	Thu Apr 26 13:33:17 2007 +0200
     1.2 +++ b/src/ZF/Resid/Reduction.thy	Thu Apr 26 14:24:08 2007 +0200
     1.3 @@ -74,16 +74,22 @@
     1.4    Sred      :: "i"
     1.5    Spar_red1 :: "i"
     1.6    Spar_red  :: "i"
     1.7 -  "-1->"    :: "[i,i]=>o"  (infixl 50)
     1.8 -  "--->"    :: "[i,i]=>o"  (infixl 50)
     1.9 -  "=1=>"    :: "[i,i]=>o"  (infixl 50)
    1.10 -  "===>"    :: "[i,i]=>o"  (infixl 50)
    1.11 +
    1.12 +abbreviation
    1.13 +  Sred1_rel (infixl "-1->" 50) where
    1.14 +  "a -1-> b == <a,b> \<in> Sred1"
    1.15  
    1.16 -translations
    1.17 -  "a -1-> b" == "<a,b> \<in> Sred1"
    1.18 -  "a ---> b" == "<a,b> \<in> Sred"
    1.19 -  "a =1=> b" == "<a,b> \<in> Spar_red1"
    1.20 -  "a ===> b" == "<a,b> \<in> Spar_red"
    1.21 +abbreviation
    1.22 +  Sred_rel (infixl "--->" 50) where
    1.23 +  "a ---> b == <a,b> \<in> Sred"
    1.24 +
    1.25 +abbreviation
    1.26 +  Spar_red1_rel (infixl "=1=>" 50) where
    1.27 +  "a =1=> b == <a,b> \<in> Spar_red1"
    1.28 +
    1.29 +abbreviation
    1.30 +  Spar_red_rel (infixl "===>" 50) where
    1.31 +  "a ===> b == <a,b> \<in> Spar_red"
    1.32    
    1.33    
    1.34  inductive