1998-03-03 paulson 1998-03-03 New theorem diff_Suc_le_Suc_diff; tidied another proof
1998-03-03 paulson 1998-03-03 auto generated
1998-02-28 nipkow 1998-02-28 Modified def.
1998-02-28 nipkow 1998-02-28 Splitters via named loopers.
1998-02-28 nipkow 1998-02-28 Little reorganization. Loop tactics have names now.
1998-02-28 nipkow 1998-02-28 Tried to reorganize rewriter a little. More to be done.
1998-02-27 oheimb 1998-02-27 added minimal description of rep_cs: corrections
1998-02-27 oheimb 1998-02-27 added minimal description of rep_cs
1998-02-27 oheimb 1998-02-27 added minimal description of rep_ss
1998-02-27 paulson 1998-02-27 "choice" moved to Set.ML
1998-02-27 paulson 1998-02-27 New absorbsion laws, etc
1998-02-27 paulson 1998-02-27 Vimage
1998-02-27 paulson 1998-02-27 New vimage laws
1998-02-26 oheimb 1998-02-26 added smart_tac
1998-02-26 oheimb 1998-02-26 removed superfluous addss
1998-02-26 paulson 1998-02-26 New theory, Vimage
1998-02-26 paulson 1998-02-26 Proved choice and bchoice; changed Fun.thy -> thy
1998-02-26 wenzelm 1998-02-26 *** empty log message ***
1998-02-26 wenzelm 1998-02-26 added clasimp.ML;
1998-02-25 oheimb 1998-02-25 renamed rep_claset to rep_cs
1998-02-25 oheimb 1998-02-25 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
1998-02-25 oheimb 1998-02-25 changed wrapper mechanism of classical reasoner
1998-02-25 oheimb 1998-02-25 added split_all_tac to claset()
1998-02-25 oheimb 1998-02-25 changed wrapper mechanism of classical reasoner
1998-02-24 paulson 1998-02-24 New theory of the inverse image of a function
1998-02-24 nipkow 1998-02-24 Added some lemmas.
1998-02-23 paulson 1998-02-23 Catches bad elim rules, handling exception OPTION
1998-02-23 paulson 1998-02-23 New laws for union
1998-02-23 paulson 1998-02-23 New laws for id
1998-02-22 nipkow 1998-02-22 New induction schemas for lists (length and snoc).
1998-02-20 nipkow 1998-02-20 *** empty log message ***
1998-02-20 nipkow 1998-02-20 Congruence rules use == in premises now.
1998-02-20 nipkow 1998-02-20 Congruence rules use == in premises now. New class linord.
1998-02-20 oheimb 1998-02-20 minor improvements
1998-02-20 oheimb 1998-02-20 re-arranged bindings for many function keys
1998-02-20 oheimb 1998-02-20 extended input syntax to handle names of special keys
1998-02-20 oheimb 1998-02-20 moved Ctrl entry before Alt entry extended input syntax to handle names of special keys
1998-02-20 paulson 1998-02-20 New theorem eq_imp_le
1998-02-19 paulson 1998-02-19 Four new Union/Intersection laws
1998-02-18 oheimb 1998-02-18 corrected problem with auto_tac: now uses a variant of depth_tac that avoids interference of the simplifier with dup_step_tac
1998-02-18 wenzelm 1998-02-18 added New Jersey mirror;
1998-02-18 nipkow 1998-02-18 Improved loop-test for rewrite rules a little. Should be done properly!
1998-02-18 wenzelm 1998-02-18 tuned comment;
1998-02-13 wenzelm 1998-02-13 added append (curried);
1998-02-12 wenzelm 1998-02-12 *** empty log message ***
1998-02-12 wenzelm 1998-02-12 Sign.merge vs. Sign.nontriv_merge;
1998-02-12 wenzelm 1998-02-12 tuned comments;
1998-02-12 wenzelm 1998-02-12 oops;
1998-02-12 wenzelm 1998-02-12 tuned print_cs;
1998-02-12 wenzelm 1998-02-12 updated;
1998-02-12 wenzelm 1998-02-12 tuned;
1998-02-12 wenzelm 1998-02-12 added explicit signature; improved comments;
1998-02-12 wenzelm 1998-02-12 improved comments;
1998-02-12 wenzelm 1998-02-12 fixed add_trrules: intern root;
1998-02-12 wenzelm 1998-02-12 export map_trrule;
1998-02-12 wenzelm 1998-02-12 tuned add_trrules;
1998-02-12 wenzelm 1998-02-12 improved is_letter etc.;
1998-02-10 paulson 1998-02-10 New Addsimps for Compl rules
1998-02-10 paulson 1998-02-10 New AddIffs le_0_eq and neq0_conv
1998-02-09 nipkow 1998-02-09 Replaced ALLNEWSUBGOALS by THEN_ALL_NEW