TFL/post.sml
2000-04-13 wenzelm use HOLogic.termT;
2000-03-31 nipkow comments modified
2000-03-30 nipkow the simplification rules returned from TFL are now paired with the row they
2000-03-20 paulson replaced best_tac by force_tac, allowing some arithmetic reasoning
1999-08-18 paulson from Konrad: support for schematic definitions
1999-04-30 wenzelm tuned defer_recdef interfaces;
1999-04-27 wenzelm proper quiet_mode;
1999-04-23 paulson Now for recdefs that omit the WF relation;
1999-04-22 wenzelm Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML;
1999-04-20 wenzelm temporarily reverted to 1.24;
1999-04-16 wenzelm Sign.base_name fid;
1999-04-14 wenzelm quiet_mode;
1999-03-17 wenzelm Theory.sign_of;
1999-03-10 paulson allow meta_outer to do nothing
1998-11-25 wenzelm replaced prs by writeln;
1998-06-30 berghofe Removed structure Prod_Syntax.
1998-05-27 paulson Changed require to requires for MLWorks
1998-04-29 wenzelm Theory.require;
1998-04-10 paulson can prove the empty relation to be WF
1997-11-03 wenzelm CLASET';
1997-10-23 wenzelm Sign.stamp_names_of;
1997-10-17 wenzelm adapted to qualified names;
1997-07-24 nipkow Replaced clumsy rewriting by the new function simplify on thms.
1997-07-23 wenzelm tmp fix to accomodate rep_ss changes;
1997-07-04 paulson Now catches the error of calling tgoalw when there are no goals to prove,
1997-06-23 paulson Removal of structure Context and its replacement by a theorem list of
1997-06-05 paulson Numerous simplifications and removal of HOL-isms
1997-06-03 paulson More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
1997-05-26 paulson Now checks the name of the function being defined
1997-05-22 paulson New headers and other minor changes
1997-05-21 paulson Basis library input/output primitives; currying the induction rule;
1997-05-20 paulson Removal of redundant code (unused or already present in Isabelle.
1997-05-16 paulson Subst now moved to directory HOL
1997-05-15 paulson TFL now integrated with HOL (more work needed)
1997-01-03 paulson Conversion to Basis Library (using prs instead of output)
1996-10-18 paulson Konrad Slind's TFL
less more (0) tip