equal
deleted
inserted
replaced
213 (E\<turnstile>es[::]Ts \<longrightarrow> ws_prog (prg E) \<longrightarrow> Ball (set Ts) (is_type (prg E))) \<and> |
213 (E\<turnstile>es[::]Ts \<longrightarrow> ws_prog (prg E) \<longrightarrow> Ball (set Ts) (is_type (prg E))) \<and> |
214 (E\<turnstile>c \<surd> \<longrightarrow> True)" |
214 (E\<turnstile>c \<surd> \<longrightarrow> True)" |
215 apply (rule ty_expr_ty_exprs_wt_stmt.induct) |
215 apply (rule ty_expr_ty_exprs_wt_stmt.induct) |
216 apply auto |
216 apply auto |
217 apply ( erule typeof_empty_is_type) |
217 apply ( erule typeof_empty_is_type) |
218 apply ( simp split add: if_split_asm) |
218 apply ( simp split: if_split_asm) |
219 apply ( drule field_fields) |
219 apply ( drule field_fields) |
220 apply ( drule (1) fields_is_type) |
220 apply ( drule (1) fields_is_type) |
221 apply ( simp (no_asm_simp)) |
221 apply ( simp (no_asm_simp)) |
222 apply (assumption) |
222 apply (assumption) |
223 apply (auto dest!: max_spec2mheads method_wf_mhead is_type_rTI |
223 apply (auto dest!: max_spec2mheads method_wf_mhead is_type_rTI |