Theory ML_Conversion_Utils

✐‹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