* word_eqI is no longer rule_format.
* Updated Isabelle/ML Thm.join_proofs to Thm.consolidate.
* Updated suffix_refl to suffix_order.order.refl.
* Removed some lines of proofs, thanks to improved simplifier.
This was broken a long while back because arch_switch_to_idle_thread
might sometimes be skipped in the implementation if the idle thread
was previously scheduled. Putting the same behaviour in the most
abstract (unit) specification is pretty easy, and it's not clear why
it wasn't done earlier.
The things that usually go wrong:
- wp fall through: add +, e.g.
apply (wp select_wp) -> apply (wp select_wp)+
- precondition: you can remove most hoare_pre, but wpc still needs it, and
sometimes the wp instance relies on being able to fit a rule to the
current non-schematic precondition. In that case, use "including no_pre"
to switch off the automatic hoare_pre application.
- very rarely there is a schematic postcondition that interferes with the
new trivial cleanup rules, because the rest of the script assumes some
specific state afterwards (shouldn't happen in a reasonable proof, but
not all proofs are reasonable..). In that case, (wp_once ...)+ should
emulate the old behaviour precisely.
This commit should at least remove merge conflict markers, and the idea
is that at least refine, crefine, drefine, and infoflow (with sorrys)
build. Subsequent commits may be required to fix build issues that I
have not picked up.