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