equal
deleted
inserted
replaced
153 apply simp |
153 apply simp |
154 apply (intro allI impI) |
154 apply (intro allI impI) |
155 apply (erule disjE, simp) |
155 apply (erule disjE, simp) |
156 apply (elim exE conjE) |
156 apply (elim exE conjE) |
157 apply (erule allE, erule impE, assumption) |
157 apply (erule allE, erule impE, assumption) |
158 apply (simp add: exec_all_def exec_d_def split: type_error.splits split_if_asm) |
158 apply (simp add: exec_all_def exec_d_def split: type_error.splits if_split_asm) |
159 apply (rule rtrancl_trans, assumption) |
159 apply (rule rtrancl_trans, assumption) |
160 apply blast |
160 apply blast |
161 done |
161 done |
162 moreover |
162 moreover |
163 assume "G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t)" |
163 assume "G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t)" |