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  ("(_ /\<in> _)" [10,10] 5)
-  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
-  Arrow  (infixr "\<longrightarrow>" 30)
+  Elem  ("(_ /\<in> _)" [10,10] 5) and
+  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
+  Arrow  (infixr "\<longrightarrow>" 30) and
   Times  (infixr "\<times>" 50)
 
 notation (HTML output)
-  Elem  ("(_ /\<in> _)" [10,10] 5)
-  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
+  Elem  ("(_ /\<in> _)" [10,10] 5) and
+  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
   Times  (infixr "\<times>" 50)
 
 syntax (xsymbols)