src/Pure/drule.ML
Mon, 31 Oct 1994 17:55:43 +0100 lcp Pure/drule/thin_rl: new
Tue, 25 Oct 1994 13:15:34 +0100 wenzelm minor change of occs_const in dest_defn;
Wed, 12 Oct 1994 16:38:58 +0100 wenzelm add_defs: improved error messages;
Tue, 23 Aug 1994 19:34:01 +0200 wenzelm added print_syntax: theory -> unit;
Fri, 19 Aug 1994 15:40:10 +0200 wenzelm added add_defs, add_defs_i;
Thu, 26 May 1994 16:43:48 +0200 wenzelm replaced ext_axtab by new_axioms;
Thu, 19 May 1994 16:17:46 +0200 wenzelm added print_sign, print_axioms: theory -> unit;
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