# 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" ("(\\_\\)") - "GeqFF" :: "tr => bool" ("(\\_\\)") - -translations - "\\x\\" == "x = TT" - "\\x\\" == "x = FF" -*) + If2_def "If2 Q x y == If Q then x else y fi" end