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/CTT/CTT.thy
changeset 22808 a7daa74e2980
parent 21524 7843e2fd14a9
child 23467 d1b97708d5eb 
--- 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*)
isabelle