equal
deleted
inserted
replaced
958 by(rule rev_cases[of xs]) auto |
958 by(rule rev_cases[of xs]) auto |
959 |
959 |
960 |
960 |
961 subsubsection {* @{text set} *} |
961 subsubsection {* @{text set} *} |
962 |
962 |
|
963 declare set.simps [code_post] --"pretty output" |
|
964 |
963 lemma finite_set [iff]: "finite (set xs)" |
965 lemma finite_set [iff]: "finite (set xs)" |
964 by (induct xs) auto |
966 by (induct xs) auto |
965 |
967 |
966 lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)" |
968 lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)" |
967 by (induct xs) auto |
969 by (induct xs) auto |