setup generic cases and induction (from Inductive.thy);

guillemot syntax;

improved internal interface of typedef;

abstract product types;

proper proof of split_paired_all (presently unused);

tuned comments;

added mk_UNIV;

tuned;

simplified exporter interface;

added implies_intr_goals;

tuned;

Tuned.

Removed exit command from end of main method.

PS method now calculates layout using default font metrics.

Inserted table for character widths.

tuned induction proofs;

dest_env: norm_term on rhs;

typedef: export result;

ignore typedef result;

declare projected induction rules stemming from nested recursion;

TypedefPackage.add_typedef_no_result;

tuned;

* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" (beware of argument permutation!);

option -o FILE --output to FILE (ps, eps, pdf);

ISABELLE_EPSTOPDF="epstopdf";

Font metrics used for batch mode layout (without X11 connection).

Added support for batch mode layout (without X11 connection).

tuned;

improved induct;

be more careful about token class markers;

proper order of kind names;

support impromptu terminology of cases parameters;

parser for underscore (actually a symbolic identifier!);

allow empty set/type name;

simplified resolveq_cases_tac for cases, separate version for induct; divinate instantiation of induct rules; tuned;

tuned;

canonical 'cases'/'induct' rules for n-tuples (n=3..7)

canonical 'cases'/'induct' rules for n-tuples (n=3..7) (really belongs to theory Product_Type, but doesn't work there yet)

setsum syntax;

intro! and elim! rules;

tuned NetRules;

Tactic.orderlist;

ObjectLogic.rulify;

Tactic.rewrite_cterm;

GPLed;

ring instead of ringS;

ring includes plus_ac0;

tuned;

support weight;

bang_args;

qualify some names;

map_nth_elem;

renamed reset_locs to del_locs

moved rulify to ObjectLogic;

moved rulify to ObjectLogic;

added qed_spec_mp etc.;