equal
deleted
inserted
replaced
52 apply ( assumption) |
52 apply ( assumption) |
53 apply (drule not_ex [THEN iffD1]) |
53 apply (drule not_ex [THEN iffD1]) |
54 apply (subst slen_infinite) |
54 apply (subst slen_infinite) |
55 apply (erule thin_rl) |
55 apply (erule thin_rl) |
56 apply (drule spec) |
56 apply (drule spec) |
57 apply (fold ile_def) |
57 apply (unfold linorder_not_less) |
58 apply (erule ile_iless_trans [THEN Infty_eq [THEN iffD1]]) |
58 apply (erule ile_iless_trans [THEN Infty_eq [THEN iffD1]]) |
59 apply (simp) |
59 apply (simp) |
60 done |
60 done |
61 |
61 |
62 |
62 |
140 apply (intro strip) |
140 apply (intro strip) |
141 apply (erule allE, erule all_dupE, erule exE, erule exE) |
141 apply (erule allE, erule all_dupE, erule exE, erule exE) |
142 apply (erule conjE) |
142 apply (erule conjE) |
143 apply (case_tac "#x < Fin i") |
143 apply (case_tac "#x < Fin i") |
144 apply ( fast) |
144 apply ( fast) |
145 apply (fold ile_def) |
145 apply (unfold linorder_not_less) |
146 apply (drule (1) mp) |
146 apply (drule (1) mp) |
147 apply (erule all_dupE, drule mp, rule refl_less) |
147 apply (erule all_dupE, drule mp, rule refl_less) |
148 apply (erule ssubst) |
148 apply (erule ssubst) |
149 apply (erule allE, drule (1) mp) |
149 apply (erule allE, drule (1) mp) |
150 apply (drule_tac P="%x. x" in subst, assumption) |
150 apply (drule_tac P="%x. x" in subst, assumption) |