# HG changeset patch # User haftmann # Date 1206641079 -3600 # Node ID 17223cf843d887ada4590858125cf7453a4e273a # Parent 6a5faa5bcf1926950c3310293bc3dc594b0ff3e1 explicit case names for rule list_induct2 diff -r 6a5faa5bcf19 -r 17223cf843d8 NEWS --- a/NEWS Thu Mar 27 19:04:38 2008 +0100 +++ b/NEWS Thu Mar 27 19:04:39 2008 +0100 @@ -48,6 +48,12 @@ *** HOL *** +* Class finite no longer treats UNIV as class parameter. Use class enum from +theory Library/Enum instead to achieve a similar effect. INCOMPATIBILITY. + +* Theory List: rule list_induct2 now has explicitly named cases "Nil" and "Cons". +INCOMPATIBILITY. + * HOL (and FOL): renamed variables in rules imp_elim and swap. Potential INCOMPATIBILITY. diff -r 6a5faa5bcf19 -r 17223cf843d8 src/HOL/Library/List_Prefix.thy --- a/src/HOL/Library/List_Prefix.thy Thu Mar 27 19:04:38 2008 +0100 +++ b/src/HOL/Library/List_Prefix.thy Thu Mar 27 19:04:39 2008 +0100 @@ -355,15 +355,15 @@ shows "xs \ ys" using len neq proof (induct rule: list_induct2) - case 1 + case Nil then show ?case by simp next - case (2 a as b bs) + case (Cons a as b bs) have ih: "as \ bs \ as \ bs" by fact show ?case proof (cases "a = b") case True - then have "as \ bs" using 2 by simp + then have "as \ bs" using Cons by simp then show ?thesis by (rule Cons_parallelI2 [OF True ih]) next case False