(* * Copyright (c) 2023 Apple Inc. All rights reserved. * * SPDX-License-Identifier: BSD-2-Clause *) theory underscore_funs imports AutoCorres2_Main.AutoCorres_Main begin (* declare [[allow_underscore_idents]] *)