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