1.1 --- a/src/HOL/Numeral.thy	Mon Oct 22 11:01:30 2001 +0200
     1.2 +++ b/src/HOL/Numeral.thy	Mon Oct 22 11:54:22 2001 +0200
     1.3 @@ -40,10 +40,10 @@
     1.4  lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
     1.5    by (simp add: Let_def)
     1.6  
     1.7 -(*The condition "True" is a hack to prevent looping.
     1.8 -  Conditional rewrite rules are tried after unconditional ones, so a rule
     1.9 -  like eq_nat_number_of will be tried first to eliminate #mm=#nn. *)
    1.10 -lemma number_of_reorient [simp]: "True ==> (number_of w = x) = (x = number_of w)"
    1.11 -  by auto
    1.12 +lemma Let_0 [simp]: "Let 0 f == f 0"
    1.13 +  by (simp add: Let_def)
    1.14 +
    1.15 +lemma Let_1 [simp]: "Let 1 f == f 1"
    1.16 +  by (simp add: Let_def)
    1.17  
    1.18  end