src/Pure/drule.ML
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