# HG changeset patch
# User haftmann
# Date 1234787897 -3600
# Node ID 0f0f5fb297ec92952f60013fc190c057a2d6c167
# Parent  80a9a55b0a0e5afc83315ce8d270bee7feda91ac# Parent  5d81dd706206aa8f3e16f18ea5e2a99c7d27f954
merged

diff -r 80a9a55b0a0e -r 0f0f5fb297ec src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Mon Feb 16 12:30:06 2009 +0100
+++ b/src/HOL/Library/Binomial.thy	Mon Feb 16 13:38:17 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Binomial.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Amine Chaieb
     Copyright   1997  University of Cambridge
 *)
@@ -13,11 +12,9 @@
 text {* This development is based on the work of Andy Gordon and
   Florian Kammueller. *}
 
-consts
-  binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat"      (infixl "choose" 65)
-primrec
+primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65) where
   binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)"
-  binomial_Suc: "(Suc n choose k) =
+  | binomial_Suc: "(Suc n choose k) =
                  (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
 
 lemma binomial_n_0 [simp]: "(n choose 0) = 1"
diff -r 80a9a55b0a0e -r 0f0f5fb297ec src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Mon Feb 16 12:30:06 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Mon Feb 16 13:38:17 2009 +0100
@@ -107,10 +107,10 @@
 
 lemma Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
   f n = (if n = 0 then g else h (n - 1))"
-  by (case_tac n) simp_all
+  by (cases n) simp_all
 
 lemma Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
-  by (case_tac n) simp_all
+  by (cases n) simp_all
 
 text {*
   The rules above are built into a preprocessor that is plugged into
@@ -132,7 +132,7 @@
       (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
     fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
     fun find_vars ct = (case term_of ct of
-        (Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
+        (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
       | _ $ _ =>
         let val (ct1, ct2) = Thm.dest_comb ct
         in 
@@ -236,7 +236,6 @@
   Codegen.add_preprocessor eqn_suc_preproc
   #> Codegen.add_preprocessor clause_suc_preproc
   #> Code.add_functrans ("eqn_Suc", lift eqn_suc_preproc)
-  #> Code.add_functrans ("clause_Suc", lift clause_suc_preproc)
 
 end;
 *}
diff -r 80a9a55b0a0e -r 0f0f5fb297ec src/HOL/ex/Codegenerator_Pretty.thy
--- a/src/HOL/ex/Codegenerator_Pretty.thy	Mon Feb 16 12:30:06 2009 +0100
+++ b/src/HOL/ex/Codegenerator_Pretty.thy	Mon Feb 16 13:38:17 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/Codegenerator_Pretty.thy
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 
diff -r 80a9a55b0a0e -r 0f0f5fb297ec src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Mon Feb 16 12:30:06 2009 +0100
+++ b/src/HOL/ex/Numeral.thy	Mon Feb 16 13:38:17 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/Numeral.thy
-    ID:         $Id$
     Author:     Florian Haftmann
 
 An experimental alternative numeral representation.
@@ -249,7 +248,7 @@
 
 text {*
   We embed binary representations into a generic algebraic
-  structure using @{text of_num}
+  structure using @{text of_num}.
 *}
 
 ML {*
@@ -891,7 +890,7 @@
 
 subsection {* Numeral equations as default simplification rules *}
 
-text {* TODO.  Be more precise here with respect to subsumed facts. *}
+text {* TODO.  Be more precise here with respect to subsumed facts.  Or use named theorems anyway. *}
 declare (in semiring_numeral) numeral [simp]
 declare (in semiring_1) numeral [simp]
 declare (in semiring_char_0) numeral [simp]