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 infix declarations
authorhuffman
Wed, 03 Mar 2010 08:26:01 -0800
changeset 35561 b56d5b1b1a55
parent 35560 d607ea103dcb
child 35562 e27550a842b9
add infix declarations
src/HOLCF/Tools/Domain/domain_axioms.ML file | annotate | diff | comparison | revisions
src/HOLCF/Tools/Domain/domain_constructors.ML file | annotate | diff | comparison | revisions 
--- 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)
--- 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 ***************************)
isabelle