Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
authorwenzelm
Thu, 12 Feb 1998 17:53:05 +0100
changeset 4628 0c7e97836e3c
parent 4627 ae95666c71cc
child 4629 401dd9b1b548
*** empty log message ***
src/HOL/List.ML file | annotate | diff | comparison | revisions
src/HOL/Power.thy file | annotate | diff | comparison | revisions 
--- 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";
--- 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
isabelle