src/ZF/Resid/Confluence.thy
changeset 22808 a7daa74e2980
parent 16417 9bc16273c2d4
child 24893 b8ef7afe3a6b
     1.1 --- a/src/ZF/Resid/Confluence.thy	Thu Apr 26 13:33:17 2007 +0200
     1.2 +++ b/src/ZF/Resid/Confluence.thy	Thu Apr 26 14:24:08 2007 +0200
     1.3 @@ -66,13 +66,15 @@
     1.4  
     1.5  consts
     1.6    Sconv1        :: "i"
     1.7 -  "<-1->"       :: "[i,i]=>o"   (infixl 50)
     1.8    Sconv         :: "i"
     1.9 -  "<--->"       :: "[i,i]=>o"   (infixl 50)
    1.10  
    1.11 -translations
    1.12 -  "a<-1->b"    == "<a,b> \<in> Sconv1"
    1.13 -  "a<--->b"    == "<a,b> \<in> Sconv"
    1.14 +abbreviation
    1.15 +  Sconv1_rel (infixl "<-1->" 50) where
    1.16 +  "a<-1->b == <a,b> \<in> Sconv1"
    1.17 +
    1.18 +abbreviation
    1.19 +  Sconv_rel (infixl "<--->" 50) where
    1.20 +  "a<--->b == <a,b> \<in> Sconv"
    1.21    
    1.22  inductive
    1.23    domains       "Sconv1" <= "lambda*lambda"