| 2015-11-12 |
wenzelm |
support short form for \<^theory_text>;
|
file |
diff |
annotate
|
| 2015-11-11 |
Andreas Lochbihler |
cancel complementary terms as arguments to sup/inf in boolean algebras
|
file |
diff |
annotate
|
| 2015-11-10 |
wenzelm |
added @{command}, @{method}, @{attribute};
|
file |
diff |
annotate
|
| 2015-11-10 |
wenzelm |
added document antiquotation @{theory_text};
|
file |
diff |
annotate
|
| 2015-11-09 |
wenzelm |
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
|
file |
diff |
annotate
|
| 2015-11-09 |
wenzelm |
prefer explicit State panel;
|
file |
diff |
annotate
|
| 2015-11-08 |
wenzelm |
added option timeout_scale;
|
file |
diff |
annotate
|
| 2015-11-07 |
wenzelm |
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
|
file |
diff |
annotate
|
| 2015-11-07 |
wenzelm |
added @{undefined} with somewhat undefined symbol;
|
file |
diff |
annotate
|
| 2015-11-06 |
wenzelm |
more formal treatment of control symbols;
|
file |
diff |
annotate
|
| 2015-11-04 |
wenzelm |
symbolic syntax "\<comment> text";
|
file |
diff |
annotate
|
| 2015-11-04 |
wenzelm |
document antiquotation @{footnote};
|
file |
diff |
annotate
|
| 2015-11-04 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2015-11-04 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
file |
diff |
annotate
|
| 2015-11-04 |
ballarin |
Qualifiers in locale expressions default to mandatory regardless of the command.
|
file |
diff |
annotate
|
| 2015-11-02 |
blanchet |
don't pollute local theory with needless names
|
file |
diff |
annotate
|
| 2015-11-02 |
blanchet |
allow selectors and discriminators with same name as type
|
file |
diff |
annotate
|
| 2015-11-02 |
wenzelm |
clarified completion of Isabelle symbols within document source;
|
file |
diff |
annotate
|
| 2015-10-31 |
wenzelm |
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
|
file |
diff |
annotate
|
| 2015-10-27 |
paulson |
Cauchy's integral formula, required lemmas, and a bit of reorganisation
|
file |
diff |
annotate
|
| 2015-10-24 |
wenzelm |
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
|
file |
diff |
annotate
|
| 2015-10-21 |
wenzelm |
rendering for \<^verbatim>;
|
file |
diff |
annotate
|
| 2015-10-20 |
wenzelm |
proper spaces around @{text};
|
file |
diff |
annotate
|
| 2015-10-20 |
wenzelm |
added isabelle update_cartouches option -t;
|
file |
diff |
annotate
|
| 2015-10-20 |
wenzelm |
another antiquotation short form: undecorated cartouche as alias for @{text};
|
file |
diff |
annotate
|
| 2015-10-19 |
wenzelm |
tuned English;
|
file |
diff |
annotate
|
| 2015-10-19 |
wenzelm |
added action "isabelle-emph";
|
file |
diff |
annotate
|
| 2015-10-18 |
wenzelm |
clarified control antiquotations: decode control symbol to get name;
|
file |
diff |
annotate
|
| 2015-10-18 |
wenzelm |
support control symbol antiquotations;
|
file |
diff |
annotate
|
| 2015-10-17 |
wenzelm |
added 'paragraph', 'subparagraph';
|
file |
diff |
annotate
|
| 2015-10-17 |
wenzelm |
more explicit output of list items;
|
file |
diff |
annotate
|
| 2015-10-14 |
wenzelm |
clarified control symbols;
|
file |
diff |
annotate
|
| 2015-10-13 |
paulson |
new material on path_component_sets, inside, outside, etc. And more default simprules
|
file |
diff |
annotate
|
| 2015-10-13 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| 2015-10-12 |
wenzelm |
some control symbols for markup and formatting;
|
file |
diff |
annotate
|
| 2015-10-10 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
| 2015-10-09 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2015-10-08 |
kuncar |
NEWS
|
file |
diff |
annotate
|
| 2015-10-06 |
blanchet |
news
|
file |
diff |
annotate
|
| 2015-10-06 |
wenzelm |
added 'proposition' command;
|
file |
diff |
annotate
|
| 2015-10-06 |
wenzelm |
fewer aliases for toplevel theorem statements;
|
file |
diff |
annotate
|
| 2015-10-05 |
blanchet |
avoid too aggressive optimization of 'finite' predicate
|
file |
diff |
annotate
|
| 2015-10-05 |
blanchet |
avoid unsound simplification of (C (s x)) when s is a selector but not C's
|
file |
diff |
annotate
|
| 2015-10-03 |
blanchet |
speed up MaSh
|
file |
diff |
annotate
|
| 2015-10-02 |
blanchet |
updated docs and NEWS
|
file |
diff |
annotate
|
| 2015-10-02 |
wenzelm |
avoid useless empty case_names;
|
file |
diff |
annotate
|
| 2015-09-30 |
wenzelm |
renamed jvmpath to platform_path;
|
file |
diff |
annotate
|
| 2015-09-25 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2015-09-25 |
wenzelm |
documentation for "Semantic subtype definitions";
|
file |
diff |
annotate
|
| 2015-09-25 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| 2015-09-22 |
wenzelm |
separate command 'print_definitions';
|
file |
diff |
annotate
|
| 2015-09-22 |
haftmann |
tuned
|
file |
diff |
annotate
|
| 2015-09-22 |
haftmann |
effective revert of e6b1236f9b3d: spontaneous eta-contraction happens on the print translation level and can only be suppressed on the print translation level
|
file |
diff |
annotate
|
| 2015-09-21 |
wenzelm |
clarified isabelle.update-state;
|
file |
diff |
annotate
|
| 2015-09-21 |
wenzelm |
added isabelle update_then;
|
file |
diff |
annotate
|
| 2015-09-21 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2015-09-19 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2015-09-15 |
lammich |
Omega_Words_Fun: Infinite words as functions from nat.
|
file |
diff |
annotate
|
| 2015-09-14 |
wenzelm |
replacement character for spaces;
|
file |
diff |
annotate
|
| 2015-09-14 |
wenzelm |
single-instance application, even on Linux;
|
file |
diff |
annotate
|