src/ZF/Resid/Conversion.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 11319 8b84ee2cc79c
     1.1 --- a/src/ZF/Resid/Conversion.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/Resid/Conversion.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	Conversion.thy
     1.5 +(*  Title:      Conversion.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Ole Rasmussen
     1.8 +    Author:     Ole Rasmussen
     1.9      Copyright   1995  University of Cambridge
    1.10      Logic Image: ZF
    1.11  
    1.12 @@ -9,10 +9,10 @@
    1.13  Conversion = Confluence+
    1.14  
    1.15  consts
    1.16 -  Sconv1	:: i
    1.17 -  "<-1->"	:: [i,i]=>o (infixl 50)
    1.18 -  Sconv		:: i
    1.19 -  "<--->"	:: [i,i]=>o (infixl 50)
    1.20 +  Sconv1        :: i
    1.21 +  "<-1->"       :: [i,i]=>o (infixl 50)
    1.22 +  Sconv         :: i
    1.23 +  "<--->"       :: [i,i]=>o (infixl 50)
    1.24  
    1.25  translations
    1.26    "a<-1->b"    == "<a,b>:Sconv1"
    1.27 @@ -21,16 +21,16 @@
    1.28  inductive
    1.29    domains       "Sconv1" <= "lambda*lambda"
    1.30    intrs
    1.31 -    red1	"m -1-> n ==> m<-1->n"
    1.32 -    expl  	"n -1-> m ==> m<-1->n"
    1.33 -  type_intrs	"[red1D1,red1D2]@lambda.intrs@bool_typechecks"
    1.34 +    red1        "m -1-> n ==> m<-1->n"
    1.35 +    expl        "n -1-> m ==> m<-1->n"
    1.36 +  type_intrs    "[red1D1,red1D2]@lambda.intrs@bool_typechecks"
    1.37  
    1.38  inductive
    1.39    domains       "Sconv" <= "lambda*lambda"
    1.40    intrs
    1.41 -    one_step	"m<-1->n  ==> m<--->n"
    1.42 -    refl  	"m:lambda ==> m<--->m"
    1.43 -    trans	"[|m<--->n; n<--->p|] ==> m<--->p"
    1.44 -  type_intrs	"[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
    1.45 +    one_step    "m<-1->n  ==> m<--->n"
    1.46 +    refl        "m:lambda ==> m<--->m"
    1.47 +    trans       "[|m<--->n; n<--->p|] ==> m<--->p"
    1.48 +  type_intrs    "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
    1.49  end
    1.50