add lemmas Nats_cases and Nats_induct

generalize some lemmas, and remove a few unnecessary ones

generalize some lemmas from class linordered_ring_strict to linordered_ring

add case_names attribute to casedist and ind rules

add some lemmas about complete lattices

Digesting strings according to SHA-1.

proper int wrapping for Word32;

separate structure Typedecl;

modernized structure Object_Logic;

modernized structure Local_Defs;

merged

merged

simplified

merged

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