# HG changeset patch
# User huffman
# Date 1128915977 -7200
# Node ID 405fb812e7387cb11db66f9ad4b2f483cb052612
# Parent  9942c5ed866aa614950fb945ec166b938476c810
add names to infix declarations

diff -r 9942c5ed866a -r 405fb812e738 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Mon Oct 10 05:30:02 2005 +0200
+++ b/src/HOLCF/Cfun.thy	Mon Oct 10 05:46:17 2005 +0200
@@ -22,7 +22,7 @@
 lemma adm_cont: "adm cont"
 by (rule admI, rule cont_lub_fun)
 
-cpodef (CFun)  ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}"
+cpodef (CFun)  ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}"
 by (simp add: Ex_cont adm_cont)
 
 syntax (xsymbols)
diff -r 9942c5ed866a -r 405fb812e738 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Mon Oct 10 05:30:02 2005 +0200
+++ b/src/HOLCF/Sprod.thy	Mon Oct 10 05:46:17 2005 +0200
@@ -15,7 +15,7 @@
 
 subsection {* Definition of strict product type *}
 
-pcpodef (Sprod)  ('a, 'b) "**" (infixr 20) =
+pcpodef (Sprod)  ('a, 'b) "**" (infixr "**" 20) =
         "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
 by simp
 
diff -r 9942c5ed866a -r 405fb812e738 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Mon Oct 10 05:30:02 2005 +0200
+++ b/src/HOLCF/Ssum.thy	Mon Oct 10 05:46:17 2005 +0200
@@ -15,7 +15,7 @@
 
 subsection {* Definition of strict sum type *}
 
-pcpodef (Ssum)  ('a, 'b) "++" (infixr 10) = 
+pcpodef (Ssum)  ('a, 'b) "++" (infixr "++" 10) = 
         "{p::'a \<times> 'b. cfst\<cdot>p = \<bottom> \<or> csnd\<cdot>p = \<bottom>}"
 by simp