isabelle2021-1: DSpecProofs

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2022-01-14 09:58:26 +11:00 · 2022-01-14 09:58:26 +11:00 · 96ec3d4372
parent be04eb0b50
commit 96ec3d4372
1 changed files with 2 additions and 2 deletions
--- a/proof/capDL-api/Retype_DP.thy
+++ b/proof/capDL-api/Retype_DP.thy
@ -463,10 +463,10 @@ lemma invoke_untyped_one_has_children:
        apply wp
       apply simp
      apply (clarsimp simp:neq_Nil_conv)
-        apply auto[1]
+        apply (cases slot, fastforce)
       apply wp+
     apply (rule hoare_strengthen_post[OF generate_object_ids_rv])
-     apply (clarsimp simp:zip_is_empty)
+     apply clarsimp
    apply (wp unlessE_wp hoare_drop_imps | simp)+
  done