src/ZF/Resid/Redex.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 2874 b1e7e2179597
     1.1 --- a/src/ZF/Resid/Redex.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/Resid/Redex.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	Redex.thy
     1.5 +(*  Title:      Redex.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 @@ -10,14 +10,14 @@
    1.13    redexes     :: i
    1.14  
    1.15  datatype
    1.16 -  "redexes" = Var ("n: nat")	        
    1.17 +  "redexes" = Var ("n: nat")            
    1.18              | Fun ("t: redexes")
    1.19              | App ("b:bool" ,"f:redexes" , "a:redexes")
    1.20    type_intrs "[bool_into_univ]"
    1.21    
    1.22  
    1.23  consts
    1.24 -  redex_rec   	:: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
    1.25 +  redex_rec     :: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
    1.26   
    1.27  defs
    1.28    redex_rec_def