equal
deleted
inserted
replaced
25 apply (case_tac "CC") |
25 apply (case_tac "CC") |
26 apply simp |
26 apply simp |
27 apply (case_tac "ref_ty") |
27 apply (case_tac "ref_ty") |
28 apply (clarsimp simp add: conf_def) |
28 apply (clarsimp simp add: conf_def) |
29 apply simp |
29 apply simp |
30 apply (ind_cases2 "G \<turnstile> Class cname \<preceq>? Class D" for cname, simp) |
30 apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D" for cname, simp) |
31 apply (rule conf_widen, assumption+) apply (erule widen.subcls) |
31 apply (rule conf_widen, assumption+) apply (erule widen.subcls) |
32 |
32 |
33 apply (unfold cast_ok_def) |
33 apply (unfold cast_ok_def) |
34 apply( case_tac "v = Null") |
34 apply( case_tac "v = Null") |
35 apply( simp) |
35 apply( simp) |
220 apply (simp (no_asm_simp) add: xconf_def) |
220 apply (simp (no_asm_simp) add: xconf_def) |
221 apply( clarsimp) |
221 apply( clarsimp) |
222 apply( rule conjI) |
222 apply( rule conjI) |
223 apply( force elim!: NewC_conforms) |
223 apply( force elim!: NewC_conforms) |
224 apply( rule conf_obj_AddrI) |
224 apply( rule conf_obj_AddrI) |
225 apply( rule_tac [2] rtrancl.rtrancl_refl) |
225 apply( rule_tac [2] rtranclp.rtrancl_refl) |
226 apply( simp (no_asm)) |
226 apply( simp (no_asm)) |
227 |
227 |
228 -- "for Cast" |
228 -- "for Cast" |
229 defer 1 |
229 defer 1 |
230 |
230 |