1997-09-02 nipkow 1997-09-02 Added Larry's equal_intr_rule
1997-07-25 wenzelm 1997-07-25 improved rewrite_thm / rewrite_goals to handle conditional eqns;
1997-07-23 wenzelm 1997-07-23 added rewrite_thm;
1997-07-18 wenzelm 1997-07-18 defs: allow conditions;
1997-02-21 paulson 1997-02-21 Replaced "flat" by the Basis Library function List.concat
1996-11-28 paulson 1996-11-28 Replaced map...~~ by
1996-11-13 paulson 1996-11-13 Removal of polymorphic equality via mem, subset, eq_set, etc
1996-11-01 paulson 1996-11-01 Now uses Int.max instead of max
1996-09-23 paulson 1996-09-23 New operations on cterms. Now same names as in Logic
1996-08-12 paulson 1996-08-12 Improved (?) wording of error message
1996-05-22 nipkow 1996-05-22 Added swap_prems_rl
1996-04-30 clasohm 1996-04-30 moved dest_cimplies to drule.ML; added adjust_maxidx
1996-03-21 paulson 1996-03-21 Printing & string functions moved to display.ML
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1996-01-15 wenzelm 1996-01-15 improved printing of errors in 'defs'; fixed small bug in 'standard' (it used to fail stripping shyps in some cases);
1996-01-11 nipkow 1996-01-11 Removed bug in type unification. Negative indexes are not used any longer. Had to change interface to Type.unify to pass maxidx. Thus changes in the clients.
1995-12-22 paulson 1995-12-22 Now "standard" compresses theorems (for sharing). Also, rewrite_rule and rewrite_goals_rule check for the empty list of rewrites and do nothing in that case.
1995-09-01 clasohm 1995-09-01 added same_sg and same_thm
1995-09-01 wenzelm 1995-09-01 adapted to new version of shyps-stuff;
1995-08-01 wenzelm 1995-08-01 modified pretty_thm, standard, eq_thm to handle shyps;
1995-07-25 lcp 1995-07-25 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
1995-03-14 nipkow 1995-03-14 Removed an old bug which made some simultaneous instantiations fail if they were given in the "wrong" order. Rewrote sign/infer_types. Fixed some comments.
1995-03-13 nipkow 1995-03-13 Changed treatment of during type inference internally generated type variables. 1. They are renamed to 'a, 'b, 'c etc away from a given set of used names. 2. They are either frozen (turned into TFrees) or left schematic (TVars) depending on a parameter. In goals they are frozen, for instantiations they are left schematic.
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-01-11 wenzelm 1995-01-11 removed print_sign, print_axioms;
1994-12-09 wenzelm 1994-12-09 improved axioms_of: returns thms as the manual says;
1994-11-14 lcp 1994-11-14 Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
1994-10-31 lcp 1994-10-31 Pure/drule/thin_rl: new
1994-10-25 wenzelm 1994-10-25 minor change of occs_const in dest_defn;
1994-10-12 wenzelm 1994-10-12 add_defs: improved error messages; installed new print_goals with nice 'env mode';
1994-08-23 wenzelm 1994-08-23 added print_syntax: theory -> unit;
1994-08-19 wenzelm 1994-08-19 added add_defs, add_defs_i;
1994-05-26 wenzelm 1994-05-26 replaced ext_axtab by new_axioms;
1994-05-19 wenzelm 1994-05-19 added print_sign, print_axioms: theory -> unit; replaced ["logic"] by logicS;
1994-02-03 wenzelm 1994-02-03 removed eq_sg, pprint_sg, print_sg (now in sign.ML); removed cterm_fun, read_ctyp (now in thm.ML); print_theory: now shows all contents;
1994-01-18 lcp 1994-01-18 Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated functions from sign.ML to thm.ML or drule.ML. This allows the "prop" field of a theorem to be regarded as a cterm -- avoids expensive calls to cterm_of.
1994-01-05 nipkow 1994-01-05 added new parameter to the simplification tactics which indicates if assumptions are to be simplified and/or to be used when simplifying the conclusion. This gets rid of METAHYPS and speeds up simplification of goals with big assumptions.
1994-01-04 nipkow 1994-01-04 added fake_cterm_of to speed up rewriting
1994-01-04 wenzelm 1994-01-04 commented out sig constraint of functor (for debugging purposes);
1993-12-21 wenzelm 1993-12-21 pretty_thm is now exported;
1993-10-21 lcp 1993-10-21 Pure/drule/print_goals_ref: new, for Centaur interface Pure/tctical/tracify,print_tac: now call !print_goals_ref Pure/goals/print_top,prepare_proof: now call !print_goals_ref
1993-09-24 lcp 1993-09-24 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a rule's premises against a list of other proofs.
1993-09-16 clasohm 1993-09-16 Initial revision