equal
deleted
inserted
replaced
553 apply (elim crelE crel_nth crel_if crel_return crel_raise crel_new_weak) |
553 apply (elim crelE crel_nth crel_if crel_return crel_raise crel_new_weak) |
554 prefer 2 apply simp |
554 prefer 2 apply simp |
555 apply auto |
555 apply auto |
556 apply (drule fold_steps_correct) |
556 apply (drule fold_steps_correct) |
557 apply (simp add: correctArray_def array_ran_def) |
557 apply (simp add: correctArray_def array_ran_def) |
558 apply (cases "n = 0", auto) |
|
559 apply (rule implies_empty_inconsistent) |
558 apply (rule implies_empty_inconsistent) |
560 apply (simp add:correctArray_def) |
559 apply (simp add:correctArray_def) |
561 apply (drule bspec) |
560 apply (drule bspec) |
562 by (rule array_ranI, auto) |
561 by (rule array_ranI, auto) |
563 |
562 |