(* Title: Containers/Equal.thy
Author: Andreas Lochbihler, KIT *)
theory Equal imports Main begin
section ‹
equal_base = fixes equal :: "'a → 'a → bool"
equal = equal_base +
assumes equal_eq: "equal = (=)"
equal_conv_eq: "equal x y ⟷ x = y"
(simp add: equal_eq)
¤ Dauer der Verarbeitung: 0.2 Sekunden
¤
*© Formatika GbR, Deutschland