equal
deleted
inserted
replaced
138 by (metis split_list_last_prop[where P = P] in_set_conv_decomp) |
138 by (metis split_list_last_prop[where P = P] in_set_conv_decomp) |
139 |
139 |
140 lemma ex_tl: "EX ys. tl ys = xs" |
140 lemma ex_tl: "EX ys. tl ys = xs" |
141 using list.sel(3) by fast |
141 using list.sel(3) by fast |
142 |
142 |
143 lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)" |
143 lemma "(\<exists>ys::nat list. tl ys = xs) \<and> (\<exists>bs::int list. tl bs = as)" |
144 by (metis ex_tl) |
144 by (metis ex_tl) |
145 |
145 |
146 end |
146 end |