| changeset 11292 | d838df879585 |
| parent 11237 | 0ef5ecc1fd4d |
| child 12631 | 7648ac4a6b95 |
| 11291:02db0084a695 | 11292:d838df879585 |
|---|---|
121 |
121 |
122 lemma "\<forall>xs. if xs = [] then A else B"; |
122 lemma "\<forall>xs. if xs = [] then A else B"; |
123 apply simp |
123 apply simp |
124 oops |
124 oops |
125 |
125 |
126 lemma "case xs @ [] of [] \<Rightarrow> A | y#ys \<Rightarrow> B"; |
126 lemma "case xs @ [] of [] \<Rightarrow> P | y#ys \<Rightarrow> Q ys y"; |
127 apply simp |
127 apply simp |
128 apply(simp split: list.split) |
128 apply(simp split: list.split) |
129 oops |
129 oops |
130 |
130 |
131 |
131 |