From 4db52e9f2c5f951bdc3f3d5f6279e2d04129f10f Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Fri, 15 Mar 2024 21:49:53 +1030 Subject: [PATCH] lib/monads: rename assert_opt_ovalid to oassert_opt_ovalid and make [wp] Signed-off-by: Michael McInerney --- lib/Monads/reader_option/Reader_Option_VCG.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy index 7fd77e32c2..d7f77bae3f 100644 --- a/lib/Monads/reader_option/Reader_Option_VCG.thy +++ b/lib/Monads/reader_option/Reader_Option_VCG.thy @@ -129,7 +129,7 @@ lemma owhile_ovalid[wp]: apply auto done -lemma assert_opt_ovalid: +lemma oassert_opt_ovalid[wp]: "\\s. \y. x = Some y \ Q y s\ oassert_opt x \Q\" unfolding oassert_opt_def by (case_tac x; wpsimp)