# HG changeset patch
# User wenzelm
# Date 887302385 -3600
# Node ID 0c7e97836e3c1059e7851dcf49d4e04f8bb4c1c2
# Parent  ae95666c71cc075046b98c528de9df31dbcaad85
*** empty log message ***

diff -r ae95666c71cc -r 0c7e97836e3c src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Feb 12 17:43:53 1998 +0100
+++ b/src/HOL/List.ML	Thu Feb 12 17:53:05 1998 +0100
@@ -84,7 +84,7 @@
 qed "length_rev";
 Addsimps [length_rev];
 
-goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = pred(length xs)";
+goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = (length xs) - 1";
 by (exhaust_tac "xs" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "length_tl";
diff -r ae95666c71cc -r 0c7e97836e3c src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu Feb 12 17:43:53 1998 +0100
+++ b/src/HOL/Power.thy	Thu Feb 12 17:53:05 1998 +0100
@@ -19,7 +19,7 @@
   binomial_0   "(0     choose k) = (if k = 0 then 1 else 0)"
 
   binomial_Suc "(Suc n choose k) =
-                (if k = 0 then 1 else (n choose pred k) + (n choose k))"
+                (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
 
 end