| changeset 63648 | f9f3006a5579 |
| parent 62002 | f1599e98c4d0 |
| child 67613 | ce654b0e6d69 |
| 63647:437bd400d808 | 63648:f9f3006a5579 |
|---|---|
23 |
23 |
24 |
24 |
25 subsection \<open>Arithmetic\<close> |
25 subsection \<open>Arithmetic\<close> |
26 |
26 |
27 lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))" |
27 lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))" |
28 by (simp add: diff_Suc split add: nat.split) |
28 by (simp add: diff_Suc split: nat.split) |
29 |
29 |
30 lemmas [simp] = hd_append set_lemmas |
30 lemmas [simp] = hd_append set_lemmas |
31 |
31 |
32 end |
32 end |