explicit case names for rule list_induct2
authorhaftmann
Thu Mar 27 19:04:39 2008 +0100 (2008-03-27)
changeset 2644517223cf843d8
parent 26444 6a5faa5bcf19
child 26446 6abb5ed522a6
explicit case names for rule list_induct2
NEWS
src/HOL/Library/List_Prefix.thy
     1.1 --- a/NEWS	Thu Mar 27 19:04:38 2008 +0100
     1.2 +++ b/NEWS	Thu Mar 27 19:04:39 2008 +0100
     1.3 @@ -48,6 +48,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Class finite no longer treats UNIV as class parameter.  Use class enum from
     1.8 +theory Library/Enum instead to achieve a similar effect.  INCOMPATIBILITY.
     1.9 +
    1.10 +* Theory List: rule list_induct2 now has explicitly named cases "Nil" and "Cons".
    1.11 +INCOMPATIBILITY.
    1.12 +
    1.13  * HOL (and FOL): renamed variables in rules imp_elim and swap.
    1.14  Potential INCOMPATIBILITY.
    1.15  
     2.1 --- a/src/HOL/Library/List_Prefix.thy	Thu Mar 27 19:04:38 2008 +0100
     2.2 +++ b/src/HOL/Library/List_Prefix.thy	Thu Mar 27 19:04:39 2008 +0100
     2.3 @@ -355,15 +355,15 @@
     2.4    shows "xs \<parallel> ys"
     2.5    using len neq
     2.6  proof (induct rule: list_induct2)
     2.7 -  case 1
     2.8 +  case Nil
     2.9    then show ?case by simp
    2.10  next
    2.11 -  case (2 a as b bs)
    2.12 +  case (Cons a as b bs)
    2.13    have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact
    2.14    show ?case
    2.15    proof (cases "a = b")
    2.16      case True
    2.17 -    then have "as \<noteq> bs" using 2 by simp
    2.18 +    then have "as \<noteq> bs" using Cons by simp
    2.19      then show ?thesis by (rule Cons_parallelI2 [OF True ih])
    2.20    next
    2.21      case False