clib: suppress simp warnings in simpl_rewrite

This gets rid of the simplified warning for Collect_const that ccorres_rewrite produces in many CRefine proofs. Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Jan 12, 2024 · b63532b · b63532b
1 parent 939d2e7
commit b63532b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lib/clib/Simpl_Rewrite.thy b/lib/clib/Simpl_Rewrite.thy
@@ -460,7 +460,7 @@ text \<open>Methods to automate rewriting.\<close>
 
 method do_rewrite uses hom ruleset declares C_simp_simps =
   (rule com_ctxt_focus_rewrite[OF hom], rule ruleset,
-   #break "simpl_rewrite_rewrite", (simp add: C_simp_simps; fail))+
+   #break "simpl_rewrite_rewrite", (not_visible \<open>simp add: C_simp_simps\<close>; fail))+
 
 method rewrite_pre uses hom declares C_simp_pre C_simp_simps =
   (do_rewrite hom: hom ruleset: C_simp_pre)