# HG changeset patch
# User huffman
# Date 1214168560 -7200
# Node ID 9e74019041d4ea4145d9e619d29cca6f9ad9b4d3
# Parent  5d24085e085809f74e257f003a0073507580e8b1
use new-style abbreviation/notation for fix syntax

diff -r 5d24085e0858 -r 9e74019041d4 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Sat Jun 21 16:18:52 2008 +0200
+++ b/src/HOLCF/Fix.thy	Sun Jun 22 23:02:40 2008 +0200
@@ -8,7 +8,7 @@
 header {* Fixed point operator and admissibility *}
 
 theory Fix
-imports Cfun Cprod Adm
+imports Cfun Cprod
 begin
 
 defaultsort pcpo
@@ -59,14 +59,12 @@
 
 text {* Binder syntax for @{term fix} *}
 
-syntax
-  "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3FIX _./ _)" [1000, 10] 10)
+abbreviation
+  fix_syn :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  (binder "FIX " 10) where
+  "fix_syn (\<lambda>x. f x) \<equiv> fix\<cdot>(\<Lambda> x. f x)"
 
-syntax (xsymbols)
-  "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3\<mu> _./ _)" [1000, 10] 10)
-
-translations
-  "\<mu> x. t" == "CONST fix\<cdot>(\<Lambda> x. t)"
+notation (xsymbols)
+  fix_syn  (binder "\<mu> " 10)
 
 text {* Properties of @{term fix} *}