equal
deleted
inserted
replaced
58 declare card_insert_disjoint [simp del] |
58 declare card_insert_disjoint [simp del] |
59 |
59 |
60 lemma nat_1' [simp]: "nat 1 = 1" |
60 lemma nat_1' [simp]: "nat 1 = 1" |
61 by simp |
61 by simp |
62 |
62 |
63 (* For those annoying moments where Suc reappears *) |
63 (* For those annoying moments where Suc reappears, use Suc_eq_plus1 *) |
64 lemma Suc_remove: "Suc n = n + 1" |
|
65 by simp |
|
66 |
64 |
67 declare nat_1 [simp del] |
65 declare nat_1 [simp del] |
68 declare add_2_eq_Suc [simp del] |
66 declare add_2_eq_Suc [simp del] |
69 declare add_2_eq_Suc' [simp del] |
67 declare add_2_eq_Suc' [simp del] |
70 |
68 |