--- a/src/CTT/CTT.thy Tue Nov 14 13:25:59 2000 +0100
+++ b/src/CTT/CTT.thy Tue Nov 14 13:26:48 2000 +0100
@@ -39,9 +39,9 @@
eq :: "i"
(*Judgements*)
Type :: "t => prop" ("(_ type)" [10] 5)
- Eqtype :: "[t,t]=>prop" ("(3_ =/ _)" [10,10] 5)
+ Eqtype :: "[t,t]=>prop" ("(_ =/ _)" [10,10] 5)
Elem :: "[i, t]=>prop" ("(_ /: _)" [10,10] 5)
- Eqelem :: "[i,i,t]=>prop" ("(3_ =/ _ :/ _)" [10,10,10] 5)
+ Eqelem :: "[i,i,t]=>prop" ("(_ =/ _ :/ _)" [10,10,10] 5)
Reduce :: "[i,i]=>prop" ("Reduce[_,_]")
(*Types*)
"@PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10)
@@ -64,6 +64,17 @@
"SUM x:A. B" => "Sum(A, %x. B)"
"A * B" => "Sum(A, _K(B))"
+syntax (xsymbols)
+ "@-->" :: "[t,t]=>t" ("(_ \\<longrightarrow>/ _)" [31,30] 30)
+ "@*" :: "[t,t]=>t" ("(_ \\<times>/ _)" [51,50] 50)
+
+syntax (symbols)
+ 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.