2015-01-13 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
2015-01-06 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
2015-01-01 |
boehmes |
merged
|
file |
diff |
annotate
|
2015-01-01 |
boehmes |
updated NEWS
|
file |
diff |
annotate
|
2014-12-30 |
wenzelm |
added system property isabelle.laf, notably for initial system dialog;
|
file |
diff |
annotate
|
2014-12-30 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
2014-12-22 |
wenzelm |
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
|
file |
diff |
annotate
|
2014-12-22 |
wenzelm |
system option "pretty_margin" is superseded by "thy_output_margin";
|
file |
diff |
annotate
|
2014-12-12 |
wenzelm |
Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
|
file |
diff |
annotate
|
2014-12-08 |
wenzelm |
expand ML cartouches to Input.source;
|
file |
diff |
annotate
|
2014-12-08 |
haftmann |
NEWS
|
file |
diff |
annotate
|
2014-11-26 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
2014-11-26 |
wenzelm |
added ML antiquotation @{apply n} or @{apply n(k)};
|
file |
diff |
annotate
|
2014-11-24 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
2014-11-13 |
wenzelm |
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
|
file |
diff |
annotate
|
2014-11-12 |
immler |
NEWS
|
file |
diff |
annotate
|
2014-11-10 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
2014-11-09 |
wenzelm |
proper context for match_tac etc.;
|
file |
diff |
annotate
|
2014-11-09 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
file |
diff |
annotate
|
2014-11-07 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
2014-11-02 |
wenzelm |
added update_header tool;
|
file |
diff |
annotate
|
2014-11-02 |
wenzelm |
uniform heading commands work in any context, even in theory header;
|
file |
diff |
annotate
|
2014-11-01 |
wenzelm |
command-line terminator ";" is no longer accepted;
|
file |
diff |
annotate
|
2014-10-31 |
wenzelm |
discontinued Isar TTY loop;
|
file |
diff |
annotate
|
2014-10-31 |
wenzelm |
discontinued Proof General;
|
file |
diff |
annotate
|
2014-10-28 |
wenzelm |
'notepad' requires proper nesting of begin/end;
|
file |
diff |
annotate
|
2014-10-26 |
wenzelm |
clarified default;
|
file |
diff |
annotate
|
2014-10-24 |
hoelzl |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
file |
diff |
annotate
|
2014-10-24 |
hoelzl |
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
|
file |
diff |
annotate
|
2014-10-23 |
haftmann |
downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
2014-10-21 |
wenzelm |
merged
|
file |
diff |
annotate
|
2014-10-21 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
2014-10-21 |
haftmann |
turn even into an abbreviation
|
file |
diff |
annotate
|
2014-10-20 |
wenzelm |
official support for "tt" style variants, avoid fragile \verb in LaTeX;
|
file |
diff |
annotate
|
2014-10-19 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
2014-10-18 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
2014-10-14 |
haftmann |
purely algebraic characterization of even and odd
|
file |
diff |
annotate
|
2014-10-12 |
haftmann |
generalized and consolidated some theorems concerning divisibility
|
file |
diff |
annotate
|
2014-10-09 |
haftmann |
more foundational definition for predicate even
|
file |
diff |
annotate
|
2014-10-08 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
2014-10-08 |
wenzelm |
simplified "sos" method;
|
file |
diff |
annotate
|
2014-10-08 |
Andreas Lochbihler |
move Code_Test to HOL/Library;
|
file |
diff |
annotate
|
2014-10-07 |
wenzelm |
added update_cartouches tool;
|
file |
diff |
annotate
|
2014-10-06 |
wenzelm |
improved spelling of formal INCOMPATIBILITY in historic versions (!) -- to avoid ad-hoc word completion multiply such lapses;
|
file |
diff |
annotate
|
2014-10-06 |
wenzelm |
completion for bibtex entries;
|
file |
diff |
annotate
|
2014-10-05 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
2014-10-04 |
wenzelm |
merged;
|
file |
diff |
annotate
|
2014-10-04 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
2014-10-03 |
wenzelm |
SideKick parser for bibtex entries;
|
file |
diff |
annotate
|
2014-10-03 |
wenzelm |
context menu for bibtex entries;
|
file |
diff |
annotate
|
2014-10-02 |
haftmann |
moved lemmas out of Int.thy which have nothing to do with int
|
file |
diff |
annotate
|
2014-09-22 |
wenzelm |
discontinued old "xnum" token category;
|
file |
diff |
annotate
|
2014-09-21 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
2014-09-18 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
2014-09-18 |
haftmann |
product over monoids for lists
|
file |
diff |
annotate
|
2014-09-12 |
haftmann |
NEWS
|
file |
diff |
annotate
|
2014-09-11 |
blanchet |
updated news
|
file |
diff |
annotate
|
2014-09-09 |
nipkow |
enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
|
file |
diff |
annotate
|
2014-09-07 |
haftmann |
restrictive options for class dependencies
|
file |
diff |
annotate
|
2014-09-04 |
blanchet |
updated docs
|
file |
diff |
annotate
|