TFL/post.sml
2000-09-07 wenzelm 2000-09-07 use Rulify.rulify_no_asm;
2000-09-05 wenzelm 2000-09-05 proper handling of hints; tuned;
2000-08-30 nipkow 2000-08-30 Fixed rulify. As a result ?-vars in some recdef induction schemas were renamed.
2000-08-18 wenzelm 2000-08-18 proper handling of defs;
2000-08-17 nipkow 2000-08-17 installed recdef congs data
2000-07-25 nipkow 2000-07-25 Replaced force by fast because force may now take forever to fail (due to a recend change of David's)
2000-05-05 wenzelm 2000-05-05 tuned messages; use Sign.simple_read_term;
2000-04-14 wenzelm 2000-04-14 use HOLogic.termT;
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-20 paulson 2000-03-20 replaced best_tac by force_tac, allowing some arithmetic reasoning
1999-08-18 paulson 1999-08-18 from Konrad: support for schematic definitions
1999-04-30 wenzelm 1999-04-30 tuned defer_recdef interfaces;
1999-04-27 wenzelm 1999-04-27 proper quiet_mode; tuned messages;
1999-04-23 paulson 1999-04-23 Now for recdefs that omit the WF relation; removed the separation between draft and theory modes
1999-04-22 wenzelm 1999-04-22 Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML; Sign.base_name fid;
1999-04-20 wenzelm 1999-04-20 temporarily reverted to 1.24;
1999-04-16 wenzelm 1999-04-16 Sign.base_name fid;
1999-04-14 wenzelm 1999-04-14 quiet_mode;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-10 paulson 1999-03-10 allow meta_outer to do nothing
1998-11-25 wenzelm 1998-11-25 replaced prs by writeln;
1998-06-30 berghofe 1998-06-30 Removed structure Prod_Syntax.
1998-05-27 paulson 1998-05-27 Changed require to requires for MLWorks
1998-04-29 wenzelm 1998-04-29 Theory.require;
1998-04-10 paulson 1998-04-10 can prove the empty relation to be WF
1997-11-03 wenzelm 1997-11-03 CLASET';
1997-10-23 wenzelm 1997-10-23 Sign.stamp_names_of;
1997-10-17 wenzelm 1997-10-17 adapted to qualified names;
1997-07-24 nipkow 1997-07-24 Replaced clumsy rewriting by the new function simplify on thms.
1997-07-23 wenzelm 1997-07-23 tmp fix to accomodate rep_ss changes;
1997-07-04 paulson 1997-07-04 Now catches the error of calling tgoalw when there are no goals to prove, instead of just letting USyntax.list_mk_conj raise an exception
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-05-26 paulson 1997-05-26 Now checks the name of the function being defined
1997-05-22 paulson 1997-05-22 New headers and other minor changes
1997-05-21 paulson 1997-05-21 Basis library input/output primitives; currying the induction rule; removing & from the induction rule
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-16 paulson 1997-05-16 Subst now moved to directory HOL
1997-05-15 paulson 1997-05-15 TFL now integrated with HOL (more work needed)
1997-01-03 paulson 1997-01-03 Conversion to Basis Library (using prs instead of output)
1996-10-18 paulson 1996-10-18 Konrad Slind's TFL