1.1 --- a/src/CTT/CTT.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/CTT/CTT.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -73,6 +73,14 @@
     1.4    "@PROD"   :: "[idt,t,t] => t"     ("(3\\<Pi> _\\<in>_./ _)"    10)
     1.5    "lam "    :: "[idts, i] => i"     ("(3\\<lambda>\\<lambda>_./ _)" 10)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +  "@*"      :: "[t,t]=>t"           ("(_ \\<times>/ _)"          [51,50] 50)
     1.9 +  Elem      :: "[i, t]=>prop"       ("(_ /\\<in> _)" [10,10] 5)
    1.10 +  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
    1.11 +  "@SUM"    :: "[idt,t,t] => t"     ("(3\\<Sigma> _\\<in>_./ _)" 10)
    1.12 +  "@PROD"   :: "[idt,t,t] => t"     ("(3\\<Pi> _\\<in>_./ _)"    10)
    1.13 +  "lam "    :: "[idts, i] => i"     ("(3\\<lambda>\\<lambda>_./ _)" 10)
    1.14 +
    1.15  rules
    1.16  
    1.17    (*Reduction: a weaker notion than equality;  a hack for simplification.