--- a/IntEx.thy	Tue Nov 24 14:19:54 2009 +0100
+++ b/IntEx.thy	Tue Nov 24 15:15:10 2009 +0100
@@ -187,7 +187,7 @@
 *}
 
 
-lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"
+lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *})
 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})