src/CTT/CTT.thy
changeset 21524 7843e2fd14a9
parent 21404 eb85850d3eb7
child 22808 a7daa74e2980
--- a/src/CTT/CTT.thy	Fri Nov 24 22:05:19 2006 +0100
+++ b/src/CTT/CTT.thy	Sun Nov 26 18:07:16 2006 +0100
@@ -72,25 +72,25 @@
   "A * B == SUM _:A. B"
 
 notation (xsymbols)
+  lambda  (binder "\<lambda>\<lambda>" 10) and
   Elem  ("(_ /\<in> _)" [10,10] 5) and
   Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
   Arrow  (infixr "\<longrightarrow>" 30) and
   Times  (infixr "\<times>" 50)
 
 notation (HTML output)
+  lambda  (binder "\<lambda>\<lambda>" 10) and
   Elem  ("(_ /\<in> _)" [10,10] 5) and
   Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
   Times  (infixr "\<times>" 50)
 
 syntax (xsymbols)
-  "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
-  "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
-  "lam "    :: "[idts, i] => i"     ("(3\<lambda>\<lambda>_./ _)" 10)
+  "_PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
+  "_SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
 
 syntax (HTML output)
-  "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
-  "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
-  "lam "    :: "[idts, i] => i"     ("(3\<lambda>\<lambda>_./ _)" 10)
+  "_PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
+  "_SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
 
 axioms