equal
deleted
inserted
replaced
148 by (Asm_simp_tac 2); |
148 by (Asm_simp_tac 2); |
149 by (subgoal_tac "r@[a] ~= []" 2); |
149 by (subgoal_tac "r@[a] ~= []" 2); |
150 by (fast_tac HOL_cs 2); |
150 by (fast_tac HOL_cs 2); |
151 by (Simp_tac 2); |
151 by (Simp_tac 2); |
152 by (subgoal_tac "flat(yss) @ zs = list" 1); |
152 by (subgoal_tac "flat(yss) @ zs = list" 1); |
153 by (Asm_simp_tac 1); |
153 by(hyp_subst_tac 1); |
|
154 by(atac 1); |
154 by (case_tac "yss = []" 1); |
155 by (case_tac "yss = []" 1); |
155 by (Asm_simp_tac 1); |
156 by (Asm_simp_tac 1); |
156 by (hyp_subst_tac 1); |
157 by (hyp_subst_tac 1); |
157 by (fast_tac (HOL_cs addSDs [no_acc]) 1); |
158 by (fast_tac (HOL_cs addSDs [no_acc]) 1); |
158 by (etac ((neq_Nil_conv RS iffD1) RS exE) 1); |
159 by (etac ((neq_Nil_conv RS iffD1) RS exE) 1); |