src/Sequents/prover.ML
2010-08-17 haftmann 2010-08-17 more antiquotations
2009-10-21 haftmann 2009-10-21 curried inter as canonical list operation (beware of argument order)
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-11-21 wenzelm 2006-11-21 removed legacy ML setup;
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-09 wenzelm 2001-11-09 theory data: finish method;
1999-08-02 wenzelm 1999-08-02 cat_lines;
1999-07-28 paulson 1999-07-28 renamed ...thm_pack... to ...pack...
1999-07-27 paulson 1999-07-27 moved the modal prover to modal.ML; installed the prover using TheoryDataFun
1998-12-28 paulson 1998-12-28 added new arg for print_tac
1997-12-19 wenzelm 1997-12-19 adapted to new sort function;
1997-10-20 wenzelm 1997-10-20 adapted to qualified names;
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1996-10-09 paulson 1996-10-09 New unified treatment of sequent calculi by Sara Kalvala combines the old LK and Modal with the new ILL (Int. Linear Logic)