--- 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
-