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

theory ChosenLogic imports HOL
begin

end


