# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260272188 -3600
# Node ID df7a2f76daaeccc4f0bb500a44e9a165f9a8eb75
# Parent  c10a46fa0de96ecc246dbc130fddf77f564bbebc
Nitpick found a counterexample for one lemma.

diff -r c10a46fa0de9 -r df7a2f76daae Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 11:59:16 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 12:36:28 2009 +0100
@@ -1,5 +1,5 @@
 theory IntEx
-imports "../QuotList"
+imports "../QuotList" Nitpick
 begin
 
 fun
@@ -237,6 +237,7 @@
 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))"
 by simp
 
+(* Don't know how to keep the goal non-contracted... *)
 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
@@ -290,10 +291,8 @@
 
 lemma
   shows "equivp (op \<approx>)"
-  and   "equivp ((op \<approx>) ===> (op \<approx>))"
-apply -
-apply(tactic {* equiv_tac @{context} 1 *})
-apply(tactic {* equiv_tac @{context} 1 *})?
+  and "equivp ((op \<approx>) ===> (op \<approx>))"
+(* Nitpick finds a counterexample! *)
 oops
 
 lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
@@ -334,6 +333,6 @@
 apply(tactic {* quotient_tac @{context} 1 *})
 apply(tactic {* quotient_tac @{context} 1 *})
 apply(rule refl)
-done
+
 
 end