# HG changeset patch
# User wenzelm
# Date 1266245441 -3600
# Node ID c1ad622e90e47f4865992e5ae53c129309596ff2
# Parent  5b29c166004761bb7424983c94d2a9202ae03248
eliminated unnamed infixes;

diff -r 5b29c1660047 -r c1ad622e90e4 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Mon Feb 15 14:04:06 2010 +0100
+++ b/src/FOLP/IFOLP.thy	Mon Feb 15 15:50:41 2010 +0100
@@ -26,14 +26,14 @@
  EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
 
       (*** Logical Connectives -- Type Formers ***)
- "="            ::      "['a,'a] => o"  (infixl 50)
+ "op ="         ::      "['a,'a] => o"  (infixl "=" 50)
  True           ::      "o"
  False          ::      "o"
  Not            ::      "o => o"        ("~ _" [40] 40)
- "&"            ::      "[o,o] => o"    (infixr 35)
- "|"            ::      "[o,o] => o"    (infixr 30)
- "-->"          ::      "[o,o] => o"    (infixr 25)
- "<->"          ::      "[o,o] => o"    (infixr 25)
+ "op &"         ::      "[o,o] => o"    (infixr "&" 35)
+ "op |"         ::      "[o,o] => o"    (infixr "|" 30)
+ "op -->"       ::      "[o,o] => o"    (infixr "-->" 25)
+ "op <->"       ::      "[o,o] => o"    (infixr "<->" 25)
       (*Quantifiers*)
  All            ::      "('a => o) => o"        (binder "ALL " 10)
  Ex             ::      "('a => o) => o"        (binder "EX " 10)
@@ -53,9 +53,9 @@
  inr            :: "p=>p"
  when           :: "[p, p=>p, p=>p]=>p"
  lambda         :: "(p => p) => p"      (binder "lam " 55)
- "`"            :: "[p,p]=>p"           (infixl 60)
+ "op `"         :: "[p,p]=>p"           (infixl "`" 60)
  alll           :: "['a=>p]=>p"         (binder "all " 55)
- "^"            :: "[p,'a]=>p"          (infixl 55)
+ "op ^"         :: "[p,'a]=>p"          (infixl "^" 55)
  exists         :: "['a,p]=>p"          ("(1[_,/_])")
  xsplit         :: "[p,['a,p]=>p]=>p"
  ideq           :: "'a=>p"
diff -r 5b29c1660047 -r c1ad622e90e4 src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Mon Feb 15 14:04:06 2010 +0100
+++ b/src/LCF/LCF.thy	Mon Feb 15 15:50:41 2010 +0100
@@ -19,8 +19,8 @@
 
 typedecl tr
 typedecl void
-typedecl ('a,'b) "*"    (infixl 6)
-typedecl ('a,'b) "+"    (infixl 5)
+typedecl ('a,'b) "*"    (infixl "*" 6)
+typedecl ('a,'b) "+"    (infixl "+" 5)
 
 arities
   "fun" :: (cpo, cpo) cpo