Gerwin Klein 449cfc702e 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 <gerwin.klein@proofcraft.systems>		2024-01-15 11:08:27 +11:00
..
BitFieldProofsLib.thy	all: adjust theory imports for TypHeapLib change	2023-01-25 10:13:45 +11:00
CCorresLemmas.thy	clib: further improvements to ccorres_While	2023-12-06 21:29:25 +10:30
CCorres_Rewrite.thy	clib+crefine: add no_name_eta to crefine tactics	2023-07-05 17:04:50 +10:00
CTranslationNICTA.thy	isabelle-2021: clib update	2021-09-30 16:53:17 +10:00
Corres_UL_C.thy	clib+crefine: improve and consolidate variants of ccorres_to_vcg	2023-10-17 13:54:56 +10:30
MonadicRewrite_C.thy	clib: generalise monadic_rewrite_ccorres_assemble	2023-04-27 08:12:31 +10:00
SIMPL_Lemmas.thy	clib: add some rules for hoarep	2023-10-17 13:54:56 +10:30
SimplRewrite.thy	isabelle-2021: clib update	2021-09-30 16:53:17 +10:00
Simpl_Rewrite.thy	clib: suppress simp warnings in simpl_rewrite	2024-01-15 11:08:27 +11:00
XPres.thy	clib: document some predicates used in `ceqv` and related automation	2021-03-19 13:01:44 +11:00