Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
authorhuffman
Wed, 27 Oct 2010 14:31:39 -0700
changeset 40323 4cce7c708402
parent 40322 707eb30e8a53
child 40324 b5e1ab22198a
add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
src/HOLCF/Lift.thy file | annotate | diff | comparison | revisions 
--- 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))"
isabelle