(* -*- isabelle-chosen-logic: "HOL" -*- *) theory ChosenLogic imports HOL begin end