--- 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.
--- 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 \<parallel> 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 \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact
show ?case
proof (cases "a = b")
case True
- then have "as \<noteq> bs" using 2 by simp
+ then have "as \<noteq> bs" using Cons by simp
then show ?thesis by (rule Cons_parallelI2 [OF True ih])
next
case False