--- 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.