mirror of https://github.com/seL4/l4v.git
dbf5a2a865
This involved the following sed commands, with care taken to avoid unnecessary rewrites in lib/Monads and lib/StateMonad.thy sed -i 's/hoare_post_taut/hoare_TrueI/g' **/*.thy sed -i 's/hoare_TrueI\s*\[where P=\\<top>\]/wp_post_taut/g' proof/**/*.thy sed -i 's/hoare_post_imp_R/hoare_strengthen_postE_R/g' **/*.thy sed -i 's/hoare_seq_ext\b/bind_wp/g' **/*.thy sed -i 's/bind_wp\s*\[rotated\]/bind_wp_fwd/g' **/*.thy sed -i 's/hoare_vcg_precond_imp/hoare_weaken_pre/g' **/*.thy sed -i 's/hoare_vcg_seqE/bindE_wp/g' **/*.thy sed -i 's/bindE_wp\s*\[rotated\]/bindE_wp_fwd/g' **/*.thy sed -i 's/validE_weaken/hoare_chainE/g' **/*.thy sed -i 's/validE_weaken/hoare_chainE/g' **/*.ML sed -i 's/seqE/bindE_wp_fwd/g' **/*.thy sed -i 's/bindE_wp_fwd\s*\[rotated\]/bindE_wp/g' **/*.thy sed -i 's/hoare_True_E_R/hoareE_R_TrueI/g' **/*.thy sed -i -e 's/hoareE_R_TrueI\[where P="\\<top>"\]/wp_post_tautE_R/g' **/*.thy sed -i "s/hoare_post_impErr'/hoare_strengthen_postE/g" **/*.thy sed -i 's/hoare_post_impErr/hoare_strengthen_postE/g' **/*.thy sed -i 's/hoare_vcg_all_lift_R/hoare_vcg_all_liftE_R/g' **/*.thy sed -i 's/hoare_seq_ext_skip/bind_wp_fwd_skip/g' **/*.thy sed -i 's/True_E_E/wp_post_tautE_E/g' **/*.thy sed -i 's/\bseq_ext/bind_wp_fwd/g' proof/**/*.thy Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems> |
||
|---|---|---|
| .. | ||
| examples | ||
| Atomicity_Lib.thy | ||
| Prefix_Refinement.thy | ||
| Triv_Refinement.thy | ||