1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory WPSimp
8imports
9  "WP"
10  "WPC"
11  "WPFix"
12  Simp_No_Conditional
13begin
14
15(* Wrap up the standard usage pattern of wp/wpc/simp into its own command: *)
16method wpsimp uses wp wp_del simp simp_del split split_del cong comb comb_del =
17  ((determ \<open>wpfix | wp add: wp del: wp_del comb: comb comb del: comb_del | wpc |
18            clarsimp_no_cond simp: simp simp del: simp_del split: split split del: split_del cong: cong |
19            clarsimp simp: simp simp del: simp_del split: split split del: split_del cong: cong\<close>)+)[1]
20
21end