| changeset 45129 | 1fce03e3e8ad |
| parent 44512 | 5e0f9e0e32fb |
| child 45343 | 873e9c0ca37d |
--- a/src/HOL/Quotient_Examples/FSet.thy Wed Oct 12 16:21:07 2011 +0200 +++ b/src/HOL/Quotient_Examples/FSet.thy Wed Oct 12 20:16:48 2011 +0200 @@ -1009,7 +1009,7 @@ lemma fset_raw_strong_cases: obtains "xs = []" | ys x where "\<not> List.member ys x" and "xs \<approx> x # ys" -proof (induct xs arbitrary: x ys) +proof (induct xs) case Nil then show thesis by simp next