--- a/Quot/Examples/IntEx.thy	Thu Dec 10 08:44:01 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Thu Dec 10 08:55:30 2009 +0100
@@ -113,6 +113,10 @@
   shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
 by (simp)
 
+lemma neg_rsp[quot_respect]:
+  shows "(op \<approx> ===> op \<approx>) my_neg my_neg"
+by simp
+
 lemma test1: "my_plus a b = my_plus a b"
 apply(rule refl)
 done
@@ -175,6 +179,27 @@
 apply(tactic {* clean_tac @{context} 1 *})
 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 ho_tst: "foldl my_plus x [] = x"
 apply simp
 done