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-14 nipkow 1994-01-14 optimized net for matching of abstractions to speed up simplifier
1994-01-11 nipkow 1994-01-11 optimized the number of eta-contractions in rewriting
1994-01-10 wenzelm 1994-01-10 commented out sig constraint of functor (for debugging purposes);
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 changed tracing of simplifier
1994-01-02 nipkow 1994-01-02 optimized simplifier - signature of rewritten term stays constant
1993-12-21 nipkow 1993-12-21 Necessary changes to accomodate type abbreviations.
1993-12-10 nipkow 1993-12-10 updated instantiate to deal with type clashes
1993-11-22 nipkow 1993-11-22 Fixed bug in rewriter (fun impc) discovered by Marcus Moore.
1993-11-11 nipkow 1993-11-11 Changed the simplifier: if the subgoaler proves an unexpected thm, chances are, it is an instance of the expected thm. Instead of aborting, rewriting now fails at that point.
1993-10-29 nipkow 1993-10-29 added function del_simps
1993-09-16 clasohm 1993-09-16 Initial revision