TFL/tfl.sml
2000-09-06 wenzelm 2000-09-06 fixed structure U;
2000-09-05 wenzelm 2000-09-05 proper handling of hints; tuned;
2000-08-31 nipkow 2000-08-31 *** empty log message ***
2000-08-29 nipkow 2000-08-29 *** empty log message ***
2000-08-18 wenzelm 2000-08-18 proper handling of defs;
2000-08-17 nipkow 2000-08-17 installed recdef congs data
2000-07-13 wenzelm 2000-07-13 adapted PureThy.add_defs_i;
2000-05-05 wenzelm 2000-05-05 error msg: counting from one (again), in order to be consistent with case names of induction rule;
2000-04-15 nipkow 2000-04-15 mod to error msg
2000-03-31 wenzelm 2000-03-31 made SML/XL happy;
2000-03-31 nipkow 2000-03-31 comments modified
2000-03-30 nipkow 2000-03-30 the simplification rules returned from TFL are now paired with the row they came from.
2000-03-17 paulson 2000-03-17 better error messages, especially for multiple types
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.;
2000-03-08 wenzelm 2000-03-08 tuned error msg: rows counted from 1;
1999-10-21 wenzelm 1999-10-21 get_thm;
1999-10-04 wenzelm 1999-10-04 renamed 'prefix' to 'prfx' (avoids clash with infix);
1999-08-19 paulson 1999-08-19 removed needless comments
1999-08-18 paulson 1999-08-18 from Konrad: support for schematic definitions
1999-07-21 paulson 1999-07-21 better error message for curried recdefs, etc.
1999-05-03 paulson 1999-05-03 improved error handling
1999-04-23 paulson 1999-04-23 Now for recdefs that omit the WF relation; removed the separation between draft and theory modes
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-04-29 wenzelm 1998-04-29 adapted to new PureThy.add_defs;
1997-11-20 wenzelm 1997-11-20 tuned infer_types interface;
1997-11-12 wenzelm 1997-11-12 structure BasisLibrary;
1997-11-05 wenzelm 1997-11-05 fixed exception OPTION;
1997-11-01 paulson 1997-11-01 New way of referring to Basis Library
1997-10-28 wenzelm 1997-10-28 PureThy.add_store_defs_i;
1997-10-20 wenzelm 1997-10-20 lookup long names of types;
1997-10-17 wenzelm 1997-10-17 adapted to qualified names;
1997-10-01 wenzelm 1997-10-01 fully qualified names: Theory.add_XXX;
1997-09-25 paulson 1997-09-25 Deleted the unused gtake and recoded enumerate to use foldl
1997-06-23 paulson 1997-06-23 Removal of structure Context and its replacement by a theorem list of congruence rules for use in CONTEXT_REWRITE_RULE (where definitions are processed)
1997-06-05 paulson 1997-06-05 Numerous simplifications and removal of HOL-isms Addition of the "simpset" feature (replacing references to \!simpset)
1997-06-03 paulson 1997-06-03 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const Changed the TFL functor to a structure (currently called Prim)
1997-06-02 paulson 1997-06-02 Type inference makes a Const here, perhaps elsewhere?thry.sml
1997-06-02 paulson 1997-06-02 poly_tvars allows recdefs to be made without type constraints
1997-05-30 paulson 1997-05-30 Simplified the calling sequence of CONTEXT_REWRITE_RULE Eliminated get_rhs, which was calling dest_Trueprop too many times
1997-05-27 paulson 1997-05-27 Removal of module Mask and datatype binding with its constructor |->
1997-05-26 paulson 1997-05-26 Now checks the name of the function being defined; More de-HOL-ification
1997-05-22 paulson 1997-05-22 Now the recdef induction rule variables are named u, v, ...
1997-05-20 paulson 1997-05-20 Removal of redundant code (unused or already present in Isabelle. This eliminates HOL compatibility but makes the code smaller and more readable
1997-05-15 paulson 1997-05-15 TFL now integrated with HOL (more work needed)
1996-10-18 paulson 1996-10-18 Konrad Slind's TFL