equal
deleted
inserted
replaced
503 apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z") |
503 apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z") |
504 apply( erule exE) |
504 apply( erule exE) |
505 apply( rotate_tac -1, frule ssubst, erule_tac [2] asm_rl) |
505 apply( rotate_tac -1, frule ssubst, erule_tac [2] asm_rl) |
506 prefer 2 |
506 prefer 2 |
507 apply( rotate_tac -1, frule ssubst, erule_tac [2] asm_rl) |
507 apply( rotate_tac -1, frule ssubst, erule_tac [2] asm_rl) |
508 apply( tactic "asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1") |
508 apply( tactic "asm_full_simp_tac (HOL_ss addsimps [@{thm not_None_eq} RS sym]) 1") |
509 apply( simp_all (no_asm_simp) del: split_paired_Ex) |
509 apply( simp_all (no_asm_simp) del: split_paired_Ex) |
510 apply( frule (1) class_wf) |
510 apply( frule (1) class_wf) |
511 apply( simp (no_asm_simp) only: split_tupled_all) |
511 apply( simp (no_asm_simp) only: split_tupled_all) |
512 apply( unfold wf_cdecl_def) |
512 apply( unfold wf_cdecl_def) |
513 apply( drule map_of_SomeD) |
513 apply( drule map_of_SomeD) |