Mercurial Mercurial > repos > Old_HOL / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Renamed plus_leD1 to add_leD1.
authorlcp
Wed, 01 Mar 1995 17:32:10 +0100
changeset 224 060ea04f6b50
parent 223 e8f719547298
child 225 fa4aebe5b6f1
Renamed plus_leD1 to add_leD1.
IOA/example/Correctness.ML file | annotate | diff | comparison | revisions 
--- 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();
Old_HOL