equal
deleted
inserted
replaced
1242 qed simp |
1242 qed simp |
1243 |
1243 |
1244 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])" |
1244 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])" |
1245 by(rule rev_cases[of xs]) auto |
1245 by(rule rev_cases[of xs]) auto |
1246 |
1246 |
|
1247 lemma length_Suc_conv_rev: "(length xs = Suc n) = (\<exists>y ys. xs = ys @ [y] \<and> length ys = n)" |
|
1248 by (induct xs rule: rev_induct) auto |
|
1249 |
1247 |
1250 |
1248 subsubsection \<open>\<^const>\<open>set\<close>\<close> |
1251 subsubsection \<open>\<^const>\<open>set\<close>\<close> |
1249 |
1252 |
1250 declare list.set[code_post] \<comment> \<open>pretty output\<close> |
1253 declare list.set[code_post] \<comment> \<open>pretty output\<close> |
1251 |
1254 |