| 2009-03-05 |
huffman |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
file |
diff |
annotate
|
| 2009-03-04 |
wenzelm |
NEWS: renamed o2s to Option.set;
|
file |
diff |
annotate
|
| 2009-03-04 |
nipkow |
Made Option a separate theory and renamed option_map to Option.map
|
file |
diff |
annotate
|
| 2009-03-03 |
nipkow |
removed and renamed redundant lemmas
|
file |
diff |
annotate
|
| 2009-03-02 |
nipkow |
name fix
|
file |
diff |
annotate
|
| 2009-03-02 |
nipkow |
name changes
|
file |
diff |
annotate
|
| 2009-03-01 |
nipkow |
removed redundant lemmas
|
file |
diff |
annotate
|
| 2009-02-28 |
huffman |
add news for HOLCF; fixed some typos and inaccuracies
|
file |
diff |
annotate
|
| 2009-02-28 |
wenzelm |
* New prover for coherent logic (see src/Tools/coherent.ML).
|
file |
diff |
annotate
|
| 2009-02-26 |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| 2009-02-25 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| 2009-02-21 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| 2009-02-12 |
kleing |
added find_consts to NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2009-02-11 |
kleing |
fixed typo
|
file |
diff |
annotate
|
| 2009-02-11 |
kleing |
updated NEWS etc with "solves" criterion and auto_solves
|
file |
diff |
annotate
|
| 2009-02-06 |
haftmann |
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
|
file |
diff |
annotate
|
| 2009-02-05 |
hoelzl |
Updated NEWS about approximation
|
file |
diff |
annotate
|
| 2009-02-05 |
hoelzl |
Add approximation method
|
file |
diff |
annotate
|
| 2009-02-03 |
haftmann |
handling type classes without parameters
|
file |
diff |
annotate
|
| 2009-02-03 |
haftmann |
established session HOL-Reflection
|
file |
diff |
annotate
|
| 2009-01-28 |
nipkow |
-
|
file |
diff |
annotate
|
| 2009-01-28 |
haftmann |
Reflection.thy now in HOL/Library
|
file |
diff |
annotate
|
| 2009-01-26 |
haftmann |
entry point for Word library now named Word
|
file |
diff |
annotate
|
| 2009-01-22 |
haftmann |
binding replaces Binding.T
|
file |
diff |
annotate
|
| 2009-01-21 |
haftmann |
no base sort in class import
|
file |
diff |
annotate
|
| 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
|
| 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
|
| 2008-06-19 |
wenzelm |
disposed Sign.read_typ etc;
|
file |
diff |
annotate
|
| 2008-06-18 |
wenzelm |
* Disposed old term read functions;
|
file |
diff |
annotate
|
| 2008-06-16 |
wenzelm |
* Rules and tactics that read instantiations now demand a proper context;
|
file |
diff |
annotate
|
| 2008-06-14 |
wenzelm |
removed exotic 'token_translation' command;
|
file |
diff |
annotate
|
| 2008-06-13 |
wenzelm |
* Recovered hiding of consts;
|
file |
diff |
annotate
|
| 2008-06-11 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2008-06-10 |
wenzelm |
tuned spacing;
|
file |
diff |
annotate
|
| 2008-06-10 |
wenzelm |
* Attributes cases, induct, coinduct support del option.
|
file |
diff |
annotate
|
| 2008-06-10 |
wenzelm |
proper news header;
|
file |
diff |
annotate
|
| 2008-06-10 |
haftmann |
rep_datatype command now takes list of constructors as input arguments
|
file |
diff |
annotate
|
| 2008-06-03 |
wenzelm |
some reorganization and fine-tuning;
|
file |
diff |
annotate
|
| 2008-06-02 |
wenzelm |
reorganized isar-ref;
|
file |
diff |
annotate
|
| 2008-05-28 |
wenzelm |
misc tuning for Isabelle2008;
|
file |
diff |
annotate
|
| 2008-05-21 |
berghofe |
Added entry explaining incompatibilities introduced by replacing sets by predicates.
|
file |
diff |
annotate
|
| 2008-05-18 |
wenzelm |
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
|
file |
diff |
annotate
|
| 2008-05-16 |
wenzelm |
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
|
file |
diff |
annotate
|
| 2008-05-15 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2008-05-15 |
wenzelm |
* Simplified pdfsetup.sty;
|
file |
diff |
annotate
|