src/CTT/CTT.thy
changeset 22808 a7daa74e2980
parent 21524 7843e2fd14a9
child 23467 d1b97708d5eb
     1.1 --- a/src/CTT/CTT.thy	Thu Apr 26 13:33:17 2007 +0200
     1.2 +++ b/src/CTT/CTT.thy	Thu Apr 26 14:24:08 2007 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4    (*General Product and Function Space*)
     1.5    Prod      :: "[t, i=>t]=>t"
     1.6    (*Types*)
     1.7 -  "+"       :: "[t,t]=>t"           (infixr 40)
     1.8 +  Plus      :: "[t,t]=>t"           (infixr "+" 40)
     1.9    (*Equality type*)
    1.10    Eq        :: "[t,i,i]=>t"
    1.11    eq        :: "i"
    1.12 @@ -51,7 +51,7 @@
    1.13  
    1.14    (*Functions*)
    1.15    lambda    :: "(i => i) => i"      (binder "lam " 10)
    1.16 -  "`"       :: "[i,i]=>i"           (infixl 60)
    1.17 +  app       :: "[i,i]=>i"           (infixl "`" 60)
    1.18    (*Natural numbers*)
    1.19    "0"       :: "i"                  ("0")
    1.20    (*Pairing*)