(* -*- isabelle-chosen-logic: "HOL" -*- *)

theory ChosenLogic2 imports HOL
begin

end