TFL/post.sml
Wed, 18 Aug 1999 18:44:20 +0200 paulson from Konrad: support for schematic definitions
Fri, 30 Apr 1999 18:08:58 +0200 wenzelm tuned defer_recdef interfaces;
Tue, 27 Apr 1999 10:52:25 +0200 wenzelm proper quiet_mode;
Fri, 23 Apr 1999 12:23:21 +0200 paulson Now for recdefs that omit the WF relation;
Thu, 22 Apr 1999 12:49:00 +0200 wenzelm Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML;
Tue, 20 Apr 1999 15:19:52 +0200 wenzelm temporarily reverted to 1.24;
Fri, 16 Apr 1999 14:43:26 +0200 wenzelm Sign.base_name fid;
Wed, 14 Apr 1999 19:07:39 +0200 wenzelm quiet_mode;
Wed, 17 Mar 1999 17:20:36 +0100 wenzelm Theory.sign_of;
Wed, 10 Mar 1999 10:43:59 +0100 paulson allow meta_outer to do nothing
Wed, 25 Nov 1998 14:04:05 +0100 wenzelm replaced prs by writeln;
Tue, 30 Jun 1998 20:57:46 +0200 berghofe Removed structure Prod_Syntax.
Wed, 27 May 1998 12:21:39 +0200 paulson Changed require to requires for MLWorks
Wed, 29 Apr 1998 11:33:06 +0200 wenzelm Theory.require;
Fri, 10 Apr 1998 13:40:29 +0200 paulson can prove the empty relation to be WF
Mon, 03 Nov 1997 12:36:48 +0100 wenzelm CLASET';
Thu, 23 Oct 1997 12:47:59 +0200 wenzelm Sign.stamp_names_of;
Fri, 17 Oct 1997 18:14:48 +0200 wenzelm adapted to qualified names;
Thu, 24 Jul 1997 11:13:12 +0200 nipkow Replaced clumsy rewriting by the new function simplify on thms.
Wed, 23 Jul 1997 10:34:18 +0200 wenzelm tmp fix to accomodate rep_ss changes;
Fri, 04 Jul 1997 12:32:31 +0200 paulson Now catches the error of calling tgoalw when there are no goals to prove,
Mon, 23 Jun 1997 11:33:59 +0200 paulson Removal of structure Context and its replacement by a theorem list of
Thu, 05 Jun 1997 13:27:28 +0200 paulson Numerous simplifications and removal of HOL-isms
Tue, 03 Jun 1997 11:08:08 +0200 paulson More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
Mon, 26 May 1997 12:28:30 +0200 paulson Now checks the name of the function being defined
Thu, 22 May 1997 15:13:16 +0200 paulson New headers and other minor changes
Wed, 21 May 1997 10:57:38 +0200 paulson Basis library input/output primitives; currying the induction rule;
Tue, 20 May 1997 11:49:57 +0200 paulson Removal of redundant code (unused or already present in Isabelle.
Fri, 16 May 1997 10:43:44 +0200 paulson Subst now moved to directory HOL
Thu, 15 May 1997 12:29:59 +0200 paulson TFL now integrated with HOL (more work needed)
Fri, 03 Jan 1997 10:45:31 +0100 paulson Conversion to Basis Library (using prs instead of output)
Fri, 18 Oct 1996 12:41:04 +0200 paulson Konrad Slind's TFL
less more (0) tip