| 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
|
| Sat, 24 Sep 2005 13:11:05 +0200 |
obua |
preliminary fix of HOL build problem
|
changeset |
files
|
| Sat, 24 Sep 2005 10:47:22 +0200 |
obua |
bug fix
|
changeset |
files
|
| Sat, 24 Sep 2005 07:57:50 +0200 |
webertj |
replay_proof optimized: now performs backwards proof search
|
changeset |
files
|
| Sat, 24 Sep 2005 07:21:46 +0200 |
webertj |
code reformatted and restructured, many minor modifications
|
changeset |
files
|
| Sat, 24 Sep 2005 07:10:57 +0200 |
webertj |
bugfix in "zchaff_with_proofs"
|
changeset |
files
|
| Sat, 24 Sep 2005 02:53:08 +0200 |
webertj |
parse_std_result_file renamed to read_std_result_file
|
changeset |
files
|
| Fri, 23 Sep 2005 23:28:59 +0200 |
webertj |
new sat tactic
|
changeset |
files
|
| Fri, 23 Sep 2005 22:58:50 +0200 |
webertj |
new sat tactic imports resolution proofs from zChaff
|
changeset |
files
|