src/CTT/CTT.thy
changeset 14565 c6dc17aab88a
parent 12110 f8b4b11cd79d
child 14765 bafb24c150c1
--- a/src/CTT/CTT.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/CTT/CTT.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -73,6 +73,14 @@
   "@PROD"   :: "[idt,t,t] => t"     ("(3\\<Pi> _\\<in>_./ _)"    10)
   "lam "    :: "[idts, i] => i"     ("(3\\<lambda>\\<lambda>_./ _)" 10)
 
+syntax (HTML output)
+  "@*"      :: "[t,t]=>t"           ("(_ \\<times>/ _)"          [51,50] 50)
+  Elem      :: "[i, t]=>prop"       ("(_ /\\<in> _)" [10,10] 5)
+  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
+  "@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)
+
 rules
 
   (*Reduction: a weaker notion than equality;  a hack for simplification.