equal
deleted
inserted
replaced
91 code_pred [skip_proof] list_all2 |
91 code_pred [skip_proof] list_all2 |
92 proof - |
92 proof - |
93 case list_all2 |
93 case list_all2 |
94 from this show thesis |
94 from this show thesis |
95 apply - |
95 apply - |
96 apply (case_tac xa) |
|
97 apply (case_tac xb) |
96 apply (case_tac xb) |
|
97 apply (case_tac xc) |
98 apply auto |
98 apply auto |
99 apply (case_tac xb) |
99 apply (case_tac xc) |
100 apply auto |
100 apply auto |
|
101 apply fastsimp |
101 done |
102 done |
102 qed |
103 qed |
103 |
104 |
104 |
105 |
105 |
106 |