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
1998-02-09 nipkow 1998-02-09 Used THEN_ALL_NEW.
1998-02-07 paulson 1998-02-07 moved freeze_thaw to drule.ML
1998-02-07 paulson 1998-02-07 Tidying; rotate_prems; moved freeze_thaw from tactic.ML
1998-02-07 paulson 1998-02-07 AC and other rewrite rules for Un and Int
1998-02-07 paulson 1998-02-07 auto update
1998-02-07 paulson 1998-02-07 Added reference to rotate_prems
1998-02-06 nipkow 1998-02-06 filter_size -> length_filter
1998-02-06 nipkow 1998-02-06 Added `remdups' nodup -> nodups
1998-02-06 wenzelm 1998-02-06 added Vartab: TABLE;
1998-02-05 wenzelm 1998-02-05 added param;
1998-02-05 wenzelm 1998-02-05 added THEN_ALL_NEW;
1998-02-05 paulson 1998-02-05 New theorem Image_id
1998-02-05 paulson 1998-02-05 New theorem order_eq_refl
1998-02-05 paulson 1998-02-05 New max, min theorems
1998-02-05 paulson 1998-02-05 Added some more explicit guarantees of key secrecy for agents Deleted spurious A~=Spy assumptions
1998-02-05 paulson 1998-02-05 Fixed a lot of overfull and underfull lines (hboxes)
1998-02-05 paulson 1998-02-05 Updated the description of how to set up hyp_subst_tac
1998-02-02 paulson 1998-02-02 New example, Pow_Sigma_bij
1998-02-02 paulson 1998-02-02 fixed WWW links