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();