# HG changeset patch
# User huffman
# Date 1114555658 -7200
# Node ID 83cb9dae3817b3d2e7fff1f4e1baf3a6bdc577e0
# Parent  674ff97ce0efe21e20ba8e2fac1ba0535f272e6f
Added binder syntax for fix

diff -r 674ff97ce0ef -r 83cb9dae3817 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Tue Apr 26 20:41:37 2005 +0200
+++ b/src/HOLCF/Fix.thy	Wed Apr 27 00:47:38 2005 +0200
@@ -9,7 +9,7 @@
 header {* Fixed point operator and admissibility *}
 
 theory Fix
-imports Cfun
+imports Cfun Cprod
 begin
 
 consts
@@ -35,6 +35,21 @@
 admw_def:      "admw P == !F. (!n. P (iterate n F UU)) -->
                             P (lub(range (%i. iterate i F UU)))" 
 
+text {* Binder syntax for @{term fix} *}
+
+syntax
+  "@FIX" :: "('a => 'a) => 'a"  (binder "FIX " 10)
+  "@FIXP" :: "[patterns, 'a] => 'a"  ("(3FIX <_>./ _)" [0, 10] 10)
+
+syntax (xsymbols)
+  "FIX " :: "[idt, 'a] => 'a"  ("(3\<mu>_./ _)" [0, 10] 10)
+  "@FIXP" :: "[patterns, 'a] => 'a"  ("(3\<mu>()<_>./ _)" [0, 10] 10)
+
+translations
+  "FIX x. LAM y. t" == "fix\<cdot>(LAM x y. t)"
+  "FIX x. t" == "fix\<cdot>(LAM x. t)"
+  "FIX <xs>. t" == "fix\<cdot>(LAM <xs>. t)"
+
 text {* derive inductive properties of iterate from primitive recursion *}
 
 lemma iterate_Suc2: "iterate (Suc n) F x = iterate n F (F$x)"