src/FOL/IsaMakefile
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-05-14 wenzelm 2011-05-14 modernized functor names; tuned;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-03-27 krauss 2011-03-27 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj"; adapted test configuration SML_makeall
2011-02-23 noschinl 2011-02-23 setup case_product attribute in HOL and FOL
2010-10-28 wenzelm 2010-10-28 moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; tuned;
2010-05-26 ballarin 2010-05-26 Revise locale test theory layout.
2010-05-12 wenzelm 2010-05-12 removed obsolete CVS Ids;
2009-07-24 wenzelm 2009-07-24 renamed functor BlastFun to Blast, require explicit theory; eliminated src/FOL/blastdata.ML;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-28 wenzelm 2009-02-28 moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
2009-02-28 wenzelm 2009-02-28 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
2009-02-16 wenzelm 2009-02-16 modernized some theory names;
2009-01-05 haftmann 2009-01-05 removed locale adaption layer
2008-12-19 ballarin 2008-12-19 All logics ported to new locales.
2008-11-21 ballarin 2008-11-21 Regression tests for new locale implementation.
2008-10-04 wenzelm 2008-10-04 replaced ISATOOL by ISABELLE_TOOL;
2008-06-14 wenzelm 2008-06-14 removed obsolete ML_SUFFIX; some reformatting;
2008-04-08 krauss 2008-04-08 fixed makefiles
2007-10-04 wenzelm 2007-10-04 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-07-22 wenzelm 2007-07-22 turned ex/prop.ML, ex/quant.ML into proper theories;
2007-05-31 wenzelm 2007-05-31 moved IsaPlanner from Provers to Tools;
2007-04-27 wenzelm 2007-04-27 removed obsolete induct/simp tactic;
2006-11-26 wenzelm 2006-11-26 converted legacy ML scripts;
2006-06-11 dixon 2006-06-11 updated IsaMakefiles for new location of IsaPlanner.
2006-06-07 wenzelm 2006-06-07 removed obsolete ML files;
2006-06-07 wenzelm 2006-06-07 removed obsolete ML files;
2006-01-06 wenzelm 2006-01-06 removed obsolete eqrule_FOL_data.ML;
2005-12-31 wenzelm 2005-12-31 removed obsolete Provers/make_elim.ML;
2005-12-22 wenzelm 2005-12-22 added Provers/project_rule.ML
2005-11-19 wenzelm 2005-11-19 FOL: -p 2;
2005-10-11 wenzelm 2005-10-11 ML_SUFFIX in targets (experimental);
2005-07-14 wenzelm 2005-07-14 removed FOL/ex/IffOracle.ML;
2005-06-01 ballarin 2005-06-01 Locales: new element constrains, parameter renaming with syntax, experimental command instantiate withdrawn.
2005-05-22 wenzelm 2005-05-22 Simplifier already setup in Pure;
2005-03-09 ballarin 2005-03-09 First version of global registration command.
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-04-02 ballarin 2004-04-02 Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>
2003-10-16 paulson 2003-10-16 partial conversion to Isar scripts
2003-08-15 paulson 2003-08-15 converting ex/If to Isar script
2002-08-30 paulson 2002-08-30 removal of blast.overloaded
2002-07-05 kleing 2002-07-05 added dependency for $(OUT)/Pure
2001-12-17 nipkow 2001-12-17 mods due to changed 1-point simprocs (quantifier1).
2001-12-05 wenzelm 2001-12-05 added ex/First_Order_Logic.thy, ex/document/root.tex;
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-04 wenzelm 2001-10-04 added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;
2000-09-07 wenzelm 2000-09-07 added Provers/rulify.ML;
2000-06-29 wenzelm 2000-06-29 improved arrangement of files; tuned;
2000-06-28 paulson 2000-06-28 new file Provers/make_elim.ML
1999-08-25 wenzelm 1999-08-25 proper bootstrap of IFOL/FOL theories and packages;
1998-03-06 wenzelm 1998-03-06 added clasimp.ML;
1998-01-07 wenzelm 1998-01-07 improved targets; fixed dependencies on parent logics;
1997-12-19 wenzelm 1997-12-19 log files; 'clean' target;
1997-12-03 paulson 1997-12-03 Instantiated the one-point-rule quantifier simpprocs for FOL New file fologic.ML holds abstract syntax operations Also, miniscoping provided for intuitionistic logic
1997-10-09 wenzelm 1997-10-09 removed declIffOracle;
1997-08-06 berghofe 1997-08-06 Removed reference to "thy_data.ML".
1997-07-07 wenzelm 1997-07-07 eliminated chmod -w;
1997-05-20 paulson 1997-05-20 new treatment of Prover files
1997-05-06 wenzelm 1997-05-06 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);