diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Lift3.thy
--- a/src/HOLCF/Lift3.thy	Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Lift3.thy	Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOLCF/lift3.thy
+(*  Title:      HOLCF/lift3.thy
     ID:         $Id$
-    Author: 	Franz Regensburger
+    Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
 
@@ -10,19 +10,19 @@
 
 Lift3 = Lift2 +
 
-arities "u" :: (pcpo)pcpo			(* Witness lift2.ML *)
+arities "u" :: (pcpo)pcpo                       (* Witness lift2.ML *)
 
 consts  
-	up	     :: "'a -> ('a)u" 
-	lift         :: "('a->'c)-> ('a)u -> 'c"
+        up           :: "'a -> ('a)u" 
+        lift         :: "('a->'c)-> ('a)u -> 'c"
 
 rules 
 
-	inst_lift_pcpo	"(UU::('a)u) = UU_lift"
+        inst_lift_pcpo  "(UU::('a)u) = UU_lift"
 
 defs
-	up_def		"up     == (LAM x.Iup(x))"
-	lift_def	"lift   == (LAM f p.Ilift(f)(p))"
+        up_def          "up     == (LAM x.Iup(x))"
+        lift_def        "lift   == (LAM f p.Ilift(f)(p))"
 
 translations
 "case l of up`x => t1" == "lift`(LAM x.t1)`l"