TFL/post.ML
2003-10-17 paulson 2003-10-17 improved tracing
2002-08-13 nipkow 2002-08-13 arith_tac should not produce counter example
2001-12-13 nipkow 2001-12-13 Terminator now uses arith_tac as well.
2001-12-03 wenzelm 2001-12-03 HOLogic.read_cterm;
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-09-28 wenzelm 2001-09-28 prove: ``strict'' argument;
2001-02-02 wenzelm 2001-02-02 tuned;
2001-01-03 wenzelm 2001-01-03 renamed .sml files to .ML; proper handling of Isabelle exceptions; tuned;