# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263462439 -3600
# Node ID 2a19e0a37131edaf5e8da88e30e129cb28a11a1b
# Parent  ce5f78f0eac5d2715a59a759def6ba9ad793f41f
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.

diff -r ce5f78f0eac5 -r 2a19e0a37131 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Jan 14 10:06:29 2010 +0100
+++ b/Quot/QuotMain.thy	Thu Jan 14 10:47:19 2010 +0100
@@ -148,30 +148,6 @@
 use "quotient_tacs.ML"
 
 
-(* Atomize infrastructure *)
-(* FIXME/TODO: is this really needed? *)
-(*
-lemma atomize_eqv[atomize]:
-  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
-proof
-  assume "A \<equiv> B"
-  then show "Trueprop A \<equiv> Trueprop B" by unfold
-next
-  assume *: "Trueprop A \<equiv> Trueprop B"
-  have "A = B"
-  proof (cases A)
-    case True
-    have "A" by fact
-    then show "A = B" using * by simp
-  next
-    case False
-    have "\<not>A" by fact
-    then show "A = B" using * by auto
-  qed
-  then show "A \<equiv> B" by (rule eq_reflection)
-qed
-*)
-
 section {* Methods / Interface *}
 
 ML {*
diff -r ce5f78f0eac5 -r 2a19e0a37131 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Thu Jan 14 10:06:29 2010 +0100
+++ b/Quot/quotient_tacs.ML	Thu Jan 14 10:47:19 2010 +0100
@@ -57,7 +57,7 @@
 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
-fun quotient_tac ctxt = SOLVED'
+fun quotient_tac ctxt =
   (REPEAT_ALL_NEW (FIRST'
     [rtac @{thm identity_quotient},
      resolve_tac (quotient_rules_get ctxt)]))
diff -r ce5f78f0eac5 -r 2a19e0a37131 Unused.thy
--- a/Unused.thy	Thu Jan 14 10:06:29 2010 +0100
+++ b/Unused.thy	Thu Jan 14 10:47:19 2010 +0100
@@ -7,6 +7,30 @@
 
 
 
+(* Atomize infrastructure *)
+(* FIXME/TODO: is this really needed? *)
+(*
+lemma atomize_eqv:
+  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+proof
+  assume "A \<equiv> B"
+  then show "Trueprop A \<equiv> Trueprop B" by unfold
+next
+  assume *: "Trueprop A \<equiv> Trueprop B"
+  have "A = B"
+  proof (cases A)
+    case True
+    have "A" by fact
+    then show "A = B" using * by simp
+  next
+    case False
+    have "\<not>A" by fact
+    then show "A = B" using * by auto
+  qed
+  then show "A \<equiv> B" by (rule eq_reflection)
+qed
+*)
+
 
 ML {*
   fun dest_cbinop t =