| 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
|
| 2008-07-25 |
haftmann |
dropped locale (open)
|
file |
diff |
annotate
|
| 2008-07-18 |
haftmann |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file |
diff |
annotate
|
| 2008-07-15 |
wenzelm |
added command 'linear_undo';
|
file |
diff |
annotate
|
| 2008-07-14 |
haftmann |
unified curried gcd, lcm, zgcd, zlcm
|
file |
diff |
annotate
|
| 2008-07-11 |
haftmann |
Fract now total; improved code generator setup
|
file |
diff |
annotate
|
| 2008-07-10 |
wenzelm |
slightly improved @{lemma} (both for latex and ML);
|
file |
diff |
annotate
|
| 2008-07-04 |
huffman |
HOL-NSA
|
file |
diff |
annotate
|
| 2008-07-02 |
haftmann |
code antiquotation roaring ahead
|
file |
diff |
annotate
|
| 2008-07-01 |
haftmann |
HOL += HOL-Complex
|
file |
diff |
annotate
|
| 2008-07-01 |
haftmann |
HOL += HOL-Complex
|
file |
diff |
annotate
|
| 2008-06-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2008-06-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2008-06-28 |
wenzelm |
additional ML antiquotations;
|
file |
diff |
annotate
|
| 2008-06-28 |
wenzelm |
@{lemma}: 'by' keyword;
|
file |
diff |
annotate
|
| 2008-06-28 |
wenzelm |
ML: improved antiquotations;
|
file |
diff |
annotate
|
| 2008-06-23 |
wenzelm |
induct_tac: mutual rules work as for method "induct";
|
file |
diff |
annotate
|
| 2008-06-20 |
haftmann |
(removed non-present change)
|
file |
diff |
annotate
|