1998-11-17 wenzelm 1998-11-17 export vars_of and friends; open BasicDrule only;
1998-10-20 wenzelm 1998-10-20 added unvarify(T);
1998-08-13 paulson 1998-08-13 Rule mk_triv_goal for making instances of triv_goal
1998-06-25 wenzelm 1998-06-25 added rewrite_cterm;
1998-04-04 wenzelm 1998-04-04 added triv_goal, rev_triv_goal (for Isar);
1998-03-10 nipkow 1998-03-10 New simplifier flag for mutual simplification.
1998-03-09 wenzelm 1998-03-09 Syntax.indexname;
1998-03-04 nipkow 1998-03-04 Reorganized simplifier. May now reorient rules. Moved loop tests from logic to thm.
1998-02-07 paulson 1998-02-07 Tidying; rotate_prems; moved freeze_thaw from tactic.ML
1998-01-30 wenzelm 1998-01-30 removed dead messy code;
1997-12-19 wenzelm 1997-12-19 adapted to new sort function;
1997-11-27 wenzelm 1997-11-27 removed same_thm;
1997-11-26 wenzelm 1997-11-26 cleaned signature; added instantiate': ctyp option list -> cterm option list -> thm -> thm;
1997-11-24 nipkow 1997-11-24 Added read_def_cterms for simultaneous reading/typing of terms under defaults. Redefined read_def_cterm in in terms of read_def_cterms. Deleted obsolete read_cterms. Cleaned up def of read_insts, which is not much shorter but much clearere are correcter now.
1997-11-21 wenzelm 1997-11-21 changed Sequence interface (now Seq, in seq.ML);
1997-11-01 wenzelm 1997-11-01 propagate exn msg;
1997-10-28 wenzelm 1997-10-28 eq_thm moved to thm.ML; store ProtoPure lemmas;
1997-10-24 wenzelm 1997-10-24 ProtoPure.thy;
1997-10-01 wenzelm 1997-10-01 moved theory stuff (add_defs etc.) to theory.ML;
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);