src/FOL/ROOT.ML
2009-11-11 wenzelm 2009-11-11 uniform use of simultabeous use_thys;
2009-07-09 wenzelm 2009-07-09 removed obsolete CVS Ids;
2007-05-31 wenzelm 2007-05-31 tuned header;
2007-05-31 wenzelm 2007-05-31 proper loading of ML files; removed obsolete IFOL.thy/FOL.thy values;
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 added updated version of IsaPlanner and substitution.
2006-01-06 wenzelm 2006-01-06 simplified EqSubst setup;
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-06-20 wenzelm 2005-06-20 removed obsolete print_depth;
2005-05-22 wenzelm 2005-05-22 Simplifier already setup in Pure;
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-04 wenzelm 2001-10-04 use "~~/src/Provers/induct_method.ML";
2000-09-07 wenzelm 2000-09-07 added Provers/rulify.ML;
2000-06-28 paulson 2000-06-28 new file Provers/make_elim.ML
1999-09-22 wenzelm 1999-09-22 tuned;
1999-08-25 wenzelm 1999-08-25 proper bootstrap of IFOL/FOL theories and packages;
1999-03-11 wenzelm 1999-03-11 removed foo_build_completed -- now handled by session management (via usedir);
1999-02-08 wenzelm 1999-02-08 ~~;
1998-08-13 paulson 1998-08-13 Blast_tac is faster
1998-07-30 wenzelm 1998-07-30 functorized Clasimp module;
1997-12-23 paulson 1997-12-23 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
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-11-12 oheimb 1997-11-12 added thin_refl to hyp_subst_tac
1997-11-12 wenzelm 1997-11-12 refer to $ISABELLE_HOME/src;
1997-11-06 paulson 1997-11-06 hyp_subst_tac checks if the equality has type variables and uses a suitable method if so. Affects the dest_eq function
1997-11-03 wenzelm 1997-11-03 moved cladata.ML, simpdata.ML to ROOT.ML;
1997-10-28 wenzelm 1997-10-28 do not change global_names flag;
1997-10-20 wenzelm 1997-10-20 reset global_names;
1997-07-25 wenzelm 1997-07-25 load simplifier.ML (again);
1997-07-09 wenzelm 1997-07-09 removed obsolete init_pps and init_thy_reader;
1997-04-02 paulson 1997-04-02 Now loads blast.ML
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-11-27 paulson 1996-11-27 Replaced obsolete "use" command
1996-02-28 paulson 1996-02-28 changed prove_goal to qed_goal
1996-01-29 clasohm 1996-01-29 expanded tabs
1995-11-21 clasohm 1995-11-21 removed make_chart from ROOT.ML; replaced exit_use by exit_use_dir
1995-10-24 clasohm 1995-10-24 added calls of init_html and make_chart
1995-10-04 clasohm 1995-10-04 removed command for loading Provers/simplifier.ML (now done in Pure/Thy/ROOT)
1995-04-06 lcp 1995-04-06 Set up for new hyp_subst_tac.
1994-11-24 lcp 1994-11-24 trivial changes
1994-10-31 lcp 1994-10-31 FOL/ROOT/FOL_dup_cs: removed as obsolete FOL/ROOT: no longer proves rev_cut_eq for hyp_subst_tac
1994-05-19 wenzelm 1994-05-19 thy reader now initialised by init_thy_reader();
1993-11-16 clasohm 1993-11-16 changed use_thy's parameter to exact theory name
1993-11-09 clasohm 1993-11-09 renamed int-prover.ML to intprover.ML, used exact theory names in ROOT.ML
1993-10-22 clasohm 1993-10-22 changes for new Readthy
1993-09-16 clasohm 1993-09-16 Initial revision