Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
indexed document
merged
more indexing
disabled counterexample output for now; confusing because often incorrect
tuned
build up preprocessing context only once
yet another attempt at actual underscore;
enforce scalable fonts for T1 encoding;
do *not* enforce scalable fonts for T1 encoding, instead rely on cm-super fonts, which also provide underscore for non-tt font;
check scalable fonts;
merged
removed junk;
minimal document;
tidied messy proofs
dropped legacy finally
method names in instance declarations are always unqualified
restoring ancient string_classes option
more elementary put_simpset: exchange the simplifier configuration outright, which is particularly relevant concerning cumulative depth, e.g. for Product_Type.split_beta in the subsequent example:

  lemma "P (\<lambda>s. (case s of (x, y) \<Rightarrow> c))"
    using [[simp_depth_limit = 1]]
    apply simp
    oops
removed rotten code;
comments;