| 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
|
| 2013-03-23 |
haftmann |
spelling
|
file |
diff |
annotate
|
| 2013-03-23 |
haftmann |
fundamental revision of big operators on sets
|
file |
diff |
annotate
|
| 2013-03-23 |
haftmann |
locales for abstract orders
|
file |
diff |
annotate
|
| 2013-03-13 |
wenzelm |
sessions may be organized via 'chapter' in ROOT;
|
file |
diff |
annotate
|
| 2013-03-12 |
wenzelm |
discontinued "isabelle usedir" option -r (reset session path);
|
file |
diff |
annotate
|
| 2013-03-11 |
wenzelm |
discontinued "isabelle usedir" option -P (remote path);
|
file |
diff |
annotate
|
| 2013-03-09 |
haftmann |
discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types
|
file |
diff |
annotate
|
| 2013-02-28 |
wenzelm |
discontinued empty name bindings in 'axiomatization';
|
file |
diff |
annotate
|
| 2013-02-28 |
wenzelm |
discontinued obsolete 'axioms' command;
|
file |
diff |
annotate
|
| 2013-02-27 |
wenzelm |
discontinued redundant 'use' command;
|
file |
diff |
annotate
|
| 2013-02-27 |
wenzelm |
discontinued obsolete 'uses' within theory header;
|
file |
diff |
annotate
|
| 2013-02-22 |
wenzelm |
discontinued obsolete src/HOL/IsaMakefile;
|
file |
diff |
annotate
|
| 2013-02-16 |
haftmann |
restored proper order of NEWS entries (lost due too long-waiting patches)
|
file |
diff |
annotate
|
| 2013-02-15 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
| 2013-02-15 |
blanchet |
updated news
|
file |
diff |
annotate
|
| 2013-02-14 |
haftmann |
consolidation of library theories on product orders
|
file |
diff |
annotate
|
| 2013-02-13 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| 2013-02-10 |
wenzelm |
updated PIDE notes;
|
file |
diff |
annotate
|
| 2013-01-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2013-01-26 |
wenzelm |
clarified NEWS on isabelle build and mkroot;
|
file |
diff |
annotate
|
| 2013-01-25 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2013-01-31 |
hoelzl |
remove unnecessary assumption from real_normed_vector
|
file |
diff |
annotate
|
| 2013-01-20 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| 2013-01-20 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| 2013-01-20 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 2013-01-14 |
kuncar |
NEWS
|
file |
diff |
annotate
|
| 2013-01-11 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 2013-01-09 |
wenzelm |
tune spelling;
|
file |
diff |
annotate
|
| 2013-01-08 |
wenzelm |
allow negative argument in "consumes" source format;
|
file |
diff |
annotate
|
| 2013-01-04 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2013-01-04 |
wenzelm |
more reactive completion popup by default;
|
file |
diff |
annotate
|
| 2013-01-04 |
blanchet |
updated docs
|
file |
diff |
annotate
|
| 2013-01-04 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 2013-01-04 |
wenzelm |
document 'locale_deps';
|
file |
diff |
annotate
|
| 2013-01-03 |
wenzelm |
NEWS: ML runtime statistics;
|
file |
diff |
annotate
|
| 2012-12-31 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 2012-12-31 |
wenzelm |
recovered Isabelle2012 NEWS from ae12b92c145a, except for e5420161d11d;
|
file |
diff |
annotate
|
| 2012-12-29 |
nipkow |
new theory Library/Finite_Lattice
|
file |
diff |
annotate
|