equal
deleted
inserted
replaced
87 |
87 |
88 by(forward_tac [inv3] 1); |
88 by(forward_tac [inv3] 1); |
89 by(case_tac "sq(sen(s))=[]" 1); |
89 by(case_tac "sq(sen(s))=[]" 1); |
90 |
90 |
91 by(asm_full_simp_tac hom_ss' 1); |
91 by(asm_full_simp_tac hom_ss' 1); |
92 by(fast_tac (HOL_cs addSDs [plus_leD1 RS leD]) 1); |
92 by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1); |
93 |
93 |
94 by(case_tac "m = hd(sq(sen(s)))" 1); |
94 by(case_tac "m = hd(sq(sen(s)))" 1); |
95 |
95 |
96 by(asm_full_simp_tac (hom_ss addsimps |
96 by(asm_full_simp_tac (hom_ss addsimps |
97 [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); |
97 [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); |
98 |
98 |
99 by(asm_full_simp_tac hom_ss 1); |
99 by(asm_full_simp_tac hom_ss 1); |
100 by(fast_tac (HOL_cs addSDs [plus_leD1 RS leD]) 1); |
100 by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1); |
101 |
101 |
102 by(asm_full_simp_tac hom_ss 1); |
102 by(asm_full_simp_tac hom_ss 1); |
103 result(); |
103 result(); |