Theory Equal

(* Title:  Containers/Equal.thy
   Author: Andreas Lochbihler, KIT *)

theory Equal imports Main begin

section ‹Locales to abstract over HOL equality›

locale equal_base = fixes equal :: "'a ⇒ 'a ⇒ bool"

locale equal = equal_base +
  assumes equal_eq: "equal = (=)"
begin

lemma equal_conv_eq: "equal x y ⟷ x = y"
by(simp add: equal_eq)

end

end