--- a/doc-src/TutorialI/Types/Numbers.thy Tue Dec 17 11:04:30 2002 +0100
+++ b/doc-src/TutorialI/Types/Numbers.thy Tue Dec 17 11:04:58 2002 +0100
@@ -132,8 +132,10 @@
\rulename{dvd_add}
For the integers, I'd list a few theorems that somehow involve negative
-numbers.
+numbers.*}
+
+text{*
Division, remainder of negatives
@@ -177,6 +179,22 @@
lemma "abs (2*x) = 2 * abs (x :: int)"
by (simp add: zabs_def)
+
+text {*Induction rules for the Integers
+
+@{thm[display] int_ge_induct[no_vars]}
+\rulename{int_ge_induct}
+
+@{thm[display] int_gr_induct[no_vars]}
+\rulename{int_gr_induct}
+
+@{thm[display] int_le_induct[no_vars]}
+\rulename{int_le_induct}
+
+@{thm[display] int_less_induct[no_vars]}
+\rulename{int_less_induct}
+*}
+
text {*REALS
@{thm[display] realpow_abs[no_vars]}