src/Pure/logic.ML
Wed, 17 Jun 1998 10:48:38 +0200 nipkow Goals may now contain assumptions, which are not returned.
Wed, 22 Apr 1998 19:08:49 +0200 wenzelm added mk_cond_defpair, mk_defpair;
Mon, 09 Mar 1998 16:09:06 +0100 wenzelm adapted to baroque chars;
Wed, 04 Mar 1998 13:16:05 +0100 nipkow Reorganized simplifier. May now reorient rules.
Sat, 28 Feb 1998 15:40:03 +0100 nipkow Tried to reorganize rewriter a little. More to be done.
Wed, 18 Feb 1998 11:31:25 +0100 nipkow Improved loop-test for rewrite rules a little.
Fri, 19 Dec 1997 10:15:51 +0100 wenzelm term order stuff moved to term.ML;
Tue, 02 Dec 1997 12:42:28 +0100 wenzelm tuned term order;
Fri, 28 Nov 1997 07:35:10 +0100 nipkow Fixed the definition of `termord': is now antisymmetric.
Tue, 04 Nov 1997 12:58:10 +0100 nipkow logic: loops -> rewrite_rule_ok
Tue, 21 Oct 1997 17:36:54 +0200 nipkow Corrected alphabetical order of entries in signature.
Fri, 17 Oct 1997 11:10:13 +0200 paulson Added "op" before "occs" to make sml/nj happy
Thu, 16 Oct 1997 13:45:16 +0200 nipkow The simplifier has been improved a little: equations s=t which used to be
Thu, 05 Jun 1997 13:30:24 +0200 paulson Removal of freeze_vars and thaw_vars (quite unused...)
Thu, 16 Jan 1997 13:44:47 +0100 wenzelm added term order;
Thu, 28 Nov 1996 10:44:24 +0100 paulson Replaced map...~~ by ListPair.map
Fri, 28 Jun 1996 11:10:32 +0200 paulson Restored warning comment
Fri, 16 Feb 1996 12:19:47 +0100 paulson Elimination of fully-functorial style.
Mon, 29 Jan 1996 14:16:13 +0100 clasohm inserted tabs again
Mon, 29 Jan 1996 13:56:41 +0100 clasohm removed tabs
Wed, 12 Oct 1994 16:31:01 +0100 wenzelm added is_equals: term -> bool;
Tue, 06 Sep 1994 13:46:53 +0200 lcp Pure/type/unvarifyT: moved there from logic.ML
Thu, 18 Aug 1994 17:56:07 +0200 lcp /unvarifyT, unvarify: moved to Pure/logic.ML
Wed, 06 Jul 1994 11:36:00 +0200 wenzelm changed comment only;
Thu, 26 May 1994 16:40:45 +0200 wenzelm added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
Tue, 04 Jan 1994 15:48:38 +0100 wenzelm commented out sig constraint of functor (for debugging purposes);
Thu, 21 Oct 1993 14:56:12 +0100 lcp logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip