| 2009-01-08 |
haftmann |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2008-12-30 |
ballarin |
New locales.
|
file |
diff |
annotate
|
| 2008-12-29 |
haftmann |
adapted HOL source structure to distribution layout
|
file |
diff |
annotate
|
| 2008-12-27 |
krauss |
tuned NEWS; CONTRIBUTORS
|
file |
diff |
annotate
|
| 2008-12-23 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2008-12-23 |
wenzelm |
* Proofs of are run in parallel on multi-core systems;
|
file |
diff |
annotate
|
| 2008-12-20 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| 2008-12-16 |
krauss |
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
|
file |
diff |
annotate
|
| 2008-12-04 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2008-12-04 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| 2008-12-04 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| 2008-12-03 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| 2008-11-30 |
wenzelm |
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
|
file |
diff |
annotate
|
| 2008-11-30 |
wenzelm |
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
|
file |
diff |
annotate
|
| 2008-11-19 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
file |
diff |
annotate
|
| 2008-11-19 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2008-11-13 |
haftmann |
simproc for let
|
file |
diff |
annotate
|
| 2008-10-30 |
ballarin |
Dropped context element 'includes'.
|
file |
diff |
annotate
|
| 2008-10-28 |
paulson |
The metis method no longer fails because the theorem is too trivial
|
file |
diff |
annotate
|
| 2008-10-24 |
haftmann |
new classes "top" and "bot"
|
file |
diff |
annotate
|
| 2008-10-23 |
wenzelm |
multithreading support only for polyml-5.2.1 or later;
|
file |
diff |
annotate
|
| 2008-10-16 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2008-10-16 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2008-10-16 |
wenzelm |
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
|
file |
diff |
annotate
|
| 2008-10-15 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2008-10-15 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2008-10-15 |
wenzelm |
generic ATP manager based on threads (by Fabian Immler);
|
file |
diff |
annotate
|
| 2008-10-10 |
haftmann |
tuned
|
file |
diff |
annotate
|
| 2008-10-10 |
haftmann |
tuned default rules of (dvd)
|
file |
diff |
annotate
|
| 2008-10-07 |
haftmann |
only one theorem table for both code generators
|
file |
diff |
annotate
|
| 2008-10-04 |
wenzelm |
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
|
file |
diff |
annotate
|
| 2008-10-03 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2008-10-03 |
wenzelm |
Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
|
file |
diff |
annotate
|
| 2008-09-25 |
haftmann |
non left-linear equations for nbe
|
file |
diff |
annotate
|
| 2008-09-18 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2008-09-18 |
wenzelm |
simplified oracle interface;
|
file |
diff |
annotate
|
| 2008-09-17 |
wenzelm |
* ML bindings produced via Isar commands are stored within the Isar context.
|
file |
diff |
annotate
|
| 2008-09-16 |
wenzelm |
multithreading for Poly/ML 5.1 is no longer supported;
|
file |
diff |
annotate
|
| 2008-09-16 |
wenzelm |
updated system manual;
|
file |
diff |
annotate
|
| 2008-09-16 |
wenzelm |
separate emacs tool for Proof General / Emacs;
|
file |
diff |
annotate
|
| 2008-09-16 |
paulson |
The metis method now fails in the usual manner, rather than raising an exception,
|
file |
diff |
annotate
|
| 2008-09-16 |
haftmann |
generic value command
|
file |
diff |
annotate
|
| 2008-09-09 |
wenzelm |
* Changed defaults for unify configuration options;
|
file |
diff |
annotate
|
| 2008-09-05 |
haftmann |
different bookkeeping for code equations
|
file |
diff |
annotate
|
| 2008-09-03 |
wenzelm |
axiomatization is now global-only;
|
file |
diff |
annotate
|
| 2008-09-03 |
wenzelm |
simplified Toplevel.add_hook: cover successful transactions only;
|
file |
diff |
annotate
|
| 2008-09-02 |
wenzelm |
* Generic Toplevel.add_hook interface allows to analyze the result of
|
file |
diff |
annotate
|
| 2008-09-02 |
wenzelm |
* Result facts now refer to the *full* internal name;
|
file |
diff |
annotate
|
| 2008-09-02 |
wenzelm |
* Name bindings in higher specification mechanisms;
|
file |
diff |
annotate
|
| 2008-09-02 |
ballarin |
Interpretation commands no longer accept interpretation attributes.
|
file |
diff |
annotate
|
| 2008-09-01 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2008-08-29 |
haftmann |
dropped parameter prefix for class theorems
|
file |
diff |
annotate
|
| 2008-08-23 |
wenzelm |
* Isabelle/lib/classes/Pure.jar;
|
file |
diff |
annotate
|
| 2008-08-11 |
haftmann |
moved class wellorder to theory Orderings
|
file |
diff |
annotate
|
| 2008-08-08 |
wenzelm |
tuned formatting;
|
file |
diff |
annotate
|
| 2008-08-06 |
ballarin |
Interpretation command (theory/proof context) no longer simplifies goal.
|
file |
diff |
annotate
|
| 2008-08-01 |
ballarin |
Generalised polynomial lemmas from cring to ring.
|
file |
diff |
annotate
|
| 2008-07-30 |
ballarin |
New locales for orders and lattices where the equivalence relation is not restricted to equality.
|
file |
diff |
annotate
|
| 2008-07-29 |
ballarin |
Zorn's Lemma for partial orders.
|
file |
diff |
annotate
|
| 2008-07-29 |
ballarin |
Unit_inv_l, Unit_inv_r made [simp];
|
file |
diff |
annotate
|