diff -r e8f719547298 -r 060ea04f6b50 IOA/example/Correctness.ML
--- a/IOA/example/Correctness.ML	Wed Mar 01 13:26:50 1995 +0100
+++ b/IOA/example/Correctness.ML	Wed Mar 01 17:32:10 1995 +0100
@@ -89,7 +89,7 @@
 by(case_tac "sq(sen(s))=[]" 1);
 
 by(asm_full_simp_tac hom_ss' 1);
-by(fast_tac (HOL_cs addSDs [plus_leD1 RS leD]) 1);
+by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);
 
 by(case_tac "m = hd(sq(sen(s)))" 1);
 
@@ -97,7 +97,7 @@
                      [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
 
 by(asm_full_simp_tac hom_ss 1);
-by(fast_tac (HOL_cs addSDs [plus_leD1 RS leD]) 1);
+by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);
 
 by(asm_full_simp_tac hom_ss 1);
 result();