added minimal description of rep_cs

added minimal description of rep_ss

"choice" moved to Set.ML

New absorbsion laws, etc

Vimage

New vimage laws

added smart_tac

removed superfluous addss

New theory, Vimage

Proved choice and bchoice; changed Fun.thy -> thy

*** empty log message ***

added clasimp.ML;

renamed rep_claset to rep_cs

factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML explicitly introducing combined type clasimpset

changed wrapper mechanism of classical reasoner

added split_all_tac to claset()

changed wrapper mechanism of classical reasoner

New theory of the inverse image of a function

Added some lemmas.

Catches bad elim rules, handling exception OPTION

New laws for union

New laws for id

New induction schemas for lists (length and snoc).

*** empty log message ***

Congruence rules use == in premises now.

Congruence rules use == in premises now. New class linord.

minor improvements

re-arranged bindings for many function keys

extended input syntax to handle names of special keys

moved Ctrl entry before Alt entry extended input syntax to handle names of special keys

New theorem eq_imp_le

Four new Union/Intersection laws

corrected problem with auto_tac: now uses a variant of depth_tac that avoids interference of the simplifier with dup_step_tac

added New Jersey mirror;

Improved loop-test for rewrite rules a little. Should be done properly!

tuned comment;

added append (curried);

*** empty log message ***

Sign.merge vs. Sign.nontriv_merge;

tuned comments;

oops;

tuned print_cs;

updated;

tuned;

added explicit signature; improved comments;

improved comments;

fixed add_trrules: intern root;

export map_trrule;