equal
deleted
inserted
replaced
50 apply (rule int_int_eq [THEN iffD1]) |
50 apply (rule int_int_eq [THEN iffD1]) |
51 apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms) |
51 apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms) |
52 apply (simp only: number_of_BIT if_False zadd_0 zadd_assoc) |
52 apply (simp only: number_of_BIT if_False zadd_0 zadd_assoc) |
53 done |
53 done |
54 |
54 |
55 lemmas nat_number_of = |
55 lemmas nat_number = |
56 nat_number_of_Pls nat_number_of_Min |
56 nat_number_of_Pls nat_number_of_Min |
57 nat_number_of_BIT_True nat_number_of_BIT_False |
57 nat_number_of_BIT_True nat_number_of_BIT_False |
58 |
58 |
59 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" |
59 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" |
60 by (simp add: Let_def) |
60 by (simp add: Let_def) |