src/Pure/drule.ML
Thu, 03 Feb 1994 13:55:03 +0100 wenzelm removed eq_sg, pprint_sg, print_sg (now in sign.ML);
Tue, 18 Jan 1994 13:46:08 +0100 lcp Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
Wed, 05 Jan 1994 19:33:56 +0100 nipkow added new parameter to the simplification tactics which indicates if
Tue, 04 Jan 1994 17:03:52 +0100 nipkow added fake_cterm_of to speed up rewriting
Tue, 04 Jan 1994 15:48:38 +0100 wenzelm commented out sig constraint of functor (for debugging purposes);
Tue, 21 Dec 1993 14:47:29 +0100 wenzelm pretty_thm is now exported;
Thu, 21 Oct 1993 17:20:01 +0100 lcp Pure/drule/print_goals_ref: new, for Centaur interface
Fri, 24 Sep 1993 10:52:55 +0200 lcp Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip