2008-03-25 |
wenzelm |
Functor NamedThmsFun: data is available to the user as dynamic fact;
|
file |
diff |
annotate
|
2008-03-24 |
wenzelm |
removed obsolete use_legacy_bindings;
|
file |
diff |
annotate
|
2008-03-20 |
haftmann |
Theory Product_Type; fixed typos
|
file |
diff |
annotate
|
2008-03-19 |
wenzelm |
removed redundant Nat.less_not_sym, Nat.less_asym;
|
file |
diff |
annotate
|
2008-03-19 |
paulson |
Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
|
file |
diff |
annotate
|
2008-03-18 |
wenzelm |
theory loader: discontinued *attached* ML scripts;
|
file |
diff |
annotate
|
2008-03-18 |
wenzelm |
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
|
file |
diff |
annotate
|
2008-03-07 |
haftmann |
added entries
|
file |
diff |
annotate
|
2008-03-06 |
wenzelm |
* system/system_out provides a robust way to invoke external shell
|
file |
diff |
annotate
|
2008-03-06 |
wenzelm |
removed obsolete THIS_IS_ISABELLE_BUILD;
|
file |
diff |
annotate
|
2008-03-05 |
wenzelm |
indexing literal facts: exclude background context;
|
file |
diff |
annotate
|
2008-03-05 |
krauss |
NEWS: RBTs, renamings in ZF
|
file |
diff |
annotate
|
2008-03-01 |
wenzelm |
added @{const} antiquotation;
|
file |
diff |
annotate
|
2008-02-28 |
wenzelm |
Transitive_Closure: induct and cases rules now declare proper case_names;
|
file |
diff |
annotate
|
2008-02-26 |
haftmann |
added accidental omissions
|
file |
diff |
annotate
|
2008-02-17 |
huffman |
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
|
file |
diff |
annotate
|
2008-02-15 |
haftmann |
<= and < on nat no longer depend on wellfounded relations
|
file |
diff |
annotate
|
2008-02-06 |
haftmann |
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
|
file |
diff |
annotate
|
2008-01-30 |
haftmann |
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
|
file |
diff |
annotate
|
2008-01-28 |
wenzelm |
* Outer syntax: string tokens no longer admit escaped white space;
|
file |
diff |
annotate
|
2008-01-27 |
wenzelm |
use_thy: do not set implicit ML context anymore;
|
file |
diff |
annotate
|
2008-01-25 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2008-01-25 |
wenzelm |
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
|
file |
diff |
annotate
|
2008-01-25 |
haftmann |
moved definition of power on ints to theory Int
|
file |
diff |
annotate
|
2008-01-22 |
haftmann |
added class semiring_div
|
file |
diff |
annotate
|
2008-01-15 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
2008-01-14 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2008-01-06 |
wenzelm |
* Rudimentary Isabelle plugin for jEdit;
|
file |
diff |
annotate
|
2008-01-02 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2008-01-02 |
wenzelm |
Multithreading.max_threads := 0 refers to number of cores of underlying machine;
|
file |
diff |
annotate
|
2008-01-02 |
haftmann |
split of class uminus
|
file |
diff |
annotate
|
2007-12-20 |
wenzelm |
``print mode'' is now a thread-local value derived from a global template;
|
file |
diff |
annotate
|
2007-12-20 |
wenzelm |
* Metis prover an order of magnitude faster, works with multithreading.
|
file |
diff |
annotate
|
2007-12-19 |
haftmann |
instantiation target
|
file |
diff |
annotate
|
2007-12-19 |
schirmer |
replaced K_record by lambda term %x. c
|
file |
diff |
annotate
|
2007-12-17 |
krauss |
spread NEWS about "induction_scheme" method
|
file |
diff |
annotate
|
2007-12-15 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2007-12-15 |
wenzelm |
* isatool browser now works with Cygwin;
|
file |
diff |
annotate
|
2007-12-14 |
wenzelm |
* isatool tty runs Isabelle process with plain tty interaction;
|
file |
diff |
annotate
|
2007-12-12 |
haftmann |
tuned
|
file |
diff |
annotate
|
2007-12-11 |
haftmann |
tuned
|
file |
diff |
annotate
|
2007-12-07 |
wenzelm |
(alt)string: allow explicit character codes (as in ML);
|
file |
diff |
annotate
|
2007-12-06 |
haftmann |
added new primrec package
|
file |
diff |
annotate
|
2007-12-04 |
wenzelm |
\<chi> is now considered a letter;
|
file |
diff |
annotate
|
2007-11-30 |
haftmann |
adjustions to due to instance target
|
file |
diff |
annotate
|
2007-11-30 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2007-11-29 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
2007-11-26 |
wenzelm |
moved new NEWS from Isabelle2007 to this Isabelle version'';
|
file |
diff |
annotate
|
2007-11-23 |
haftmann |
deleted card definition as code lemma; authentic syntax for card
|
file |
diff |
annotate
|
2007-11-20 |
wenzelm |
tuned spacing;
|
file |
diff |
annotate
|
2007-11-15 |
wenzelm |
cover ISABELLE_IDENTIFIER;
|
file |
diff |
annotate
|
2007-11-13 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2007-11-12 |
schirmer |
fixed typo;
|
file |
diff |
annotate
|
2007-11-11 |
wenzelm |
* HOL-Statespace;
|
file |
diff |
annotate
|
2007-10-26 |
haftmann |
tuned
|
file |
diff |
annotate
|
2007-10-26 |
krauss |
added NEWS entry for function package
|
file |
diff |
annotate
|
2007-10-25 |
haftmann |
tuned
|
file |
diff |
annotate
|
2007-10-24 |
wenzelm |
tuned file names etc.;
|
file |
diff |
annotate
|
2007-10-24 |
haftmann |
tuned
|
file |
diff |
annotate
|
2007-10-22 |
wenzelm |
tuned Nominal entry;
|
file |
diff |
annotate
|