--- a/Attic/Quot/Examples/IntEx.thy	Fri Apr 23 09:54:42 2010 +0200
+++ b/Attic/Quot/Examples/IntEx.thy	Fri Apr 23 10:21:34 2010 +0200
@@ -165,27 +165,6 @@
 apply(lifting plus_assoc_pre)
 done
 
-lemma int_induct_raw:
-  assumes a: "P (0::nat, 0)"
-  and     b: "\<And>i. P i \<Longrightarrow> P (my_plus i (1,0))"
-  and     c: "\<And>i. P i \<Longrightarrow> P (my_plus i (my_neg (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 ZERO"
-  and     b: "\<And>i. P i \<Longrightarrow> P (PLUS i ONE)"
-  and     c: "\<And>i. P i \<Longrightarrow> P (PLUS i (NEG ONE))"
-  shows      "P x"
-  using a b c
-  by (lifting int_induct_raw)
-
 lemma ex1tst: "Bex1_rel (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)"
 sorry