diff -r a267ecd51f90 -r 7843e2fd14a9 src/CTT/CTT.thy --- a/src/CTT/CTT.thy Fri Nov 24 22:05:19 2006 +0100 +++ b/src/CTT/CTT.thy Sun Nov 26 18:07:16 2006 +0100 @@ -72,25 +72,25 @@ "A * B == SUM _:A. B" notation (xsymbols) + lambda (binder "\\" 10) and Elem ("(_ /\ _)" [10,10] 5) and Eqelem ("(2_ =/ _ \/ _)" [10,10,10] 5) and Arrow (infixr "\" 30) and Times (infixr "\" 50) notation (HTML output) + lambda (binder "\\" 10) and Elem ("(_ /\ _)" [10,10] 5) and Eqelem ("(2_ =/ _ \/ _)" [10,10,10] 5) and Times (infixr "\" 50) syntax (xsymbols) - "@SUM" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) - "@PROD" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) - "lam " :: "[idts, i] => i" ("(3\\_./ _)" 10) + "_PROD" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) + "_SUM" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) syntax (HTML output) - "@SUM" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) - "@PROD" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) - "lam " :: "[idts, i] => i" ("(3\\_./ _)" 10) + "_PROD" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) + "_SUM" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) axioms