new classical example from Lewis Carroll via S G Pulman

tuned mode_name; improved handling of assumptions; eliminated let_thms (named prop bindings moved to auto_bind.ML);

improved handling of assumptions;

facts: bind named props (from proof.ML/let_thms);

reset HOL_quantifiers by default;

Added lots of 'replicate' lemmas.

groups as monoids; tuned;

tuned comments;

added Ord.order_antisym;

auto_bind_goal, auto_bind_facts; varify_tfrees: no longer generalize types of free term variables; let_thms: no bindings;

auto_bind_goal, auto_bind_facts;

added get_st;

tuned;

varifyT': observe additional 'fixed' tfrees;

removed ObjectLogic.setup;

proper calculation;

renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;

fixed "...": dest_arg;

oops;

added order_le_less_trans, order_less_le_trans;

Calculation.thy: Setup transitivity rules for calculational proofs.

Support for calculational proofs.

added put_st;

added the_fact, level;

export multi_resolve;

added also, finally;

added 'also', 'finally' commands;

added COMP attribute;

added calculation.ML;

added Isar/calculation.ML;

fixed BUG in have_thmss: return thy';

added dest_main_statement;

print "..." variable;

no message "Adding axioms for datatype(s)";

added Group.thy;

added Isar_examples/Group.thy;

Some bits of group theory. Demonstrate calculational proofs.

read_term/prop_pat: do not freeze;

added dddot_tr;

added dddot_indexname;

"..." syntax;

find -print;

'kill' made improper;

improved print_state;

'note': Toplevel.print;

tuned markup;

broder size 3;

setup_goal: proper handling of non-atomic goals (include cprems into asms);

Isabelle manuals now also available as PDF;

move pdfs back into dist;

pdf docs;

separate archive for pdf docs;

\def\bold;

tuned formal comments;

tuned manual.bib;

changed {| |} verbatim syntax to {* *};

changed {| |} verbatim syntax to {* *} in order to simplify ProofGeneral setup;

improved undo / kill operations;

fixed corruptoin of end of file

removal of Always_StableI