equal
deleted
inserted
replaced
252 apply (erule contrapos_np) |
252 apply (erule contrapos_np) |
253 apply (drule fstream_exhaust_eq [THEN iffD1]) |
253 apply (drule fstream_exhaust_eq [THEN iffD1]) |
254 apply (clarsimp) |
254 apply (clarsimp) |
255 apply (drule (1) fstream_lub_lemma) |
255 apply (drule (1) fstream_lub_lemma) |
256 apply (clarsimp) |
256 apply (clarsimp) |
257 apply (tactic "simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1") |
257 apply (simp only: ex_simps [symmetric] all_simps [symmetric]) |
258 apply (rule_tac x="Xa" in exI) |
258 apply (rule_tac x="Xa" in exI) |
259 apply (rule allI) |
259 apply (rule allI) |
260 apply (rotate_tac -1) |
260 apply (rotate_tac -1) |
261 apply (erule_tac x="i" in allE) |
261 apply (erule_tac x="i" in allE) |
262 apply (clarsimp) |
262 apply (clarsimp) |