# HG changeset patch
# User huffman
# Date 1288215099 25200
# Node ID 4cce7c7084027360ac2673260f3d92f1459165ea
# Parent  707eb30e8a53f5d2d84261954a0ffeef693629af
add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'

diff -r 707eb30e8a53 -r 4cce7c708402 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Wed Oct 27 14:15:54 2010 -0700
+++ b/src/HOLCF/Lift.thy	Wed Oct 27 14:31:39 2010 -0700
@@ -95,6 +95,11 @@
   flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder "FLIFT " 10)  where
   "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
 
+translations
+  "\<Lambda>(XCONST Def x). t" => "CONST flift1 (\<lambda>x. t)"
+  "\<Lambda>(CONST Def x). FLIFT y. t" <= "FLIFT x y. t"
+  "\<Lambda>(CONST Def x). t" <= "FLIFT x. t"
+
 definition
   flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
   "flift2 f = (FLIFT x. Def (f x))"