diff -r dd58f13a8eb4 -r eb85850d3eb7 src/CTT/CTT.thy --- a/src/CTT/CTT.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/CTT/CTT.thy Fri Nov 17 02:20:03 2006 +0100 @@ -65,20 +65,21 @@ "SUM x:A. B" == "Sum(A, %x. B)" abbreviation - Arrow :: "[t,t]=>t" (infixr "-->" 30) + Arrow :: "[t,t]=>t" (infixr "-->" 30) where "A --> B == PROD _:A. B" - Times :: "[t,t]=>t" (infixr "*" 50) +abbreviation + Times :: "[t,t]=>t" (infixr "*" 50) where "A * B == SUM _:A. B" notation (xsymbols) - Elem ("(_ /\ _)" [10,10] 5) - Eqelem ("(2_ =/ _ \/ _)" [10,10,10] 5) - Arrow (infixr "\" 30) + Elem ("(_ /\ _)" [10,10] 5) and + Eqelem ("(2_ =/ _ \/ _)" [10,10,10] 5) and + Arrow (infixr "\" 30) and Times (infixr "\" 50) notation (HTML output) - Elem ("(_ /\ _)" [10,10] 5) - Eqelem ("(2_ =/ _ \/ _)" [10,10,10] 5) + Elem ("(_ /\ _)" [10,10] 5) and + Eqelem ("(2_ =/ _ \/ _)" [10,10,10] 5) and Times (infixr "\" 50) syntax (xsymbols)