isabelle: File revisions

src/HOL/ROOT.ML

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

isabelle

RSS Atom