TFL/tfl.sml
Thu, 21 Oct 1999 18:46:33 +0200 wenzelm get_thm;
Mon, 04 Oct 1999 21:41:09 +0200 wenzelm renamed 'prefix' to 'prfx' (avoids clash with infix);
Thu, 19 Aug 1999 15:13:37 +0200 paulson removed needless comments
Wed, 18 Aug 1999 18:44:20 +0200 paulson from Konrad: support for schematic definitions
Wed, 21 Jul 1999 15:16:32 +0200 paulson better error message for curried recdefs, etc.
Mon, 03 May 1999 11:19:08 +0200 paulson improved error handling
Fri, 23 Apr 1999 12:23:21 +0200 paulson Now for recdefs that omit the WF relation;
Wed, 17 Mar 1999 17:20:36 +0100 wenzelm Theory.sign_of;
Tue, 12 Jan 1999 13:54:51 +0100 wenzelm eliminated tthm type and Attribute structure;
Wed, 29 Apr 1998 11:33:27 +0200 wenzelm adapted to new PureThy.add_defs;
Thu, 20 Nov 1997 12:59:20 +0100 wenzelm tuned infer_types interface;
Wed, 12 Nov 1997 16:27:13 +0100 wenzelm structure BasisLibrary;
Wed, 05 Nov 1997 11:45:51 +0100 wenzelm fixed exception OPTION;
Sat, 01 Nov 1997 13:01:07 +0100 paulson New way of referring to Basis Library
Tue, 28 Oct 1997 17:56:57 +0100 wenzelm PureThy.add_store_defs_i;
Mon, 20 Oct 1997 11:14:16 +0200 wenzelm lookup long names of types;
Fri, 17 Oct 1997 18:14:48 +0200 wenzelm adapted to qualified names;
Wed, 01 Oct 1997 18:13:41 +0200 wenzelm fully qualified names: Theory.add_XXX;
Thu, 25 Sep 1997 12:24:53 +0200 paulson Deleted the unused gtake and recoded enumerate to use foldl
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, 02 Jun 1997 12:19:01 +0200 paulson Type inference makes a Const here, perhaps elsewhere?thry.sml
Mon, 02 Jun 1997 12:17:19 +0200 paulson poly_tvars allows recdefs to be made without type constraints
Fri, 30 May 1997 15:55:27 +0200 paulson Simplified the calling sequence of CONTEXT_REWRITE_RULE
Tue, 27 May 1997 13:22:30 +0200 paulson Removal of module Mask and datatype binding with its constructor |->
Mon, 26 May 1997 12:29:55 +0200 paulson Now checks the name of the function being defined;
Thu, 22 May 1997 15:11:56 +0200 paulson Now the recdef induction rule variables are named u, v, ...
Tue, 20 May 1997 11:49:57 +0200 paulson Removal of redundant code (unused or already present in Isabelle.
Thu, 15 May 1997 12:29:59 +0200 paulson TFL now integrated with HOL (more work needed)
Fri, 18 Oct 1996 12:41:04 +0200 paulson Konrad Slind's TFL
less more (0) tip