diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Resid/Conversion.thy
--- a/src/ZF/Resid/Conversion.thy	Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(*  Title:      Conversion.thy
-    ID:         $Id$
-    Author:     Ole Rasmussen
-    Copyright   1995  University of Cambridge
-    Logic Image: ZF
-
-*)
-
-Conversion = Confluence+
-
-consts
-  Sconv1        :: i
-  "<-1->"       :: [i,i]=>o (infixl 50)
-  Sconv         :: i
-  "<--->"       :: [i,i]=>o (infixl 50)
-
-translations
-  "a<-1->b"    == "<a,b>:Sconv1"
-  "a<--->b"    == "<a,b>:Sconv"
-  
-inductive
-  domains       "Sconv1" <= "lambda*lambda"
-  intrs
-    red1        "m -1-> n ==> m<-1->n"
-    expl        "n -1-> m ==> m<-1->n"
-  type_intrs    "[red1D1,red1D2]@lambda.intrs@bool_typechecks"
-
-inductive
-  domains       "Sconv" <= "lambda*lambda"
-  intrs
-    one_step    "m<-1->n  ==> m<--->n"
-    refl        "m \\<in> lambda ==> m<--->m"
-    trans       "[|m<--->n; n<--->p|] ==> m<--->p"
-  type_intrs    "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
-end
-