2010-12-06 |
huffman |
remove lemma cont_cfun;
|
file |
diff |
annotate
|
2010-12-06 |
huffman |
rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
|
file |
diff |
annotate
|
2010-12-03 |
hoelzl |
it is known as the extended reals, not the infinite reals
|
file |
diff |
annotate
|
2010-12-06 |
wenzelm |
more correct NEWS;
|
file |
diff |
annotate
|
2010-12-05 |
wenzelm |
IsabelleText font: include Cyrillic, Hebrew, Arabic from DejaVu Sans 2.32;
|
file |
diff |
annotate
|
2010-12-05 |
wenzelm |
command 'notepad' replaces former 'example_proof';
|
file |
diff |
annotate
|
2010-12-04 |
wenzelm |
added Syntax.default_root;
|
file |
diff |
annotate
|
2010-12-04 |
wenzelm |
added Syntax.pretty_priority;
|
file |
diff |
annotate
|
2010-12-03 |
wenzelm |
minor tuning for release;
|
file |
diff |
annotate
|
2010-12-03 |
wenzelm |
source files are always encoded as UTF-8;
|
file |
diff |
annotate
|
2010-12-03 |
wenzelm |
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
|
file |
diff |
annotate
|
2010-12-03 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
2010-12-02 |
wenzelm |
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
|
file |
diff |
annotate
|
2010-12-02 |
wenzelm |
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
|
file |
diff |
annotate
|
2010-12-02 |
nipkow |
coercions
|
file |
diff |
annotate
|
2010-12-01 |
hoelzl |
Updated NEWS
|
file |
diff |
annotate
|
2010-12-01 |
haftmann |
NEWS
|
file |
diff |
annotate
|
2010-11-30 |
haftmann |
merged
|
file |
diff |
annotate
|
2010-11-29 |
haftmann |
equivI has replaced equiv.intro
|
file |
diff |
annotate
|
2010-11-29 |
wenzelm |
added document antiquotation @{file};
|
file |
diff |
annotate
|
2010-11-28 |
wenzelm |
recovered Isabelle2009-2 NEWS -- published part is read-only;
|
file |
diff |
annotate
|
2010-11-27 |
huffman |
renamed several HOLCF theorems (listed in NEWS)
|
file |
diff |
annotate
|
2010-11-26 |
wenzelm |
merged
|
file |
diff |
annotate
|
2010-11-26 |
blanchet |
document changes in Nitpick and MESON/Metis
|
file |
diff |
annotate
|
2010-11-26 |
wenzelm |
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
|
file |
diff |
annotate
|
2010-11-26 |
wenzelm |
more correct spelling;
|
file |
diff |
annotate
|
2010-11-26 |
haftmann |
globbing constant expressions use more idiomatic underscore rather than star;
|
file |
diff |
annotate
|
2010-11-22 |
hoelzl |
Replace surj by abbreviation; remove surj_on.
|
file |
diff |
annotate
|
2010-11-24 |
bulwahn |
announcing some latest change (d40b347d5b0b)
|
file |
diff |
annotate
|
2010-11-22 |
haftmann |
merged
|
file |
diff |
annotate
|
2010-11-22 |
haftmann |
replaced misleading Fset/fset name -- these do not stand for finite sets
|
file |
diff |
annotate
|
2010-11-22 |
bulwahn |
renaming quickcheck generator code to random
|
file |
diff |
annotate
|
2010-11-19 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
2010-11-19 |
huffman |
merged
|
file |
diff |
annotate
|
2010-11-17 |
huffman |
accumulated NEWS updates for HOLCF
|
file |
diff |
annotate
|
2010-11-18 |
blanchet |
mention Sledgehammer with SMT
|
file |
diff |
annotate
|
2010-11-17 |
boehmes |
require the b2i file ending in the boogie_open command (for consistency with the theory header)
|
file |
diff |
annotate
|
2010-11-08 |
boehmes |
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
|
file |
diff |
annotate
|
2010-11-05 |
krauss |
abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
|
file |
diff |
annotate
|
2010-11-05 |
wenzelm |
moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
|
file |
diff |
annotate
|
2010-11-04 |
haftmann |
merged
|
file |
diff |
annotate
|
2010-11-03 |
haftmann |
Theory Multiset provides stable quicksort implementation of sort_key.
|
file |
diff |
annotate
|
2010-11-03 |
blanchet |
standardize on seconds for Nitpick and Sledgehammer timeouts
|
file |
diff |
annotate
|
2010-11-03 |
wenzelm |
discontinued obsolete function sys_error and exception SYS_ERROR;
|
file |
diff |
annotate
|
2010-10-31 |
nipkow |
merged
|
file |
diff |
annotate
|
2010-10-29 |
nipkow |
Plus -> Sum_Type.Plus
|
file |
diff |
annotate
|
2010-10-30 |
wenzelm |
support for real valued preferences;
|
file |
diff |
annotate
|
2010-10-30 |
wenzelm |
support for real valued configuration options;
|
file |
diff |
annotate
|
2010-10-29 |
wenzelm |
merged
|
file |
diff |
annotate
|
2010-10-29 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
2010-10-28 |
wenzelm |
discontinued obsolete ML antiquotation @{theory_ref};
|
file |
diff |
annotate
|
2010-10-26 |
krauss |
fixed typo
|
file |
diff |
annotate
|
2010-10-26 |
krauss |
NEWS
|
file |
diff |
annotate
|
2010-10-26 |
boehmes |
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
|
file |
diff |
annotate
|
2010-10-25 |
wenzelm |
merged
|
file |
diff |
annotate
|
2010-10-25 |
wenzelm |
significantly improved Isabelle/Isar implementation manual;
|
file |
diff |
annotate
|
2010-10-25 |
blanchet |
merged
|
file |
diff |
annotate
|
2010-10-25 |
blanchet |
introduced manual version of "Auto Solve" as "solve_direct"
|
file |
diff |
annotate
|
2010-10-25 |
wenzelm |
added ML antiquotation @{assert};
|
file |
diff |
annotate
|
2010-10-24 |
nipkow |
renamed nat_number
|
file |
diff |
annotate
|