diff -r 715d01b34abb -r a7daa74e2980 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Thu Apr 26 13:33:17 2007 +0200
+++ b/src/CTT/CTT.thy	Thu Apr 26 14:24:08 2007 +0200
@@ -37,7 +37,7 @@
   (*General Product and Function Space*)
   Prod      :: "[t, i=>t]=>t"
   (*Types*)
-  "+"       :: "[t,t]=>t"           (infixr 40)
+  Plus      :: "[t,t]=>t"           (infixr "+" 40)
   (*Equality type*)
   Eq        :: "[t,i,i]=>t"
   eq        :: "i"
@@ -51,7 +51,7 @@
 
   (*Functions*)
   lambda    :: "(i => i) => i"      (binder "lam " 10)
-  "`"       :: "[i,i]=>i"           (infixl 60)
+  app       :: "[i,i]=>i"           (infixl "`" 60)
   (*Natural numbers*)
   "0"       :: "i"                  ("0")
   (*Pairing*)