Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/LCF/LCF.thy
changeset 41310 65631ca437c9
parent 36452 d37c6eed8117
child 47025 b2b8ae61d6ad 
--- a/src/LCF/LCF.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/LCF/LCF.thy	Mon Dec 20 16:44:33 2010 +0100
@@ -18,13 +18,13 @@
 
 typedecl tr
 typedecl void
-typedecl ('a,'b) "*"    (infixl "*" 6)
-typedecl ('a,'b) "+"    (infixl "+" 5)
+typedecl ('a,'b) prod  (infixl "*" 6)
+typedecl ('a,'b) sum  (infixl "+" 5)
 
 arities
   "fun" :: (cpo, cpo) cpo
-  "*" :: (cpo, cpo) cpo
-  "+" :: (cpo, cpo) cpo
+  prod :: (cpo, cpo) cpo
+  sum :: (cpo, cpo) cpo
   tr :: cpo
   void :: cpo
isabelle