src/FOLP/intprover.ML
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2013-06-26 wenzelm 2013-06-26 SOMEthing went utterly wrong;
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2008-03-18 wenzelm 2008-03-18 converted legacy ML scripts;
2007-09-15 haftmann 2007-09-15 fixed title
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2000-07-06 paulson 2000-07-06 removal of batch style, and tidying
1997-12-19 wenzelm 1997-12-19 adapted to new sort function;
1997-02-10 paulson 1997-02-10 Renamed structure Int (intuitionistic prover) to IntPr to prevent clash with Basis Library structure Int
1997-01-31 paulson 1997-01-31 ex_impE was incorrectly listed as Safe
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-29 clasohm 1996-01-29 expanded tabs
1993-09-16 clasohm 1993-09-16 Initial revision