1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Crunch 8imports 9 WPSimp 10 Lib 11 MLUtils 12keywords "crunch" "crunch_ignore" "crunches" :: thy_decl 13begin 14 15named_theorems "crunch_def" 16named_theorems "crunch_rules" 17named_theorems "crunch_param_rules" 18 19ML_file "crunch-cmd.ML" 20ML_file "Crunch.ML" 21 22end 23