updated keywords;

more explicit axiomatization;

prefer vacuous definitional type classes over axiomatic ones;

more explicit axiomatization;

prefer vacuous definitional type classes over axiomatic ones;

comments;

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;

merged

check scalable fonts;

do *not* enforce scalable fonts for T1 encoding, instead rely on cm-super fonts, which also provide underscore for non-tt font;

yet another attempt at actual underscore; enforce scalable fonts for T1 encoding;

build up preprocessing context only once

tuned

disabled counterexample output for now; confusing because often incorrect

more indexing

merged

indexed document

Simplified some proofs, deleting a lot of strange unused material at the end of the theory.

fight spurious nitpick timeouts

reverted a87e49f4336d -- overwriting of data entries yields to merge problems later

more docs