removed rotten code;

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

merged

improved lin.arith. for terms involving division

restoring ancient string_classes option

method names in instance declarations are always unqualified

dropped legacy finally

tidied messy proofs

minimal document;

removed junk;