--- 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 {*