| Mon, 26 Sep 2005 19:19:12 +0200 |
wenzelm |
yet another atempt to get doc/Contents right;
|
changeset |
files
|
| Mon, 26 Sep 2005 19:04:31 +0200 |
berghofe |
Renamed wf_rec to wfrec in consts_code declaration.
|
changeset |
files
|
| Mon, 26 Sep 2005 17:14:48 +0200 |
wenzelm |
really copy doc/Contents;
|
changeset |
files
|
| Mon, 26 Sep 2005 16:10:19 +0200 |
obua |
Release HOL4 and HOLLight Importer.
|
changeset |
files
|
| Mon, 26 Sep 2005 15:56:28 +0200 |
wenzelm |
copy doc/Contents;
|
changeset |
files
|
| Mon, 26 Sep 2005 15:17:33 +0200 |
skalberg |
Made sure all lemmas now have names (especially so that certain of them
|
changeset |
files
|
| Mon, 26 Sep 2005 13:12:24 +0200 |
wenzelm |
echo HOL_USERDIR_OPTIONS;
|
changeset |
files
|
| Mon, 26 Sep 2005 08:50:21 +0200 |
obua |
tuned
|
changeset |
files
|
| Mon, 26 Sep 2005 08:49:50 +0200 |
obua |
added ROOT.ML
|
changeset |
files
|
| Mon, 26 Sep 2005 08:41:24 +0200 |
haftmann |
adjusted web link
|
changeset |
files
|
| Mon, 26 Sep 2005 02:27:59 +0200 |
obua |
added entry for running HOLLight
|
changeset |
files
|
| Mon, 26 Sep 2005 02:27:14 +0200 |
obua |
fixed disambiguation problem
|
changeset |
files
|
| Mon, 26 Sep 2005 02:06:44 +0200 |
obua |
added Drule.disambiguate_frees : thm -> thm
|
changeset |
files
|
| Sun, 25 Sep 2005 23:36:14 +0200 |
wenzelm |
zero_var_inst: replace loose bounds :000 etc.;
|
changeset |
files
|
| Sun, 25 Sep 2005 20:24:23 +0200 |
wenzelm |
* Hyperreal: A theory of Taylor series.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:24:10 +0200 |
wenzelm |
more;
|
changeset |
files
|
| Sun, 25 Sep 2005 20:19:31 +0200 |
berghofe |
eq_codegen now ensures that code for bool type is generated.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:17:44 +0200 |
berghofe |
Fixed print mode problem in test_term.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:17:13 +0200 |
berghofe |
Added ExecutableSet and Taylor.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:15:29 +0200 |
berghofe |
Now uses set implementation from ExecutableSet.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:14:39 +0200 |
berghofe |
Added Taylor.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:14:16 +0200 |
berghofe |
Formalization of Taylor series by Lukas Bulwahn and
|
changeset |
files
|
| Sun, 25 Sep 2005 20:12:59 +0200 |
berghofe |
Added ExecutableSet.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:12:26 +0200 |
berghofe |
New theory for implementing finite sets by lists.
|
changeset |
files
|
| Sun, 25 Sep 2005 01:12:49 +0200 |
webertj |
sat_solver.ML not loaded anymore (already loaded by Refute.thy)
|
changeset |
files
|
| Sat, 24 Sep 2005 23:55:17 +0200 |
obua |
set show_types and show_sorts during import
|
changeset |
files
|
| Sat, 24 Sep 2005 21:13:15 +0200 |
nipkow |
a few new filter lemmas
|
changeset |
files
|
| Sat, 24 Sep 2005 16:43:41 +0200 |
obua |
HOL4-Import: map ONTO to Fun.surj
|
changeset |
files
|
| Sat, 24 Sep 2005 13:54:35 +0200 |
webertj |
cnf_struct renamed to cnf
|
changeset |
files
|
| Sat, 24 Sep 2005 13:26:40 +0200 |
obua |
remove debug clutter
|
changeset |
files
|