# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259836474 -3600
# Node ID abafefa0d58b951d80cd680b3a69d58d719e0836
# Parent  672b94510e7d07aae4b4003a16ea23e26051ce12
merged

diff -r 672b94510e7d -r abafefa0d58b IntEx.thy
--- a/IntEx.thy	Thu Dec 03 11:33:24 2009 +0100
+++ b/IntEx.thy	Thu Dec 03 11:34:34 2009 +0100
@@ -285,8 +285,6 @@
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
 apply(simp only: nil_prs)
-apply(rule test_all_prs)
-apply(tactic {* rtac quot 1 *})
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 done