1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Resurrect old "defs" command which was removed in Isabelle 2016. 8 * Should be replaced with overloading..definition..end blocks. *) 9 10theory Defs 11imports Main 12keywords "defs" :: thy_decl and "consts'" :: thy_decl 13begin 14 15ML_file "defs.ML" 16 17end 18 19