151 (* Atomize infrastructure *)

   152 (* FIXME/TODO: is this really needed? *)

   153 (*

   154 lemma atomize_eqv[atomize]:

   155   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"

   156 proof

   157   assume "A \<equiv> B"

   158   then show "Trueprop A \<equiv> Trueprop B" by unfold

   159 next

   160   assume *: "Trueprop A \<equiv> Trueprop B"

   161   have "A = B"

   162   proof (cases A)

   163     case True

   164     have "A" by fact

   165     then show "A = B" using * by simp

   166   next

   167     case False

   168     have "\<not>A" by fact

   169     then show "A = B" using * by auto

   170   qed

   171   then show "A \<equiv> B" by (rule eq_reflection)

   172 qed

   173 *)

   174