equal
deleted
inserted
replaced
563 apply (erule (1) subcls1_induct) |
563 apply (erule (1) subcls1_induct) |
564 |
564 |
565 apply clarify |
565 apply clarify |
566 apply (frule wf_prog_ws_prog) |
566 apply (frule wf_prog_ws_prog) |
567 apply (frule fields_Object, assumption+) |
567 apply (frule fields_Object, assumption+) |
568 apply (simp only: is_class_Object) apply simp |
568 apply (simp only: is_class_Object) |
569 |
569 |
570 apply clarify |
570 apply clarify |
571 apply (frule fields_rec) |
571 apply (frule fields_rec) |
572 apply (simp (no_asm_simp) add: wf_prog_ws_prog) |
572 apply (simp (no_asm_simp) add: wf_prog_ws_prog) |
573 |
573 |