Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Lift3.thy
changeset 1479 21eb5e156d91
parent 1274 ea0668a1c0ba 
--- 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"
isabelle