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