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