equal
deleted
inserted
replaced
104 |
104 |
105 by(forward_tac [inv3] 1); |
105 by(forward_tac [inv3] 1); |
106 by(case_tac "sq(sen(s))=[]" 1); |
106 by(case_tac "sq(sen(s))=[]" 1); |
107 |
107 |
108 by(asm_full_simp_tac ss' 1); |
108 by(asm_full_simp_tac ss' 1); |
109 by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1); |
109 by(fast_tac (!claset addSDs [add_leD1 RS leD]) 1); |
110 |
110 |
111 by(case_tac "m = hd(sq(sen(s)))" 1); |
111 by(case_tac "m = hd(sq(sen(s)))" 1); |
112 |
112 |
113 by(asm_full_simp_tac (!simpset addsimps |
113 by(asm_full_simp_tac (!simpset addsimps |
114 [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); |
114 [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); |
115 |
115 |
116 by(Asm_full_simp_tac 1); |
116 by(Asm_full_simp_tac 1); |
117 by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1); |
117 by(fast_tac (!claset addSDs [add_leD1 RS leD]) 1); |
118 |
118 |
119 by(Asm_full_simp_tac 1); |
119 by(Asm_full_simp_tac 1); |
120 qed"ntp_correct"; |
120 qed"ntp_correct"; |