# HG changeset patch
# User paulson
# Date 1040119498 -3600
# Node ID 33b84d172c97068b56b458bf05257cc921a4cb0a
# Parent  41abb61ecce9a4065d4fb2531c1680f39a9eb13c
new int induction rules

diff -r 41abb61ecce9 -r 33b84d172c97 doc-src/TutorialI/Types/Numbers.thy
--- 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]}