equal
deleted
inserted
replaced
552 by (cases z) |
552 by (cases z) |
553 (simp add: of_int add minus int_def diff_minus) |
553 (simp add: of_int add minus int_def diff_minus) |
554 qed |
554 qed |
555 |
555 |
556 lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z" |
556 lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z" |
557 by (cases z rule: eq_Abs_Integ, simp add: nat le of_int Zero_int_def) |
557 by (cases z rule: eq_Abs_Integ) |
|
558 (simp add: nat le of_int Zero_int_def of_nat_diff) |
558 |
559 |
559 |
560 |
560 subsection{*The Set of Integers*} |
561 subsection{*The Set of Integers*} |
561 |
562 |
562 constdefs |
563 constdefs |