# HG changeset patch
# User mueller
# Date 861897087 -7200
# Node ID 5aa3bb94b7290815b8374c3f895953c204d1eb91
# Parent  5230c37ad29f55f8440b56aebcc3569a91209ff5
deleted definitions for blift and plift

diff -r 5230c37ad29f -r 5aa3bb94b729 src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Thu Apr 24 17:50:34 1997 +0200
+++ b/src/HOLCF/Tr.thy	Thu Apr 24 17:51:27 1997 +0200
@@ -20,7 +20,7 @@
         trand           :: "tr -> tr -> tr"
         tror            :: "tr -> tr -> tr"
         neg             :: "tr -> tr"
-        plift           :: "('a::term => bool) => 'a lift -> tr"
+        If2             :: "tr=>'c=>'c=>'c"
 
 syntax  "@cifte"        :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60)
         "@andalso"      :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
@@ -37,21 +37,7 @@
   ifte_def    "Icifte == (LAM b t e.flift1(%b.if b then t else e)`b)"
   andalso_def "trand == (LAM x y.If x then y else FF fi)"
   orelse_def  "tror == (LAM x y.If x then TT else y fi)"
-(* andalso, orelse are different from strict functions 
-  andalso_def "trand == flift1(flift2 o (op &))"
-  orelse_def  "tror == flift1(flift2 o (op |))"
-*)
-  plift_def   "plift p == (LAM x. flift1(%a.Def(p a))`x)"
-
-(* FIXME remove?
-syntax
-  "GeqTT"        :: "tr => bool"               ("(\\<lceil>_\\<rceil>)")
-  "GeqFF"        :: "tr => bool"               ("(\\<lfloor>_\\<rfloor>)")
-
-translations
-  "\\<lceil>x\\<rceil>" == "x = TT"
-  "\\<lfloor>x\\<rfloor>" == "x = FF"
-*)
+  If2_def     "If2 Q x y == If Q then x else y fi"
 
 end