| 2010-07-02 |
haftmann |
tuned bootstrap files
|
file |
diff |
annotate
|
| 2009-12-29 |
wenzelm |
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
|
file |
diff |
annotate
|
| 2009-11-11 |
wenzelm |
uniform use of simultabeous use_thys;
|
file |
diff |
annotate
|
| 2009-10-24 |
bulwahn |
processing of tuples in introduction rules
|
file |
diff |
annotate
|
| 2009-02-26 |
wenzelm |
back to canonical ROOT, to see if memory problems still persist;
|
file |
diff |
annotate
|
| 2009-01-27 |
wenzelm |
added share_common_data -- reduces heap space, but takes long;
|
file |
diff |
annotate
|
| 2009-01-11 |
wenzelm |
load main entry points sequentially, for reduced memory demands;
|
file |
diff |
annotate
|
| 2009-01-01 |
wenzelm |
tuned header and description of boot files;
|
file |
diff |
annotate
|
| 2008-12-19 |
ballarin |
All logics ported to new locales.
|
file |
diff |
annotate
|
| 2008-12-14 |
ballarin |
Ported HOL and HOL-Library to new locales.
|
file |
diff |
annotate
|
| 2008-12-05 |
haftmann |
corrected theory path
|
file |
diff |
annotate
|
| 2008-12-03 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| 2008-09-17 |
wenzelm |
moved global ML bindings to global place;
|
file |
diff |
annotate
|
| 2008-07-01 |
haftmann |
HOL += HOL-Complex
|
file |
diff |
annotate
|
| 2008-06-26 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| 2008-01-25 |
haftmann |
consistent interacitve bootstrap of HOL-Main
|
file |
diff |
annotate
|
| 2007-07-21 |
wenzelm |
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
|
file |
diff |
annotate
|
| 2007-05-31 |
wenzelm |
proper loading of ML files (in HOL.thy);
|
file |
diff |
annotate
|
| 2007-05-17 |
haftmann |
canonical prefixing of class constants
|
file |
diff |
annotate
|
| 2007-05-13 |
haftmann |
added modules rat.ML and int.ML
|
file |
diff |
annotate
|
| 2006-12-27 |
haftmann |
removed Main.thy
|
file |
diff |
annotate
|
| 2006-11-08 |
wenzelm |
added structure Main (from Main.ML);
|
file |
diff |
annotate
|
| 2006-06-10 |
dixon |
added updated version of IsaPlanner and substitution.
|
file |
diff |
annotate
|
| 2006-03-02 |
paulson |
moved the "use" directive
|
file |
diff |
annotate
|
| 2006-03-01 |
mengj |
Added file Tools/res_atpset.ML.
|
file |
diff |
annotate
|
| 2006-01-06 |
wenzelm |
simplified EqSubst setup;
|
file |
diff |
annotate
|
| 2005-12-31 |
wenzelm |
removed obsolete Provers/make_elim.ML;
|
file |
diff |
annotate
|
| 2005-12-21 |
wenzelm |
added Provers/project_rule.ML
|
file |
diff |
annotate
|
| 2005-12-21 |
paulson |
new hash table module in HOL/Too/s
|
file |
diff |
annotate
|
| 2005-12-16 |
paulson |
hashing to eliminate the output of duplicate clauses
|
file |
diff |
annotate
|