--- 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 =