# HG changeset patch
# User huffman
# Date 1267633561 28800
# Node ID b56d5b1b1a558525b3177c61c97be7a8919f5b8b
# Parent  d607ea103dcbb40f682ea0bf0f3b1c89bca12b00
add infix declarations

diff -r d607ea103dcb -r b56d5b1b1a55 src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Wed Mar 03 08:20:20 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Wed Mar 03 08:26:01 2010 -0800
@@ -25,6 +25,10 @@
 
 open HOLCF_Library;
 
+infixr 6 ->>;
+infix -->>;
+infix 9 `;
+
 fun axiomatize_isomorphism
     (dbind : binding, (lhsT, rhsT))
     (thy : theory)
diff -r d607ea103dcb -r b56d5b1b1a55 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Mar 03 08:20:20 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Mar 03 08:26:01 2010 -0800
@@ -35,8 +35,10 @@
 struct
 
 open HOLCF_Library;
+
 infixr 6 ->>;
 infix -->>;
+infix 9 `;
 
 (************************** miscellaneous functions ***************************)