150276Speter(* 2176187Srafan * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 350276Speter * 450276Speter * SPDX-License-Identifier: BSD-2-Clause 550276Speter *) 650276Speter 750276Spetertheory Crunch 850276Speterimports 950276Speter WPSimp 1050276Speter Lib 1150276Speter MLUtils 1250276Speterkeywords "crunch" "crunch_ignore" "crunches" :: thy_decl 1350276Speterbegin 1450276Speter 1550276Speternamed_theorems "crunch_def" 1650276Speternamed_theorems "crunch_rules" 1750276Speternamed_theorems "crunch_param_rules" 1850276Speter 1950276SpeterML_file "crunch-cmd.ML" 2050276SpeterML_file "Crunch.ML" 2150276Speter 2250276Speterend 2350276Speter