equal
deleted
inserted
replaced
131 apply (rule_tac x=Z in spec) |
131 apply (rule_tac x=Z in spec) |
132 apply (induct_tac "n") |
132 apply (induct_tac "n") |
133 apply (clarify intro!: Impl_nvalid_0) |
133 apply (clarify intro!: Impl_nvalid_0) |
134 apply (clarify intro!: Impl_nvalid_Suc) |
134 apply (clarify intro!: Impl_nvalid_Suc) |
135 apply (drule nvalids_SucD) |
135 apply (drule nvalids_SucD) |
136 apply (simp only: all_simps) |
136 apply (simp only: HOL.all_simps) |
137 apply (erule (1) impE) |
137 apply (erule (1) impE) |
138 apply (drule (2) Impl_sound_lemma) |
138 apply (drule (2) Impl_sound_lemma) |
139 apply blast |
139 apply blast |
140 apply assumption |
140 apply assumption |
141 done |
141 done |