src/HOL/ROOT.ML
1999-03-17 wenzelm 1999-03-17 tuned;
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-11-27 nipkow 1998-11-27 At last: linear arithmetic for nat!
1998-10-20 wenzelm 1998-10-20 split_paired_all.ML;
1998-10-02 paulson 1998-10-02 new file Provers/Arith/abel_cancel.ML
1998-09-25 wenzelm 1998-09-25 tuned;
1998-09-18 paulson 1998-09-18 new files in Integ
1998-09-02 nipkow 1998-09-02 Added function upto to List. Had to rearrange loading sequence because now List uses Recdef.
1998-08-12 oheimb 1998-08-12 removed use_thys implied by use_thy "Main"
1998-07-30 wenzelm 1998-07-30 functorized Clasimp module;
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-03 wenzelm 1998-07-03 stepping stones: Recdef, Main; String now part of main HOL;
1998-07-02 wenzelm 1998-07-02 fixed Integ;
1998-07-01 berghofe 1998-07-01 Replaced "use_dir" command by "use", because nested calls of "use_dir" cause the HTML generator to crash.
1998-07-01 wenzelm 1998-07-01 tuned Inductive.thy;
1998-06-30 berghofe 1998-06-30 Adapted to new inductive definition package.
1998-06-25 paulson 1998-06-25 Installation of target HOL-Real
1998-05-05 paulson 1998-05-05 New syntax for function update; moved to main HOL directory
1998-04-29 wenzelm 1998-04-29 removed typedef.ML, record.ML; added Tools/typedef_package.ML, Tools/record_package.ML, Record.thy;
1998-03-30 oheimb 1998-03-30 removed superfluous use_thy
1998-01-14 wenzelm 1998-01-14 added record.ML;
1998-01-06 wenzelm 1998-01-06 tuned;
1997-11-28 nipkow 1997-11-28 Moved the quantifier elimination simp procs into Provers.
1997-11-26 wenzelm 1997-11-26 added Arith provers;
1997-11-12 wenzelm 1997-11-12 refer to $ISABELLE_HOME/src;
1997-11-03 wenzelm 1997-11-03 added thy_data; misc fixes;
1997-10-28 wenzelm 1997-10-28 do not change global_names flag;
1997-10-24 nipkow 1997-10-24 Added the new theory Map.
1997-10-20 wenzelm 1997-10-20 adapted to qualified 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-05-15 paulson 1997-05-15 Preliminary TFL versions
1997-04-02 paulson 1997-04-02 Now loads blast_tac
1996-10-21 nipkow 1996-10-21 Added trans_tac (see Provers/nat_transitive.ML)
1996-09-24 nipkow 1996-09-24 Moved Option out of IOA into core HOL
1996-09-12 paulson 1996-09-12 Now hologic.ML is loaded in HOL.ML
1996-02-19 nipkow 1996-02-19 Introduced normalize_thm into HOL.ML Corrected some dependencies among Sum, Prod and mono. Extended RelPow
1996-02-15 nipkow 1996-02-15 Added a few thms and the new theory RelPow.
1996-02-01 clasohm 1996-02-01 renamed subtype.ML to typedef.ML
1995-11-21 clasohm 1995-11-21 removed make_chart
1995-11-17 clasohm 1995-11-17 changed simpset of "HOL"
1995-10-25 nipkow 1995-10-25 Added various thms and tactics.
1995-10-24 clasohm 1995-10-24 added calls of init_html and make_chart
1995-10-06 regensbu 1995-10-06 added 8bit pragmas
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-06-29 clasohm 1995-06-29 renamed CHOL to HOL
1995-04-10 nipkow 1995-04-10 ROOT.ML: installed new hyp_subst_tac Nat.ML: Changed proof of lessE for new hyp_subst_tac
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application