| 2013-08-23 |
wenzelm |
clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
|
file |
diff |
annotate
|
| 2013-08-23 |
wenzelm |
obsolete (see 52790e3961fe);
|
file |
diff |
annotate
|
| 2013-08-23 |
wenzelm |
added action isabelle.reset-font-size;
|
file |
diff |
annotate
|
| 2013-08-23 |
wenzelm |
tuned -- some reformatting;
|
file |
diff |
annotate
|
| 2013-08-20 |
krauss |
renamed theory Mrec to Legacy_Mrec, no longer included by default
|
file |
diff |
annotate
|
| 2013-08-17 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-08-13 |
wenzelm |
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
|
file |
diff |
annotate
|
| 2013-08-13 |
wenzelm |
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
|
file |
diff |
annotate
|
| 2013-08-09 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-08-07 |
wenzelm |
more NEWS and CONTRIBUTORS;
|
file |
diff |
annotate
|
| 2013-07-31 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-07-31 |
wenzelm |
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
|
file |
diff |
annotate
|
| 2013-07-30 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| 2013-07-29 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-07-27 |
wenzelm |
discontinued historic document formats;
|
file |
diff |
annotate
|
| 2013-07-27 |
wenzelm |
avoid predefined symbols -- allow editing with Isabelle/jEdit in isabelle-news mode;
|
file |
diff |
annotate
|
| 2013-07-27 |
wenzelm |
discontinued ISABELLE_DOC_FORMAT;
|
file |
diff |
annotate
|
| 2013-07-13 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2013-07-13 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-07-13 |
haftmann |
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
|
file |
diff |
annotate
|
| 2013-07-07 |
wenzelm |
discontinued obsolete "isabelle print";
|
file |
diff |
annotate
|
| 2013-07-07 |
wenzelm |
discontinued command 'print_drafts';
|
file |
diff |
annotate
|
| 2013-07-06 |
wenzelm |
minimal jedit mode for Isabelle NEWS;
|
file |
diff |
annotate
|
| 2013-06-30 |
wenzelm |
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
|
file |
diff |
annotate
|
| 2013-06-30 |
wenzelm |
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
|
file |
diff |
annotate
|
| 2013-06-27 |
wenzelm |
manage option "proofs" within theory context -- with minor overhead for primitive inferences;
|
file |
diff |
annotate
|
| 2013-06-27 |
wenzelm |
updated documentation;
|
file |
diff |
annotate
|
| 2013-06-25 |
wenzelm |
dockable window for Isabelle documentation;
|
file |
diff |
annotate
|
| 2013-06-24 |
wenzelm |
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
|
file |
diff |
annotate
|
| 2013-06-23 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
| 2013-06-23 |
wenzelm |
proper diagnostic command 'print_state';
|
file |
diff |
annotate
|
| 2013-06-18 |
wenzelm |
eliminated old "ref" manual;
|
file |
diff |
annotate
|
| 2013-06-15 |
haftmann |
lifting for primitive definitions;
|
file |
diff |
annotate
|
| 2013-06-02 |
haftmann |
make reification part of HOL
|
file |
diff |
annotate
|
| 2013-05-31 |
bulwahn |
NEWS about Spec_Check
|
file |
diff |
annotate
|
| 2013-05-25 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2013-05-25 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| 2013-05-25 |
haftmann |
weaker precendence of syntax for big intersection and union on sets
|
file |
diff |
annotate
|
| 2013-05-22 |
wenzelm |
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
|
file |
diff |
annotate
|
| 2013-05-17 |
wenzelm |
renamed 'print_configs' to 'print_options';
|
file |
diff |
annotate
|
| 2013-05-17 |
wenzelm |
proper option quick_and_dirty;
|
file |
diff |
annotate
|
| 2013-05-17 |
wenzelm |
discontinued obsolete isabelle-process options -f and -u;
|
file |
diff |
annotate
|
| 2013-05-17 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-05-17 |
wenzelm |
discontinued obsolete isabelle usedir, mkdir, make;
|
file |
diff |
annotate
|
| 2013-04-25 |
hoelzl |
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
|
file |
diff |
annotate
|
| 2013-04-25 |
hoelzl |
renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
|
file |
diff |
annotate
|
| 2013-04-24 |
hoelzl |
spell conditional_ly_-complete lattices correct
|
file |
diff |
annotate
|
| 2013-04-23 |
haftmann |
documentation and NEWS
|
file |
diff |
annotate
|
| 2013-04-22 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| 2013-04-18 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| 2013-04-12 |
wenzelm |
modifiers for classical wrappers operate on Proof.context instead of claset;
|
file |
diff |
annotate
|
| 2013-04-10 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2013-04-10 |
wenzelm |
added ML antiquotation @{theory_context};
|
file |
diff |
annotate
|
| 2013-04-10 |
traytel |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2013-04-02 |
wenzelm |
NEWS for 635562bc14ef;
|
file |
diff |
annotate
|
| 2013-03-27 |
ballarin |
Improvements to the print_dependencies command.
|
file |
diff |
annotate
|
| 2013-03-27 |
wenzelm |
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
|
file |
diff |
annotate
|
| 2013-03-27 |
wenzelm |
tuned signature and module arrangement;
|
file |
diff |
annotate
|
| 2013-03-26 |
wenzelm |
dockable window for timing information;
|
file |
diff |
annotate
|
| 2013-03-25 |
ballarin |
Discontinued theories src/HOL/Algebra/abstract and .../poly.
|
file |
diff |
annotate
|