lemma restrict_complement_singleton_eq

some lemma refinements

added Table.thy

provide ProofContext.def_type depending on "pattern" mode;

record_type_tr': more robust strip_fields (printed types are not necessarily well-formed, e.g. in Syntax.pretty_arity);

record_type_abbr_tr': removed obsolete workaround for decode_type, which now retains syntactic categories of variables vs. constructors (authentic syntax);

eliminated Args.bang_facts (legacy feature);

eliminated old-style prems; tuned proofs;

removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);

Some notes on platform support of Isabelle.

"private" map_of_map lemma

added insort_insert

added dom_option_map, map_of_map_keys

added bulkload; tuned document

merged

merged

moved lemma map_sorted_distinct_set_unique

various refinements

print message when finiteness of domain definition is detected

merged

skip coinduction proofs for indirect-recursive domain definitions

merged

introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'

add comment

move take_proofs-related stuff to a new section

remove dead code

tuned dead code;

use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;

merged

fix proof script so 'domain foo = Foo foo' works