--- a/Quot/Examples/IntEx2.thy	Thu Dec 10 08:44:01 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Thu Dec 10 08:55:30 2009 +0100
@@ -225,7 +225,7 @@
   shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
 by (simp add: equivp_reflp[OF int_equivp])
 
-lemma int_def:
+lemma int_of_nat:
   shows "of_nat m = int_of_nat m"
 apply (induct m)
 apply (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)
@@ -303,26 +303,6 @@
 apply(simp_all add: left_distrib add_strict_mono)
 done
 
-lemma int_induct_raw:
-  assumes a: "P (0::nat, 0)"
-  and     b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1,0))"
-  and     c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (uminus_raw (1,0)))"
-  shows      "P x"
-apply(case_tac x) apply(simp)
-apply(rule_tac x="b" in spec)
-apply(rule_tac Nat.induct)
-apply(rule allI)
-apply(rule_tac Nat.induct)
-using a b c apply(auto)
-done
-
-lemma int_induct:
-  assumes a: "P (0::int)"
-  and     b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
-  and     c: "\<And>i. P i \<Longrightarrow> P (i + (- 1))"
-  shows      "P x"
-using a b c by (lifting int_induct_raw)
-
 lemma zero_le_imp_eq_int_raw:
   fixes k::"(nat \<times> nat)"
   shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
@@ -335,8 +315,8 @@
 
 lemma zero_le_imp_eq_int:
   fixes k::int
-  shows "0 < k \<Longrightarrow> \<exists>n > 0. k = int_of_nat n"
-  unfolding less_int_def 
+  shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
+  unfolding less_int_def int_of_nat
   by (lifting zero_le_imp_eq_int_raw)
 
 lemma zmult_zless_mono2: 
@@ -346,7 +326,6 @@
 using a
 using a
 apply(drule_tac zero_le_imp_eq_int)
-apply(fold int_def)
 apply(auto simp add: zmult_zless_mono2_lemma)
 done