src/CTT/CTT.thy
changeset 21524 7843e2fd14a9
parent 21404 eb85850d3eb7
child 22808 a7daa74e2980
     1.1 --- a/src/CTT/CTT.thy	Fri Nov 24 22:05:19 2006 +0100
     1.2 +++ b/src/CTT/CTT.thy	Sun Nov 26 18:07:16 2006 +0100
     1.3 @@ -72,25 +72,25 @@
     1.4    "A * B == SUM _:A. B"
     1.5  
     1.6  notation (xsymbols)
     1.7 +  lambda  (binder "\<lambda>\<lambda>" 10) and
     1.8    Elem  ("(_ /\<in> _)" [10,10] 5) and
     1.9    Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
    1.10    Arrow  (infixr "\<longrightarrow>" 30) and
    1.11    Times  (infixr "\<times>" 50)
    1.12  
    1.13  notation (HTML output)
    1.14 +  lambda  (binder "\<lambda>\<lambda>" 10) and
    1.15    Elem  ("(_ /\<in> _)" [10,10] 5) and
    1.16    Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
    1.17    Times  (infixr "\<times>" 50)
    1.18  
    1.19  syntax (xsymbols)
    1.20 -  "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    1.21 -  "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
    1.22 -  "lam "    :: "[idts, i] => i"     ("(3\<lambda>\<lambda>_./ _)" 10)
    1.23 +  "_PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
    1.24 +  "_SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    1.25  
    1.26  syntax (HTML output)
    1.27 -  "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    1.28 -  "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
    1.29 -  "lam "    :: "[idts, i] => i"     ("(3\<lambda>\<lambda>_./ _)" 10)
    1.30 +  "_PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
    1.31 +  "_SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    1.32  
    1.33  axioms
    1.34