isabelle: File revisions

src/HOL/ROOT.ML

2009-11-11	wenzelm	2009-11-11	uniform use of simultabeous use_thys;	file \| diff \| annotate
2009-10-24	bulwahn	2009-10-24	processing of tuples in introduction rules	file \| diff \| annotate
2009-02-26	wenzelm	2009-02-26	back to canonical ROOT, to see if memory problems still persist;	file \| diff \| annotate
2009-01-27	wenzelm	2009-01-27	added share_common_data -- reduces heap space, but takes long;	file \| diff \| annotate
2009-01-11	wenzelm	2009-01-11	load main entry points sequentially, for reduced memory demands;	file \| diff \| annotate
2009-01-02	wenzelm	2009-01-02	tuned header and description of boot files;	file \| diff \| annotate
2008-12-19	ballarin	2008-12-19	All logics ported to new locales.	file \| diff \| annotate
2008-12-14	ballarin	2008-12-14	Ported HOL and HOL-Library to new locales.	file \| diff \| annotate
2008-12-05	haftmann	2008-12-05	corrected theory path	file \| diff \| annotate
2008-12-03	haftmann	2008-12-03	made repository layout more coherent with logical distribution structure; stripped some $Id$s	file \| diff \| annotate
2008-09-17	wenzelm	2008-09-17	moved global ML bindings to global place;	file \| diff \| annotate
2008-07-01	haftmann	2008-07-01	HOL += HOL-Complex	file \| diff \| annotate
2008-06-26	haftmann	2008-06-26	established Plain theory and image	file \| diff \| annotate
2008-01-25	haftmann	2008-01-25	consistent interacitve bootstrap of HOL-Main	file \| diff \| annotate
2007-07-21	wenzelm	2007-07-21	tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);	file \| diff \| annotate
2007-05-31	wenzelm	2007-05-31	proper loading of ML files (in HOL.thy); moved Integ files to canonical place; misc cleanup;	file \| diff \| annotate
2007-05-17	haftmann	2007-05-17	canonical prefixing of class constants	file \| diff \| annotate
2007-05-13	haftmann	2007-05-13	added modules rat.ML and int.ML	file \| diff \| annotate
2006-12-27	haftmann	2006-12-27	removed Main.thy	file \| diff \| annotate
2006-11-08	wenzelm	2006-11-08	added structure Main (from Main.ML);	file \| diff \| annotate
2006-06-11	dixon	2006-06-11	added updated version of IsaPlanner and substitution.	file \| diff \| annotate
2006-03-02	paulson	2006-03-02	moved the "use" directive	file \| diff \| annotate
2006-03-01	mengj	2006-03-01	Added file Tools/res_atpset.ML.	file \| diff \| annotate
2006-01-06	wenzelm	2006-01-06	simplified EqSubst setup;	file \| diff \| annotate
2005-12-31	wenzelm	2005-12-31	removed obsolete Provers/make_elim.ML;	file \| diff \| annotate
2005-12-22	wenzelm	2005-12-22	added Provers/project_rule.ML	file \| diff \| annotate
2005-12-21	paulson	2005-12-21	new hash table module in HOL/Too/s	file \| diff \| annotate
2005-12-16	paulson	2005-12-16	hashing to eliminate the output of duplicate clauses	file \| diff \| annotate
2005-10-19	wenzelm	2005-10-19	removed obsolete HOL/thy_syntax.ML;	file \| diff \| annotate
2005-06-24	paulson	2005-06-24	deleted a redundant "use" line	file \| diff \| annotate
2005-06-20	wenzelm	2005-06-20	removed obsolete print_depth;	file \| diff \| annotate
2005-05-22	wenzelm	2005-05-22	Simplifier already setup in Pure;	file \| diff \| annotate
2004-12-02	paulson	2004-12-02	new CLAUSIFY attribute for proof reconstruction with lemmas	file \| diff \| annotate
2004-12-01	paulson	2004-12-01	resolution package tools by Jia Meng	file \| diff \| annotate
2004-08-03	ballarin	2004-08-03	New transitivity reasoners for transitivity only and quasi orders.	file \| diff \| annotate
2004-02-19	ballarin	2004-02-19	Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.	file \| diff \| annotate
2004-02-15	paulson	2004-02-15	Polymorphic treatment of binary arithmetic using axclasses	file \| diff \| annotate
2002-11-28	ballarin	2002-11-28	HOL-Algebra partially ported to Isar.	file \| diff \| annotate
2002-08-23	nipkow	2002-08-23	Added div+mod cancelling simproc	file \| diff \| annotate
2002-07-21	berghofe	2002-07-21	Added theory for setting up program extraction.	file \| diff \| annotate
2001-10-22	paulson	2001-10-22	Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.	file \| diff \| annotate
2001-10-19	wenzelm	2001-10-19	got rid of Provers/split_paired_all.ML;	file \| diff \| annotate
2001-10-14	wenzelm	2001-10-14	moved rulify to ObjectLogic;	file \| diff \| annotate
2001-10-04	wenzelm	2001-10-04	use "~~/src/Provers/induct_method.ML";	file \| diff \| annotate
2001-01-03	paulson	2001-01-03	removal of the nat_cancel_factor simproc	file \| diff \| annotate
2000-12-18	paulson	2000-12-18	loads the new simproc extract_common_term	file \| diff \| annotate
2000-11-29	paulson	2000-11-29	new simproc file cancel_numeral_factor.ML	file \| diff \| annotate
2000-10-19	wenzelm	2000-10-19	tuned;	file \| diff \| annotate
2000-10-18	wenzelm	2000-10-18	path_add "~~/src/HOL/Library";	file \| diff \| annotate
2000-09-07	wenzelm	2000-09-07	added Provers/rulify;	file \| diff \| annotate
2000-06-28	paulson	2000-06-28	new file Provers/make_elim.ML	file \| diff \| annotate
2000-05-05	wenzelm	2000-05-05	removed Pure/section_utils.ML;	file \| diff \| annotate
2000-05-03	paulson	2000-05-03	removed obsolete simproc combine_coeff	file \| diff \| annotate
2000-05-02	paulson	2000-05-02	combine_numerals replaces both fold_Suc and combine_coeff	file \| diff \| annotate
2000-04-21	paulson	2000-04-21	Provers/Arith/inverse_fold.ML is already obsolete	file \| diff \| annotate
2000-04-18	paulson	2000-04-18	new simprocs for numerals of type "nat"	file \| diff \| annotate
1999-10-05	wenzelm	1999-10-05	tuned comment;	file \| diff \| annotate
1999-10-04	wenzelm	1999-10-04	proper dependencies of all theories and packages;	file \| diff \| annotate
1999-09-21	nipkow	1999-09-21	ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML	file \| diff \| annotate
1999-08-26	wenzelm	1999-08-26	tuned;	file \| diff \| annotate

isabelle

RSS Atom