new settings for afp test

Heap_Monad uses Monad_Syntax

State_Monad uses Monad_Syntax

uniform do notation for monads

generic ad-hoc overloading via check/uncheck

corrected title

theorem collections do not contain default rules any longer

fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions; added tests for Ball/Bex

removed unused/untested IOA 'automaton' package;

removed impractical tolerate_legacy_features flag;

tuned comment;

removed legacy aliases;

moved misc legacy stuff from OldGoals to Misc_Legacy; OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;

eliminated OldGoals.strip_context;

removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years;

do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel; use up-to-date ML_Compiler.exn_message;

some modernization of really ancient Meson experiments;

dropped empty theory

moved auxiliary lemma

dropped unused lemmas of dubious value

dropped unused lemmas of dubious value

split off mrec into separate theory

spelt out relational framework in a consistent way

avoid explicit mandatory prefix markers when prefixes are mandatory implicitly

merged

moved co-regularity to class section; avoid duplicated class_deps

dropped superfluous [code del]s

merged