✐‹creator "Kevin Kappelmann"› section ‹ML Conversion Utils› theory ML_Conversion_Utils imports Pure begin paragraph ‹Summary› text ‹Utilities for conversions.› lemma meta_eq_symmetric: "(A ≡ B) ≡ (B ≡ A)" by (rule equal_intr_rule) simp_all ML_file‹conversion_util.ML› end