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