*** empty log message ***
authorwenzelm
Thu Feb 12 17:53:05 1998 +0100 (1998-02-12)
changeset 46280c7e97836e3c
parent 4627 ae95666c71cc
child 4629 401dd9b1b548
*** empty log message ***
src/HOL/List.ML
src/HOL/Power.thy
     1.1 --- a/src/HOL/List.ML	Thu Feb 12 17:43:53 1998 +0100
     1.2 +++ b/src/HOL/List.ML	Thu Feb 12 17:53:05 1998 +0100
     1.3 @@ -84,7 +84,7 @@
     1.4  qed "length_rev";
     1.5  Addsimps [length_rev];
     1.6  
     1.7 -goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = pred(length xs)";
     1.8 +goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = (length xs) - 1";
     1.9  by (exhaust_tac "xs" 1);
    1.10  by (ALLGOALS Asm_full_simp_tac);
    1.11  qed "length_tl";
     2.1 --- a/src/HOL/Power.thy	Thu Feb 12 17:43:53 1998 +0100
     2.2 +++ b/src/HOL/Power.thy	Thu Feb 12 17:53:05 1998 +0100
     2.3 @@ -19,7 +19,7 @@
     2.4    binomial_0   "(0     choose k) = (if k = 0 then 1 else 0)"
     2.5  
     2.6    binomial_Suc "(Suc n choose k) =
     2.7 -                (if k = 0 then 1 else (n choose pred k) + (n choose k))"
     2.8 +                (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
     2.9  
    2.10  end
    2.11