NEWS
author wenzelm
Mon, 23 Dec 2019 22:30:03 +0100
changeset 71552 7a53175fb0f4
parent 71534 0131b7b44c32
child 71587 820cf124dced
permissions -rw-r--r--
NEWS;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
57491
9eedaafc05c8 tuned grammar and spelling (cf. 0cf15843b82f);
wenzelm
parents: 57476
diff changeset
     1
Isabelle NEWS -- history of user-relevant changes
9eedaafc05c8 tuned grammar and spelling (cf. 0cf15843b82f);
wenzelm
parents: 57476
diff changeset
     2
=================================================
2553
ed941505cab7 Isabelle NEWS -- history of user-visible changes;
wenzelm
parents:
diff changeset
     3
62114
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents: 62111
diff changeset
     4
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
60007
wenzelm
parents: 59998
diff changeset
     5
64603
a7f5e59378f7 tuned whitespace;
wenzelm
parents: 64602
diff changeset
     6
70449
a8238fd25541 back to post-release mode;
wenzelm
parents: 70444
diff changeset
     7
New in this Isabelle version
a8238fd25541 back to post-release mode;
wenzelm
parents: 70444
diff changeset
     8
----------------------------
a8238fd25541 back to post-release mode;
wenzelm
parents: 70444
diff changeset
     9
70748
wenzelm
parents: 70711
diff changeset
    10
*** General ***
wenzelm
parents: 70711
diff changeset
    11
70867
56d70f7ce4a4 more documentation;
wenzelm
parents: 70794
diff changeset
    12
* Session ROOT files need to specify explicit 'directories' for import
70871
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70867
diff changeset
    13
of theory files. Directories cannot be shared by different sessions.
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70867
diff changeset
    14
(Recall that import of theories from other sessions works via
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70867
diff changeset
    15
session-qualified theory names, together with suitable 'sessions'
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70867
diff changeset
    16
declarations in the ROOT.)
70867
56d70f7ce4a4 more documentation;
wenzelm
parents: 70794
diff changeset
    17
70748
wenzelm
parents: 70711
diff changeset
    18
* Internal derivations record dependencies on oracles and other theorems
wenzelm
parents: 70711
diff changeset
    19
accurately, including the implicit type-class reasoning wrt. proven
wenzelm
parents: 70711
diff changeset
    20
class relations and type arities. In particular, the formal tagging with
wenzelm
parents: 70711
diff changeset
    21
"Pure.skip_proofs" of results stemming from "instance ... sorry" is now
wenzelm
parents: 70711
diff changeset
    22
propagated properly to theorems depending on such type instances.
wenzelm
parents: 70711
diff changeset
    23
wenzelm
parents: 70711
diff changeset
    24
* Command 'sorry' (oracle "Pure.skip_proofs") is more precise about the
wenzelm
parents: 70711
diff changeset
    25
actual proposition that is assumed in the goal and proof context. This
wenzelm
parents: 70711
diff changeset
    26
requires at least Proofterm.proofs = 1 to show up in theorem
wenzelm
parents: 70711
diff changeset
    27
dependencies.
wenzelm
parents: 70711
diff changeset
    28
wenzelm
parents: 70711
diff changeset
    29
* Command 'thm_oracles' prints all oracles used in given theorems,
wenzelm
parents: 70711
diff changeset
    30
covering the full graph of transitive dependencies.
wenzelm
parents: 70711
diff changeset
    31
70791
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70785
diff changeset
    32
* Command 'thm_deps' prints immediate theorem dependencies of the given
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70785
diff changeset
    33
facts. The former graph visualization has been discontinued, because it
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70785
diff changeset
    34
was hardly usable.
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70785
diff changeset
    35
70748
wenzelm
parents: 70711
diff changeset
    36
70708
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
    37
*** Isar ***
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
    38
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
    39
* The proof method combinator (subproofs m) applies the method
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
    40
expression m consecutively to each subgoal, constructing individual
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
    41
subproofs internally. This impacts the internal construction of proof
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
    42
terms: it makes a cascade of let-expressions within the derivation tree
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
    43
and may thus improve scalability.
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
    44
70794
d997c7ba3305 Tracing of locale activation.
ballarin
parents: 70791
diff changeset
    45
* New attribute "trace_locales" for tracing activation of locale
71364
c9433e8e314e Remove diagnostic command 'print_dependencies'.
ballarin
parents: 71348
diff changeset
    46
instances during roundup.  It replaces the diagnostic command
c9433e8e314e Remove diagnostic command 'print_dependencies'.
ballarin
parents: 71348
diff changeset
    47
'print_dependencies', which was removed.
70794
d997c7ba3305 Tracing of locale activation.
ballarin
parents: 70791
diff changeset
    48
70708
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
    49
70873
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70871
diff changeset
    50
*** Isabelle/jEdit Prover IDE ***
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70871
diff changeset
    51
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70871
diff changeset
    52
* Prover IDE startup is now much faster, because theory dependencies are
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70871
diff changeset
    53
no longer explored in advance. The overall session structure with its
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70871
diff changeset
    54
declarations of 'directories' is sufficient to locate theory files. Thus
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70871
diff changeset
    55
the "session focus" of option "isabelle jedit -S" has become obsolete
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70871
diff changeset
    56
(likewise for "isabelle vscode_server -S"). Existing option "-R" is both
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70871
diff changeset
    57
sufficient and more convenient to start editing a particular session.
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70871
diff changeset
    58
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70871
diff changeset
    59
70522
48609a6af1a0 removed relics of ASCII syntax for indexed big operators
haftmann
parents: 70485
diff changeset
    60
*** HOL ***
48609a6af1a0 removed relics of ASCII syntax for indexed big operators
haftmann
parents: 70485
diff changeset
    61
71473
0c454a5d125d NEWS, CONTRIBUTORS, and documentation
traytel
parents: 71468
diff changeset
    62
* Improvements of the "lift_bnf" command:
0c454a5d125d NEWS, CONTRIBUTORS, and documentation
traytel
parents: 71468
diff changeset
    63
  - Add support for quotient types.
0c454a5d125d NEWS, CONTRIBUTORS, and documentation
traytel
parents: 71468
diff changeset
    64
  - Generate transfer rules for the lifted map/set/rel/pred
0c454a5d125d NEWS, CONTRIBUTORS, and documentation
traytel
parents: 71468
diff changeset
    65
    constants (theorems "<type>.<constant>_transfer_raw").
0c454a5d125d NEWS, CONTRIBUTORS, and documentation
traytel
parents: 71468
diff changeset
    66
70974
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
    67
* Term_XML.Encode/Decode.term uses compact representation of Const
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
    68
"typargs" from the given declaration environment. This also makes more
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
    69
sense for translations to lambda-calculi with explicit polymorphism.
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
    70
INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
    71
applications.
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
    72
70710
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
    73
* ASCII membership syntax concerning big operators for infimum and
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
    74
supremum is gone. INCOMPATIBILITY.
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
    75
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
    76
* Clear distinction between types for bits (False / True) and Z2 (0 /
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
    77
1): theory HOL/Library/Bit.thy has been renamed accordingly.
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
    78
INCOMPATIBILITY.
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
    79
71007
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70974
diff changeset
    80
* Fact collections algebra_split_simps and field_split_simps correspond
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70974
diff changeset
    81
to algebra_simps and field_simps but contain more aggressive rules
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70974
diff changeset
    82
potentially splitting goals; algebra_split_simps roughly replaces
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70974
diff changeset
    83
sign_simps and field_split_simps can be used instead of divide_simps.
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70974
diff changeset
    84
INCOMPATIBILITY.
70710
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
    85
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
    86
* Theory HOL-Library.Monad_Syntax: infix operation "bind" (>>=)
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
    87
associates to the left now as is customary.
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
    88
71468
09aee7f5b447 Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents: 71364
diff changeset
    89
* Theory HOL-Library.Ramsey: full finite Ramsey's theorem with
09aee7f5b447 Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents: 71364
diff changeset
    90
multiple colours and arbitrary exponents.
09aee7f5b447 Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents: 71364
diff changeset
    91
71146
nipkow
parents: 71007
diff changeset
    92
* Theory Complete_Lattices:
nipkow
parents: 71007
diff changeset
    93
renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf
70620
4abd07cd034f News for bind infixl
nipkow
parents: 70532
diff changeset
    94
71345
wenzelm
parents: 71332
diff changeset
    95
* Session HOL-Analysis: proof method "metric" implements a decision
wenzelm
parents: 71332
diff changeset
    96
procedure for simple linear statements in metric spaces.
wenzelm
parents: 71332
diff changeset
    97
71347
a7d1fb0c9e16 proper prefix syntax
haftmann
parents: 71345
diff changeset
    98
* Word: Bitwise NOT-operator has proper prefix syntax.  Minor
a7d1fb0c9e16 proper prefix syntax
haftmann
parents: 71345
diff changeset
    99
INCOMPATIBILITY.
a7d1fb0c9e16 proper prefix syntax
haftmann
parents: 71345
diff changeset
   100
71348
9e7d40d67258 tuned whitespace
haftmann
parents: 71347
diff changeset
   101
70711
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   102
*** ML ***
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   103
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   104
* Theory construction may be forked internally, the operation
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   105
Theory.join_theory recovers a single result theory. See also the example
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   106
in theory "HOL-ex.Join_Theory".
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   107
70751
d0b75c59beca added ML antiquotation @{oracle_name};
wenzelm
parents: 70748
diff changeset
   108
* Antiquotation @{oracle_name} inlines a formally checked oracle name.
d0b75c59beca added ML antiquotation @{oracle_name};
wenzelm
parents: 70748
diff changeset
   109
70711
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   110
70785
wenzelm
parents: 70751
diff changeset
   111
*** System ***
wenzelm
parents: 70751
diff changeset
   112
71552
wenzelm
parents: 71534
diff changeset
   113
* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
wenzelm
parents: 71534
diff changeset
   114
have been discontinued -- deprecated since Isabelle2018.
wenzelm
parents: 71534
diff changeset
   115
71502
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   116
* The command-line tool "isabelle phabricator_setup" facilitates
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   117
self-hosting of the Phabricator software-development platform, with
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   118
support for Git, Mercurial, Subversion repositories. This helps to avoid
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   119
monoculture and to escape the gravity of centralized version control by
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   120
Github and/or Bitbucket. For further documentation, see chapter
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   121
"Phabricator server administration" in the "system" manual. A notable
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   122
example installation is https://isabelle-dev.sketis.net/.
71332
wenzelm
parents: 71153
diff changeset
   123
71534
wenzelm
parents: 71502
diff changeset
   124
* The command-line tool "isabelle hg_setup" simplifies the setup of
wenzelm
parents: 71502
diff changeset
   125
Mercurial repositories, with hosting via Phabricator or SSH file server
wenzelm
parents: 71502
diff changeset
   126
access.
wenzelm
parents: 71502
diff changeset
   127
70876
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70873
diff changeset
   128
* The command-line tool "isabelle imports" has been discontinued: strict
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70873
diff changeset
   129
checking of session directories enforces session-qualified theory names
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70873
diff changeset
   130
in applications -- users are responsible to specify session ROOT entries
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70873
diff changeset
   131
properly.
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70873
diff changeset
   132
70785
wenzelm
parents: 70751
diff changeset
   133
* Theory export via Isabelle/Scala has been reworked. The former "fact"
wenzelm
parents: 70751
diff changeset
   134
name space is now split into individual "thm" items: names are
wenzelm
parents: 70751
diff changeset
   135
potentially indexed, such as "foo" for singleton facts, or "bar(1)",
wenzelm
parents: 70751
diff changeset
   136
"bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now
wenzelm
parents: 70751
diff changeset
   137
exported as well: this spans an overall dependency graph of internal
wenzelm
parents: 70751
diff changeset
   138
inferences; it might help to reconstruct the formal structure of theory
wenzelm
parents: 70751
diff changeset
   139
libraries. See also the module Export_Theory in Isabelle/Scala.
wenzelm
parents: 70751
diff changeset
   140
70449
a8238fd25541 back to post-release mode;
wenzelm
parents: 70444
diff changeset
   141
70974
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
   142
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   143
New in Isabelle2019 (June 2019)
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   144
-------------------------------
68683
d69127c6e80f back to post-release mode -- after fork point;
wenzelm
parents: 68681
diff changeset
   145
69042
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   146
*** General ***
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   147
70214
0674c24afc5e updated for release;
wenzelm
parents: 70213
diff changeset
   148
* The font collection "Isabelle DejaVu" is systematically derived from
0674c24afc5e updated for release;
wenzelm
parents: 70213
diff changeset
   149
the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif"
69353
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   150
and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   151
The DejaVu base fonts are retricted to well-defined Unicode ranges and
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   152
augmented by special Isabelle symbols, taken from the former
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   153
"IsabelleText" font (which is no longer provided separately). The line
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   154
metrics and overall rendering quality is closer to original DejaVu.
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   155
INCOMPATIBILITY with display configuration expecting the old
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   156
"IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead.
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   157
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   158
* The Isabelle fonts render "\<inverse>" properly as superscript "-1".
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   159
69042
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   160
* Old-style inner comments (* ... *) within the term language are no
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   161
longer supported (legacy feature in Isabelle2018).
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   162
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   163
* Old-style {* verbatim *} tokens are explicitly marked as legacy
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   164
feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   165
via "isabelle update_cartouches -t" (available since Isabelle2015).
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   166
70482
wenzelm
parents: 70466
diff changeset
   167
* Infix operators that begin or end with a "*" are now parenthesized
wenzelm
parents: 70466
diff changeset
   168
without additional spaces, e.g. "(*)" instead of "( * )". Minor
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   169
INCOMPATIBILITY.
69066
nipkow
parents: 69045
diff changeset
   170
69592
6f755e3cd95d mixfix annotations may use cartouches;
wenzelm
parents: 69579
diff changeset
   171
* Mixfix annotations may use cartouches instead of old-style double
69598
9171d1ce5a35 support for "isabelle update -u mixfix_cartouches";
wenzelm
parents: 69597
diff changeset
   172
quotes, e.g. (infixl \<open>+\<close> 60). The command-line tool "isabelle update -u
9171d1ce5a35 support for "isabelle update -u mixfix_cartouches";
wenzelm
parents: 69597
diff changeset
   173
mixfix_cartouches" allows to update existing theory sources
9171d1ce5a35 support for "isabelle update -u mixfix_cartouches";
wenzelm
parents: 69597
diff changeset
   174
automatically.
69592
6f755e3cd95d mixfix annotations may use cartouches;
wenzelm
parents: 69579
diff changeset
   175
69221
1a52baa70aed clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents: 69218
diff changeset
   176
* ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation')
1a52baa70aed clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents: 69218
diff changeset
   177
need to provide a closed expression -- without trailing semicolon. Minor
1a52baa70aed clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents: 69218
diff changeset
   178
INCOMPATIBILITY.
1a52baa70aed clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents: 69218
diff changeset
   179
70239
0403b5127da1 documentation for generated files;
wenzelm
parents: 70214
diff changeset
   180
* Commands 'generate_file', 'export_generated_files', and
0403b5127da1 documentation for generated files;
wenzelm
parents: 70214
diff changeset
   181
'compile_generated_files' support a stateless (PIDE-conformant) model
0403b5127da1 documentation for generated files;
wenzelm
parents: 70214
diff changeset
   182
for generated sources and compiled binaries of other languages. The
70242
wenzelm
parents: 70239
diff changeset
   183
compilation process is managed in Isabelle/ML, and results exported to
70239
0403b5127da1 documentation for generated files;
wenzelm
parents: 70214
diff changeset
   184
the session database for further use (e.g. with "isabelle export" or
0403b5127da1 documentation for generated files;
wenzelm
parents: 70214
diff changeset
   185
"isabelle build -e").
0403b5127da1 documentation for generated files;
wenzelm
parents: 70214
diff changeset
   186
69042
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   187
69190
wenzelm
parents: 69184
diff changeset
   188
*** Isabelle/jEdit Prover IDE ***
wenzelm
parents: 69184
diff changeset
   189
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   190
* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   191
DejaVu" collection by default, which provides uniform rendering quality
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   192
with the usual Isabelle symbols. Line spacing no longer needs to be
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   193
adjusted: properties for the old IsabelleText font had "Global Options /
70251
381035c03220 proper default;
wenzelm
parents: 70250
diff changeset
   194
Text Area / Extra vertical line spacing (in pixels): -2", it now
381035c03220 proper default;
wenzelm
parents: 70250
diff changeset
   195
defaults to 1, but 0 works as well.
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   196
69796
wenzelm
parents: 69794
diff changeset
   197
* The jEdit File Browser is more prominent in the default GUI layout of
wenzelm
parents: 69794
diff changeset
   198
Isabelle/jEdit: various virtual file-systems provide access to Isabelle
wenzelm
parents: 69794
diff changeset
   199
resources, notably via "favorites:" (or "Edit Favorites").
wenzelm
parents: 69794
diff changeset
   200
70243
5b75480f371a more NEWS;
wenzelm
parents: 70242
diff changeset
   201
* Further markup and rendering for "plain text" (e.g. informal prose)
5b75480f371a more NEWS;
wenzelm
parents: 70242
diff changeset
   202
and "raw text" (e.g. verbatim sources). This improves the visual
5b75480f371a more NEWS;
wenzelm
parents: 70242
diff changeset
   203
appearance of formal comments inside the term language, or in general
5b75480f371a more NEWS;
wenzelm
parents: 70242
diff changeset
   204
for repeated alternation of formal and informal text.
5b75480f371a more NEWS;
wenzelm
parents: 70242
diff changeset
   205
69656
83f15deb2d36 added action "isabelle-export-browser";
wenzelm
parents: 69637
diff changeset
   206
* Action "isabelle-export-browser" points the File Browser to the theory
69780
wenzelm
parents: 69771
diff changeset
   207
exports of the current buffer, based on the "isabelle-export:" virtual
wenzelm
parents: 69771
diff changeset
   208
file-system. The directory view needs to be reloaded manually to follow
wenzelm
parents: 69771
diff changeset
   209
ongoing document processing.
wenzelm
parents: 69771
diff changeset
   210
wenzelm
parents: 69771
diff changeset
   211
* Action "isabelle-session-browser" points the File Browser to session
wenzelm
parents: 69771
diff changeset
   212
information, based on the "isabelle-session:" virtual file-system. Its
wenzelm
parents: 69771
diff changeset
   213
entries are structured according to chapter / session names, the open
wenzelm
parents: 69771
diff changeset
   214
operation is redirected to the session ROOT file.
69656
83f15deb2d36 added action "isabelle-export-browser";
wenzelm
parents: 69637
diff changeset
   215
69278
wenzelm
parents: 69274
diff changeset
   216
* Support for user-defined file-formats via class isabelle.File_Format
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
   217
in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
   218
the shell function "isabelle_file_format" in etc/settings (e.g. of an
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
   219
Isabelle component).
69278
wenzelm
parents: 69274
diff changeset
   220
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   221
* System option "jedit_text_overview" allows to disable the text
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   222
overview column.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   223
70035
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   224
* Command-line options "-s" and "-u" of "isabelle jedit" override the
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   225
default for system option "system_heaps" that determines the heap
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   226
storage directory for "isabelle build". Option "-n" is now clearly
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   227
separated from option "-s".
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   228
70291
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   229
* The Isabelle/jEdit desktop application uses the same options as
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   230
"isabelle jedit" for its internal "isabelle build" process: the implicit
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   231
option "-o system_heaps" (or "-s") has been discontinued. This reduces
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   232
the potential for surprise wrt. command-line tools.
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   233
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   234
* The official download of the Isabelle/jEdit application already
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   235
contains heap images for Isabelle/HOL within its main directory: thus
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   236
the first encounter becomes faster and more robust (e.g. when run from a
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   237
read-only directory).
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   238
70254
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   239
* Isabelle DejaVu fonts are available with hinting by default, which is
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   240
relevant for low-resolution displays. This may be disabled via system
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   241
option "isabelle_fonts_hinted = false" in
70258
ee0b8e06b01c proper etc/preferences;
wenzelm
parents: 70254
diff changeset
   242
$ISABELLE_HOME_USER/etc/preferences -- it occasionally yields better
70254
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   243
results.
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   244
70213
wenzelm
parents: 70208
diff changeset
   245
* OpenJDK 11 has quite different font rendering, with better glyph
wenzelm
parents: 70208
diff changeset
   246
shapes and improved sub-pixel anti-aliasing. In some situations results
70254
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   247
might be *worse* than Oracle Java 8, though -- a proper HiDPI / UHD
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   248
display is recommended.
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   249
70442
b4534d72dd22 more NEWS;
wenzelm
parents: 70421
diff changeset
   250
* OpenJDK 11 supports GTK version 2.2 and 3 (according to system
b4534d72dd22 more NEWS;
wenzelm
parents: 70421
diff changeset
   251
property jdk.gtk.version). The factory default is version 3, but
b4534d72dd22 more NEWS;
wenzelm
parents: 70421
diff changeset
   252
ISABELLE_JAVA_SYSTEM_OPTIONS includes "-Djdk.gtk.version=2.2" to make
b4534d72dd22 more NEWS;
wenzelm
parents: 70421
diff changeset
   253
this more conservative (as in Java 8). Depending on the GTK theme
b4534d72dd22 more NEWS;
wenzelm
parents: 70421
diff changeset
   254
configuration, "-Djdk.gtk.version=3" might work better or worse.
b4534d72dd22 more NEWS;
wenzelm
parents: 70421
diff changeset
   255
69190
wenzelm
parents: 69184
diff changeset
   256
70144
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   257
*** Document preparation ***
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   258
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   259
* Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   260
are stripped from document output: the effect is to modify the semantic
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   261
presentation context or to emit markup to the PIDE document. Some
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   262
predefined markers are taken from the Dublin Core Metadata Initiative,
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   263
e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that
70466
wenzelm
parents: 70444
diff changeset
   264
can be retrieved from the document database.
70144
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   265
70325
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   266
* Old-style command tags %name are re-interpreted as markers with
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   267
proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   268
before. Potential INCOMPATIBILITY: multiple markers are composed in
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   269
canonical order, resulting in a reversed list of tags in the
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   270
presentation context.
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   271
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   272
* Marker \<^marker>\<open>tag name\<close> does not apply to the proof of a top-level goal
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   273
statement by default (e.g. 'theorem', 'lemma'). This is a subtle change
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   274
of semantics wrt. old-style %name.
70144
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   275
70328
0cc7fe616924 more abbrevs;
wenzelm
parents: 70325
diff changeset
   276
* In Isabelle/jEdit, the string "\tag" may be completed to a "\<^marker>\<open>tag \<close>"
0cc7fe616924 more abbrevs;
wenzelm
parents: 70325
diff changeset
   277
template.
0cc7fe616924 more abbrevs;
wenzelm
parents: 70325
diff changeset
   278
70307
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70292
diff changeset
   279
* Document antiquotation option "cartouche" indicates if the output
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70292
diff changeset
   280
should be delimited as cartouche; this takes precedence over the
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70292
diff changeset
   281
analogous option "quotes".
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70292
diff changeset
   282
70308
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   283
* Many document antiquotations are internally categorized as "embedded"
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   284
and expect one cartouche argument, which is typically used with the
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   285
\<^control>\<open>cartouche\<close> notation (e.g. \<^term>\<open>\<lambda>x y. x\<close>). The cartouche
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   286
delimiters are stripped in output of the source (antiquotation option
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   287
"source"), but it is possible to enforce delimiters via option
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   288
"source_cartouche", e.g. @{term [source_cartouche] \<open>\<lambda>x y. x\<close>}.
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   289
70144
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   290
68879
wenzelm
parents: 68848
diff changeset
   291
*** Isar ***
wenzelm
parents: 68848
diff changeset
   292
69045
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
   293
* Implicit cases goal1, goal2, goal3, etc. have been discontinued
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
   294
(legacy feature since Isabelle2016).
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
   295
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   296
* More robust treatment of structural errors: begin/end blocks take
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   297
precedence over goal/proof. This is particularly relevant for the
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   298
headless PIDE session and server.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   299
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   300
* Command keywords of kind thy_decl / thy_goal may be more specifically
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   301
fit into the traditional document model of "definition-statement-proof"
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   302
via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   303
69045
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
   304
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   305
*** HOL ***
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   306
70191
435fb018e8ee "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents: 70144
diff changeset
   307
* Command 'export_code' produces output as logical files within the
70193
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   308
theory context, as well as formal session exports that can be
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   309
materialized via command-line tools "isabelle export" or "isabelle build
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   310
-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   311
provides a virtual file-system "isabelle-export:" that can be explored
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   312
in the regular file-browser. A 'file_prefix' argument allows to specify
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   313
an explicit name prefix for the target file (SML, OCaml, Scala) or
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   314
directory (Haskell); the default is "export" with a consecutive number
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   315
within each theory.
70191
435fb018e8ee "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents: 70144
diff changeset
   316
435fb018e8ee "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents: 70144
diff changeset
   317
* Command 'export_code': the 'file' argument is now legacy and will be
435fb018e8ee "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents: 70144
diff changeset
   318
removed soon: writing to the physical file-system is not well-defined in
70193
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   319
a reactive/parallel application like Isabelle. The empty 'file' argument
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   320
has been discontinued already: it is superseded by the file-browser in
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   321
Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.
69637
e02bdf853a4c optional code export as theory export
haftmann
parents: 69622
diff changeset
   322
70204
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70193
diff changeset
   323
* Command 'code_reflect' no longer supports the 'file' argument: it has
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70193
diff changeset
   324
been superseded by 'file_prefix' for stateless file management as in
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70193
diff changeset
   325
'export_code'. Minor INCOMPATIBILITY.
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70193
diff changeset
   326
69759
6a9a8ef5e4c6 prefer proper strings in OCaml
haftmann
parents: 69749
diff changeset
   327
* Code generation for OCaml: proper strings are used for literals.
6a9a8ef5e4c6 prefer proper strings in OCaml
haftmann
parents: 69749
diff changeset
   328
Minor INCOMPATIBILITY.
6a9a8ef5e4c6 prefer proper strings in OCaml
haftmann
parents: 69749
diff changeset
   329
70108
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
   330
* Code generation for OCaml: Zarith supersedes Nums as library for
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
   331
proper integer arithmetic. The library is located via standard
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
   332
invocations of "ocamlfind" (via ISABELLE_OCAMLFIND settings variable).
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
   333
The environment provided by "isabelle ocaml_setup" already contains this
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
   334
tool and the required packages. Minor INCOMPATIBILITY.
70087
55534affe445 migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents: 70084
diff changeset
   335
69705
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69686
diff changeset
   336
* Code generation for Haskell: code includes for Haskell must contain
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69686
diff changeset
   337
proper module frame, nothing is added magically any longer.
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69686
diff changeset
   338
INCOMPATIBILITY.
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69686
diff changeset
   339
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   340
* Code generation: slightly more conventional syntax for 'code_stmts'
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   341
antiquotation. Minor INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   342
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   343
* Theory List: the precedence of the list_update operator has changed:
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   344
"f a [n := x]" now needs to be written "(f a)[n := x]".
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   345
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   346
* The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter> (not the corresponding binding operators)
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   347
now have the same precedence as any other prefix function symbol. Minor
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   348
INCOMPATIBILITY.
70042
62e47f06d22c avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents: 70035
diff changeset
   349
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   350
* Simplified syntax setup for big operators under image. In rare
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   351
situations, type conversions are not inserted implicitly any longer
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   352
and need to be given explicitly. Auxiliary abbreviations INFIMUM,
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   353
SUPREMUM, UNION, INTER should now rarely occur in output and are just
70421
7e9269c188d6 more NEWS
haftmann
parents: 70400
diff changeset
   354
retained as migration auxiliary. Abbreviations MINIMUM and MAXIMUM
7e9269c188d6 more NEWS
haftmann
parents: 70400
diff changeset
   355
are gone INCOMPATIBILITY.
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   356
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   357
* The simplifier uses image_cong_simp as a congruence rule. The historic
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   358
and not really well-formed congruence rules INF_cong*, SUP_cong*, are
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   359
not used by default any longer. INCOMPATIBILITY; consider using declare
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   360
image_cong_simp [cong del] in extreme situations.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   361
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   362
* INF_image and SUP_image are no default simp rules any longer.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   363
INCOMPATIBILITY, prefer image_comp as simp rule if needed.
68938
a0b19a163f5e left-over rename from 3f9bb52082c4
haftmann
parents: 68883
diff changeset
   364
69164
74f1b0f10b2b uniform naming of strong congruence rules
nipkow
parents: 69155
diff changeset
   365
* Strong congruence rules (with =simp=> in the premises) for constant f
69558
27dae626822b prefer naming convention from datatype package for strong congruence rules
haftmann
parents: 69518
diff changeset
   366
are now uniformly called f_cong_simp, in accordance with congruence
27dae626822b prefer naming convention from datatype package for strong congruence rules
haftmann
parents: 69518
diff changeset
   367
rules produced for mappers by the datatype package. INCOMPATIBILITY.
69164
74f1b0f10b2b uniform naming of strong congruence rules
nipkow
parents: 69155
diff changeset
   368
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   369
* Retired lemma card_Union_image; use the simpler card_UN_disjoint
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   370
instead. INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   371
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   372
* Facts sum_mset.commute and prod_mset.commute have been renamed to
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   373
sum_mset.swap and prod_mset.swap, similarly to sum.swap and prod.swap.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   374
INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   375
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   376
* ML structure Inductive: slightly more conventional naming schema.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   377
Minor INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   378
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   379
* ML: Various _global variants of specification tools have been removed.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   380
Minor INCOMPATIBILITY, prefer combinators
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   381
Named_Target.theory_map[_result] to lift specifications to the global
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   382
theory level.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   383
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   384
* Theory HOL-Library.Simps_Case_Conv: 'case_of_simps' now supports
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   385
overlapping and non-exhaustive patterns and handles arbitrarily nested
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   386
patterns. It uses on the same algorithm as HOL-Library.Code_Lazy, which
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   387
assumes sequential left-to-right pattern matching. The generated
69569
de09a7261120 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents: 69518
diff changeset
   388
equation no longer tuples the arguments on the right-hand side.
de09a7261120 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents: 69518
diff changeset
   389
INCOMPATIBILITY.
de09a7261120 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents: 69518
diff changeset
   390
70482
wenzelm
parents: 70466
diff changeset
   391
* Theory HOL-Library.Multiset: the \<Union># operator now has the same
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   392
precedence as any other prefix function symbol.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   393
70263
traytel
parents: 70258
diff changeset
   394
* Theory HOL-Library.Cardinal_Notations has been discontinued in favor
70352
e79bbf86a984 tuned for release;
wenzelm
parents: 70348
diff changeset
   395
of the bundle cardinal_syntax (available in theory Main). Minor
e79bbf86a984 tuned for release;
wenzelm
parents: 70348
diff changeset
   396
INCOMPATIBILITY.
70263
traytel
parents: 70258
diff changeset
   397
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   398
* Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring,
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   399
used for computing powers in class "monoid_mult" and modular
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   400
exponentiation.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   401
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   402
* Session HOL-Computational_Algebra: Formal Laurent series and overhaul
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   403
of Formal power series.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   404
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   405
* Session HOL-Number_Theory: More material on residue rings in
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   406
Carmichael's function, primitive roots, more properties for "ord".
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   407
70300
b601c2c87076 type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents: 70292
diff changeset
   408
* Session HOL-Analysis: Better organization and much more material
b601c2c87076 type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents: 70292
diff changeset
   409
at the level of abstract topological spaces.
b601c2c87076 type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents: 70292
diff changeset
   410
70348
1f163f772da3 Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)
paulson <lp15@cam.ac.uk>
parents: 70328
diff changeset
   411
* Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
70400
8371a25ca177 Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents: 70359
diff changeset
   412
 algebraic closure of a field by de Vilhena and Baillon.
70214
0674c24afc5e updated for release;
wenzelm
parents: 70213
diff changeset
   413
70352
e79bbf86a984 tuned for release;
wenzelm
parents: 70348
diff changeset
   414
* Session HOL-Homology has been added. It is a port of HOL Light's
e79bbf86a984 tuned for release;
wenzelm
parents: 70348
diff changeset
   415
homology library, with new proofs of "invariance of domain" and related
e79bbf86a984 tuned for release;
wenzelm
parents: 70348
diff changeset
   416
results.
e79bbf86a984 tuned for release;
wenzelm
parents: 70348
diff changeset
   417
69099
d44cb8a3e5e0 HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents: 69095
diff changeset
   418
* Session HOL-SPARK: .prv files are no longer written to the
d44cb8a3e5e0 HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents: 69095
diff changeset
   419
file-system, but exported to the session database. Results may be
70208
6ae9505d693a more convenient export;
wenzelm
parents: 70205
diff changeset
   420
retrieved via "isabelle build -e HOL-SPARK-Examples" on the
6ae9505d693a more convenient export;
wenzelm
parents: 70205
diff changeset
   421
command-line.
69099
d44cb8a3e5e0 HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents: 69095
diff changeset
   422
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   423
* Sledgehammer:
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   424
  - The URL for SystemOnTPTP, which is used by remote provers, has been
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   425
    updated.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   426
  - The machine-learning-based filter MaSh has been optimized to take
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   427
    less time (in most cases).
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   428
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   429
* SMT: reconstruction is now possible using the SMT solver veriT.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   430
70358
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70352
diff changeset
   431
* Session HOL-Word:
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70352
diff changeset
   432
  * New theory More_Word as comprehensive entrance point.
70359
85fb1a585f52 eliminated type class
haftmann
parents: 70358
diff changeset
   433
  * Merged type class bitss into type class bits.
70358
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70352
diff changeset
   434
  INCOMPATIBILITY.
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70352
diff changeset
   435
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   436
68804
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
   437
*** ML ***
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
   438
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   439
* Command 'generate_file' allows to produce sources for other languages,
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   440
with antiquotations in the Isabelle context (only the control-cartouche
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   441
form). The default "cartouche" antiquotation evaluates an ML expression
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   442
of type string and inlines the result as a string literal of the target
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   443
language. For example, this works for Haskell as follows:
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   444
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   445
  generate_file "Pure.hs" = \<open>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   446
  module Isabelle.Pure where
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   447
    allConst, impConst, eqConst :: String
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   448
    allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   449
    impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   450
    eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   451
  \<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   452
70268
4f936de6d9b8 tuned -- prefer Isar command 'compile_generated_files';
wenzelm
parents: 70263
diff changeset
   453
See also commands 'export_generated_files' and 'compile_generated_files'
4f936de6d9b8 tuned -- prefer Isar command 'compile_generated_files';
wenzelm
parents: 70263
diff changeset
   454
to use the results.
68804
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
   455
70444
22cfcfcadd8b more documentation;
wenzelm
parents: 70442
diff changeset
   456
* ML evaluation (notably via command 'ML' or 'ML_file') is subject to
68824
7414ce0256e1 some NEWS (instead of proper documentation);
wenzelm
parents: 68804
diff changeset
   457
option ML_environment to select a named environment, such as "Isabelle"
70444
22cfcfcadd8b more documentation;
wenzelm
parents: 70442
diff changeset
   458
for Isabelle/ML, or "SML" for official Standard ML.
68804
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
   459
69391
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69387
diff changeset
   460
* ML antiquotation @{master_dir} refers to the master directory of the
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69387
diff changeset
   461
underlying theory, i.e. the directory of the theory file.
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69387
diff changeset
   462
69481
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69391
diff changeset
   463
* ML antiquotation @{verbatim} inlines its argument as string literal,
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69391
diff changeset
   464
preserving newlines literally. The short form \<^verbatim>\<open>abc\<close> is particularly
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69391
diff changeset
   465
useful.
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69391
diff changeset
   466
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   467
* Local_Theory.reset is no longer available in user space. Regular
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   468
definitional packages should use balanced blocks of
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   469
Local_Theory.open_target versus Local_Theory.close_target instead, or
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   470
the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   471
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   472
* Original PolyML.pointerEq is retained as a convenience for tools that
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   473
don't use Isabelle/ML (where this is called "pointer_eq").
69391
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69387
diff changeset
   474
69287
94fa3376ba33 added ML antiquotation @{master_dir};
wenzelm
parents: 69282
diff changeset
   475
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
   476
*** System ***
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
   477
70213
wenzelm
parents: 70208
diff changeset
   478
* Update to OpenJDK 11: the current long-term support version of Java.
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   479
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   480
* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   481
the full overhead of 64-bit values everywhere. This special x86_64_32
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   482
mode provides up to 16GB ML heap, while program code and stacks are
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   483
allocated elsewhere. Thus approx. 5 times more memory is available for
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   484
applications compared to old x86 mode (which is no longer used by
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   485
Isabelle). The switch to the x86_64 CPU architecture also avoids
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   486
compatibility problems with Linux and macOS, where 32-bit applications
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   487
are gradually phased out.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   488
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   489
* System option "checkpoint" has been discontinued: obsolete thanks to
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   490
improved memory management in Poly/ML.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   491
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   492
* System option "system_heaps" determines where to store the session
70035
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   493
image of "isabelle build" (and other tools using that internally).
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   494
Former option "-s" is superseded by option "-o system_heaps".
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   495
INCOMPATIBILITY in command-line syntax.
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   496
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   497
* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   498
source modules for Isabelle tools implemented in Haskell, notably for
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   499
Isabelle/PIDE.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   500
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   501
* The command-line tool "isabelle build -e" retrieves theory exports
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   502
from the session build database, using 'export_files' in session ROOT
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   503
entries.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   504
69597
wenzelm
parents: 69592
diff changeset
   505
* The command-line tool "isabelle update" uses Isabelle/PIDE in
wenzelm
parents: 69592
diff changeset
   506
batch-mode to update theory sources based on semantic markup produced in
69622
wenzelm
parents: 69604
diff changeset
   507
Isabelle/ML. Actual updates depend on system options that may be enabled
69600
wenzelm
parents: 69598
diff changeset
   508
via "-u OPT" (for "update_OPT"), see also $ISABELLE_HOME/etc/options
wenzelm
parents: 69598
diff changeset
   509
section "Theory update". Theory sessions are specified as in "isabelle
69597
wenzelm
parents: 69592
diff changeset
   510
dump".
wenzelm
parents: 69592
diff changeset
   511
69604
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69600
diff changeset
   512
* The command-line tool "isabelle update -u control_cartouches" changes
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69600
diff changeset
   513
antiquotations into control-symbol format (where possible): @{NAME}
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69600
diff changeset
   514
becomes \<^NAME> and @{NAME ARG} becomes \<^NAME>\<open>ARG\<close>.
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69600
diff changeset
   515
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
   516
* Support for Isabelle command-line tools defined in Isabelle/Scala.
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
   517
Instances of class Isabelle_Scala_Tools may be configured via the shell
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
   518
function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
   519
component).
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
   520
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   521
* Isabelle Server command "use_theories" supports "nodes_status_delay"
69044
wenzelm
parents: 69042
diff changeset
   522
for continuous output of node status information. The time interval is
wenzelm
parents: 69042
diff changeset
   523
specified in seconds; a negative value means it is disabled (default).
wenzelm
parents: 69042
diff changeset
   524
wenzelm
parents: 69042
diff changeset
   525
* Isabelle Server command "use_theories" terminates more robustly in the
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
   526
presence of structurally broken sources: full consolidation of theories
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
   527
is no longer required.
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
   528
70108
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
   529
* OCaml tools and libraries are now accesed via ISABELLE_OCAMLFIND,
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
   530
which needs to point to a suitable version of "ocamlfind" (e.g. via
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
   531
OPAM, see below). INCOMPATIBILITY: settings variables ISABELLE_OCAML and
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
   532
ISABELLE_OCAMLC are no longer supported.
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
   533
69273
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   534
* Support for managed installations of Glasgow Haskell Compiler and
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   535
OCaml via the following command-line tools:
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   536
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   537
  isabelle ghc_setup
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   538
  isabelle ghc_stack
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   539
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   540
  isabelle ocaml_setup
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   541
  isabelle ocaml_opam
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   542
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   543
The global installation state is determined by the following settings
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   544
(and corresponding directory contents):
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   545
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   546
  ISABELLE_STACK_ROOT
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   547
  ISABELLE_STACK_RESOLVER
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   548
  ISABELLE_GHC_VERSION
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   549
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   550
  ISABELLE_OPAM_ROOT
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   551
  ISABELLE_OCAML_VERSION
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   552
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   553
After setup, the following Isabelle settings are automatically
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   554
redirected (overriding existing user settings):
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   555
69274
1bee990d443c tuned whitespace;
wenzelm
parents: 69273
diff changeset
   556
  ISABELLE_GHC
1bee990d443c tuned whitespace;
wenzelm
parents: 69273
diff changeset
   557
70108
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
   558
  ISABELLE_OCAMLFIND
69273
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   559
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   560
The old meaning of these settings as locally installed executables may
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
   561
be recovered by purging the directories ISABELLE_STACK_ROOT /
70108
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
   562
ISABELLE_OPAM_ROOT, or by resetting these variables in
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
   563
$ISABELLE_HOME_USER/etc/settings.
69190
wenzelm
parents: 69184
diff changeset
   564
70002
8c587dd44f51 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents: 69990
diff changeset
   565
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
   566
68392
9b4f60bdad54 updated for release;
wenzelm
parents: 68373
diff changeset
   567
New in Isabelle2018 (August 2018)
9b4f60bdad54 updated for release;
wenzelm
parents: 68373
diff changeset
   568
---------------------------------
66653
435cb8d69e27 back to post-release mode -- after fork point;
wenzelm
parents: 66652
diff changeset
   569
66712
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 66690
diff changeset
   570
*** General ***
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 66690
diff changeset
   571
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   572
* Session-qualified theory names are mandatory: it is no longer possible
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   573
to refer to unqualified theories from the parent session.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   574
INCOMPATIBILITY for old developments that have not been updated to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   575
Isabelle2017 yet (using the "isabelle imports" tool).
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   576
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   577
* Only the most fundamental theory names are global, usually the entry
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   578
points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   579
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   580
formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   581
68559
7aae213d9e69 discontinued pending_shyps: too much complication due to lazy facts;
wenzelm
parents: 68548
diff changeset
   582
* Global facts need to be closed: no free variables and no hypotheses.
7aae213d9e69 discontinued pending_shyps: too much complication due to lazy facts;
wenzelm
parents: 68548
diff changeset
   583
Rare INCOMPATIBILITY.
68540
000a0e062529 disallow pending hyps;
wenzelm
parents: 68523
diff changeset
   584
68665
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
   585
* Facts stemming from locale interpretation are subject to lazy
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
   586
evaluation for improved performance. Rare INCOMPATIBILITY: errors
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
   587
stemming from interpretation morphisms might be deferred and thus
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
   588
difficult to locate; enable system option "strict_facts" temporarily to
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
   589
avoid this.
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
   590
67446
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
   591
* Marginal comments need to be written exclusively in the new-style form
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
   592
"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
   593
supported. INCOMPATIBILITY, use the command-line tool "isabelle
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
   594
update_comments" to update existing theory files.
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
   595
67507
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
   596
* Old-style inner comments (* ... *) within the term language are legacy
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
   597
and will be discontinued soon: use formal comments "\<comment> \<open>...\<close>" or "\<^cancel>\<open>...\<close>"
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
   598
instead.
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
   599
67402
nipkow
parents: 67400
diff changeset
   600
* The "op <infix-op>" syntax for infix operators has been replaced by
67400
nipkow
parents: 67398
diff changeset
   601
"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
nipkow
parents: 67398
diff changeset
   602
be a space between the "*" and the corresponding parenthesis.
68543
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   603
INCOMPATIBILITY, use the command-line tool "isabelle update_op" to
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   604
convert theory and ML files to the new syntax. Because it is based on
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   605
regular expression matching, the result may need a bit of manual
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   606
postprocessing. Invoking "isabelle update_op" converts all files in the
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   607
current directory (recursively). In case you want to exclude conversion
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   608
of ML files (because the tool frequently also converts ML's "op"
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   609
syntax), use option "-m".
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67395
diff changeset
   610
67013
335a7dce7cb3 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents: 66994
diff changeset
   611
* Theory header 'abbrevs' specifications need to be separated by 'and'.
335a7dce7cb3 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents: 66994
diff changeset
   612
INCOMPATIBILITY.
335a7dce7cb3 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents: 66994
diff changeset
   613
66757
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
   614
* Command 'external_file' declares the formal dependency on the given
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
   615
file name, such that the Isabelle build process knows about it, but
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
   616
without specific Prover IDE management.
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
   617
66759
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
   618
* Session ROOT entries no longer allow specification of 'files'. Rare
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
   619
INCOMPATIBILITY, use command 'external_file' within a proper theory
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
   620
context.
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
   621
66764
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
   622
* Session root directories may be specified multiple times: each
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
   623
accessible ROOT file is processed only once. This facilitates
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
   624
specification of $ISABELLE_HOME_USER/ROOTS or command-line options like
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
   625
-d or -D for "isabelle build" and "isabelle jedit". Example:
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
   626
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
   627
  isabelle build -D '~~/src/ZF'
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
   628
67264
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67263
diff changeset
   629
* The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67263
diff changeset
   630
use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67263
diff changeset
   631
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   632
* In HTML output, the Isabelle symbol "\<hyphen>" is rendered as explicit
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   633
Unicode hyphen U+2010, to avoid unclear meaning of the old "soft hyphen"
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   634
U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   635
output.
67305
ecb74607063f more robust hyphen (see also "Soft hyphen (SHY) – a hard problem?" http://jkorpela.fi/shy.html);
wenzelm
parents: 67304
diff changeset
   636
66712
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 66690
diff changeset
   637
67262
wenzelm
parents: 67248
diff changeset
   638
*** Isabelle/jEdit Prover IDE ***
66768
f27488f47a47 completion supports theory header imports;
wenzelm
parents: 66764
diff changeset
   639
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   640
* The command-line tool "isabelle jedit" provides more flexible options
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   641
for session management:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   642
68472
581a1bfec8ad clarified documentation;
wenzelm
parents: 68470
diff changeset
   643
  - option -R builds an auxiliary logic image with all theories from
581a1bfec8ad clarified documentation;
wenzelm
parents: 68470
diff changeset
   644
    other sessions that are not already present in its parent
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   645
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   646
  - option -S is like -R, with a focus on the selected session and its
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   647
    descendants (this reduces startup time for big projects like AFP)
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   648
68472
581a1bfec8ad clarified documentation;
wenzelm
parents: 68470
diff changeset
   649
  - option -A specifies an alternative ancestor session for options -R
581a1bfec8ad clarified documentation;
wenzelm
parents: 68470
diff changeset
   650
    and -S
581a1bfec8ad clarified documentation;
wenzelm
parents: 68470
diff changeset
   651
68541
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68540
diff changeset
   652
  - option -i includes additional sessions into the name-space of
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68540
diff changeset
   653
    theories
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68540
diff changeset
   654
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   655
  Examples:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   656
    isabelle jedit -R HOL-Number_Theory
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   657
    isabelle jedit -R HOL-Number_Theory -A HOL
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   658
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   659
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
68541
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68540
diff changeset
   660
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   661
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   662
* PIDE markup for session ROOT files: allows to complete session names,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   663
follow links to theories and document files etc.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   664
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   665
* Completion supports theory header imports, using theory base name.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   666
E.g. "Prob" may be completed to "HOL-Probability.Probability".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   667
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   668
* Named control symbols (without special Unicode rendering) are shown as
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   669
bold-italic keyword. This is particularly useful for the short form of
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   670
antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   671
"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   672
arguments into this format.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   673
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   674
* Completion provides templates for named symbols with arguments,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   675
e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   676
68369
wenzelm
parents: 68365
diff changeset
   677
* Slightly more parallel checking, notably for high priority print
wenzelm
parents: 68365
diff changeset
   678
functions (e.g. State output).
wenzelm
parents: 68365
diff changeset
   679
68080
17f79ae49401 set view title dynamically;
wenzelm
parents: 68072
diff changeset
   680
* The view title is set dynamically, according to the Isabelle
17f79ae49401 set view title dynamically;
wenzelm
parents: 68072
diff changeset
   681
distribution and the logic session name. The user can override this via
17f79ae49401 set view title dynamically;
wenzelm
parents: 68072
diff changeset
   682
set-view-title (stored persistently in $JEDIT_SETTINGS/perspective.xml).
17f79ae49401 set view title dynamically;
wenzelm
parents: 68072
diff changeset
   683
67395
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67381
diff changeset
   684
* System options "spell_checker_include" and "spell_checker_exclude"
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67381
diff changeset
   685
supersede former "spell_checker_elements" to determine regions of text
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67381
diff changeset
   686
that are subject to spell-checking. Minor INCOMPATIBILITY.
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67381
diff changeset
   687
67248
68177abb2988 isabelle.preview presents bibtex database files as well;
wenzelm
parents: 67246
diff changeset
   688
* Action "isabelle.preview" is able to present more file formats,
67267
wenzelm
parents: 67264
diff changeset
   689
notably bibtex database files and ML files.
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67224
diff changeset
   690
67263
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67262
diff changeset
   691
* Action "isabelle.draft" is similar to "isabelle.preview", but shows a
68068
b91c4acc1aaf clarified menu actions;
wenzelm
parents: 68034
diff changeset
   692
plain-text document draft. Both are available via the menu "Plugins /
b91c4acc1aaf clarified menu actions;
wenzelm
parents: 68034
diff changeset
   693
Isabelle".
67263
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67262
diff changeset
   694
67304
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
   695
* When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
   696
is only used if there is no conflict with existing Unicode sequences in
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
   697
the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
   698
symbols remain in literal \<symbol> form. This avoids accidental loss of
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
   699
Unicode content when saving the file.
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
   700
68545
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68543
diff changeset
   701
* Bibtex database files (.bib) are semantically checked.
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68543
diff changeset
   702
67994
wenzelm
parents: 67929
diff changeset
   703
* Update to jedit-5.5.0, the latest release.
wenzelm
parents: 67929
diff changeset
   704
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67224
diff changeset
   705
67262
wenzelm
parents: 67248
diff changeset
   706
*** Isabelle/VSCode Prover IDE ***
wenzelm
parents: 67248
diff changeset
   707
wenzelm
parents: 67248
diff changeset
   708
* HTML preview of theories and other file-formats similar to
wenzelm
parents: 67248
diff changeset
   709
Isabelle/jEdit.
wenzelm
parents: 67248
diff changeset
   710
68690
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
   711
* Command-line tool "isabelle vscode_server" accepts the same options
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
   712
-A, -R, -S, -i for session selection as "isabelle jedit". This is
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
   713
relevant for isabelle.args configuration settings in VSCode. The former
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
   714
option -A (explore all known session files) has been discontinued: it is
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
   715
enabled by default, unless option -S is used to focus on a particular
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
   716
spot in the session structure. INCOMPATIBILITY.
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
   717
66768
f27488f47a47 completion supports theory header imports;
wenzelm
parents: 66764
diff changeset
   718
67140
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   719
*** Document preparation ***
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   720
67448
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   721
* Formal comments work uniformly in outer syntax, inner syntax (term
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   722
language), Isabelle/ML and some other embedded languages of Isabelle.
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   723
See also "Document comments" in the isar-ref manual. The following forms
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   724
are supported:
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   725
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   726
  - marginal text comment: \<comment> \<open>\<dots>\<close>
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   727
  - canceled source: \<^cancel>\<open>\<dots>\<close>
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   728
  - raw LaTeX: \<^latex>\<open>\<dots>\<close>
67413
2555713586c8 added \<^cancel> operator for unused text;
wenzelm
parents: 67402
diff changeset
   729
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 67368
diff changeset
   730
* Outside of the inner theory body, the default presentation context is
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 67368
diff changeset
   731
theory Pure. Thus elementary antiquotations may be used in markup
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 67368
diff changeset
   732
commands (e.g. 'chapter', 'section', 'text') and formal comments.
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 67368
diff changeset
   733
68513
88b0e63d58a5 updated documentation;
wenzelm
parents: 68484
diff changeset
   734
* System option "document_tags" specifies alternative command tags. This
88b0e63d58a5 updated documentation;
wenzelm
parents: 68484
diff changeset
   735
is occasionally useful to control the global visibility of commands via
88b0e63d58a5 updated documentation;
wenzelm
parents: 68484
diff changeset
   736
session options (e.g. in ROOT).
67140
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   737
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   738
* Document markup commands ('section', 'text' etc.) are implicitly
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   739
tagged as "document" and visible by default. This avoids the application
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   740
of option "document_tags" to these commands.
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   741
67145
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
   742
* Isabelle names are mangled into LaTeX macro names to allow the full
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
   743
identifier syntax with underscore, prime, digits. This is relevant for
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
   744
antiquotations in control symbol notation, e.g. \<^const_name> becomes
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
   745
\isactrlconstUNDERSCOREname.
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
   746
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   747
* Document preparation with skip_proofs option now preserves the content
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   748
more accurately: only terminal proof steps ('by' etc.) are skipped.
67297
86a099f896fc formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents: 67295
diff changeset
   749
68484
59793df7f853 clarified document antiquotation @{theory};
wenzelm
parents: 68472
diff changeset
   750
* Document antiquotation @{theory name} requires the long
59793df7f853 clarified document antiquotation @{theory};
wenzelm
parents: 68472
diff changeset
   751
session-qualified theory name: this is what users reading the text
59793df7f853 clarified document antiquotation @{theory};
wenzelm
parents: 68472
diff changeset
   752
normally need to import.
59793df7f853 clarified document antiquotation @{theory};
wenzelm
parents: 68472
diff changeset
   753
67219
81e9804b2014 added document antiquotation @{session name};
wenzelm
parents: 67215
diff changeset
   754
* Document antiquotation @{session name} checks and prints the given
81e9804b2014 added document antiquotation @{session name};
wenzelm
parents: 67215
diff changeset
   755
session name verbatim.
81e9804b2014 added document antiquotation @{session name};
wenzelm
parents: 67215
diff changeset
   756
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   757
* Document antiquotation @{cite} now checks the given Bibtex entries
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   758
against the Bibtex database files -- only in batch-mode session builds.
67157
d0657c8b7616 clarified document preparation vs. skip_proofs;
wenzelm
parents: 67145
diff changeset
   759
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 67173
diff changeset
   760
* Command-line tool "isabelle document" has been re-implemented in
67194
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67191
diff changeset
   761
Isabelle/Scala, with simplified arguments and explicit errors from the
67203
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67199
diff changeset
   762
latex and bibtex process. Minor INCOMPATIBILITY.
67173
e746db6db903 more explicit latex errors;
wenzelm
parents: 67157
diff changeset
   763
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   764
* Session ROOT entry: empty 'document_files' means there is no document
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   765
for this session. There is no need to specify options [document = false]
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   766
anymore.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   767
67140
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   768
67702
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67615
diff changeset
   769
*** Isar ***
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67615
diff changeset
   770
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67615
diff changeset
   771
* Command 'interpret' no longer exposes resulting theorems as literal
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67615
diff changeset
   772
facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67615
diff changeset
   773
improves modularity of proofs and scalability of locale interpretation.
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67615
diff changeset
   774
Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67615
diff changeset
   775
(e.g. use 'find_theorems' or 'try' to figure this out).
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67615
diff changeset
   776
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   777
* The old 'def' command has been discontinued (legacy since
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   778
Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   779
object-logic equality or equivalence.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   780
68543
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   781
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   782
*** Pure ***
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   783
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   784
* The inner syntax category "sort" now includes notation "_" for the
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   785
dummy sort: it is effectively ignored in type-inference.
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   786
67740
b6ce18784872 Proper rewrite morphisms in locale instances.
ballarin
parents: 67719
diff changeset
   787
* Rewrites clauses (keyword 'rewrites') were moved into the locale
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   788
expression syntax, where they are part of locale instances. In
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   789
interpretation commands rewrites clauses now need to occur before 'for'
68470
aad109fde9ec In interpretation commands, clarify what to do with definitions immediately subject to rewriting.
ballarin
parents: 68465
diff changeset
   790
and 'defines'. Rare INCOMPATIBILITY; definitions immediately subject to
aad109fde9ec In interpretation commands, clarify what to do with definitions immediately subject to rewriting.
ballarin
parents: 68465
diff changeset
   791
rewriting may need to be pulled up into the surrounding theory.
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   792
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   793
* For 'rewrites' clauses, if activating a locale instance fails, fall
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   794
back to reading the clause first. This helps avoid qualification of
67764
0f8cb5568b63 Drop rewrites after defines in interpretations.
ballarin
parents: 67741
diff changeset
   795
locale instances where the qualifier's sole purpose is avoiding
0f8cb5568b63 Drop rewrites after defines in interpretations.
ballarin
parents: 67741
diff changeset
   796
duplicate constant declarations.
67741
d5a7f2c54655 Fall back to reading rewrite morphism first if activation fails without it.
ballarin
parents: 67740
diff changeset
   797
68543
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   798
* Proof method "simp" now supports a new modifier "flip:" followed by a
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   799
list of theorems. Each of these theorems is removed from the simpset
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   800
(without warning if it is not there) and the symmetric version of the
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   801
theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto"
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   802
and friends the modifier is "simp flip:".
67719
17874d43d3b3 notation for dummy sort;
wenzelm
parents: 67702
diff changeset
   803
17874d43d3b3 notation for dummy sort;
wenzelm
parents: 67702
diff changeset
   804
66663
fdab65297bd6 real oracle
blanchet
parents: 66653
diff changeset
   805
*** HOL ***
fdab65297bd6 real oracle
blanchet
parents: 66653
diff changeset
   806
68568
cf01d04e94d7 more NEWS;
wenzelm
parents: 68559
diff changeset
   807
* Sledgehammer: bundled version of "vampire" (for non-commercial users)
cf01d04e94d7 more NEWS;
wenzelm
parents: 68559
diff changeset
   808
helps to avoid fragility of "remote_vampire" service.
cf01d04e94d7 more NEWS;
wenzelm
parents: 68559
diff changeset
   809
68028
1f9f973eed2a proper datatype for 8-bit characters
haftmann
parents: 68027
diff changeset
   810
* Clarified relationship of characters, strings and code generation:
1f9f973eed2a proper datatype for 8-bit characters
haftmann
parents: 68027
diff changeset
   811
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   812
  - Type "char" is now a proper datatype of 8-bit values.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   813
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   814
  - Conversions "nat_of_char" and "char_of_nat" are gone; use more
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   815
    general conversions "of_char" and "char_of" with suitable type
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   816
    constraints instead.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   817
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   818
  - The zero character is just written "CHR 0x00", not "0" any longer.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   819
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   820
  - Type "String.literal" (for code generation) is now isomorphic to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   821
    lists of 7-bit (ASCII) values; concrete values can be written as
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   822
    "STR ''...''" for sequences of printable characters and "STR 0x..."
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   823
    for one single ASCII code point given as hexadecimal numeral.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   824
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   825
  - Type "String.literal" supports concatenation "... + ..." for all
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   826
    standard target languages.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   827
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   828
  - Theory HOL-Library.Code_Char is gone; study the explanations
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   829
    concerning "String.literal" in the tutorial on code generation to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   830
    get an idea how target-language string literals can be converted to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   831
    HOL string values and vice versa.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   832
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   833
  - Session Imperative-HOL: operation "raise" directly takes a value of
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   834
    type "String.literal" as argument, not type "string".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   835
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   836
INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   837
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   838
* Code generation: Code generation takes an explicit option
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   839
"case_insensitive" to accomodate case-insensitive file systems.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   840
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   841
* Abstract bit operations as part of Main: push_bit, take_bit, drop_bit.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   842
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   843
* New, more general, axiomatization of complete_distrib_lattice. The
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   844
former axioms:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   845
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   846
  "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   847
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   848
are replaced by:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   849
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   850
  "Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   851
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   852
The instantiations of sets and functions as complete_distrib_lattice are
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   853
moved to Hilbert_Choice.thy because their proofs need the Hilbert choice
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   854
operator. The dual of this property is also proved in theory
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   855
HOL.Hilbert_Choice.
67831
07f5588f2735 Removed stray 'sledgehammer' invocation
Manuel Eberl <eberlm@in.tum.de>
parents: 67830
diff changeset
   856
67999
1b05f74f2e5f tidying up including contributions from Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents: 67994
diff changeset
   857
* New syntax for the minimum/maximum of a function over a finite set:
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   858
MIN x\<in>A. B and even MIN x. B (only useful for finite types), also MAX.
67999
1b05f74f2e5f tidying up including contributions from Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents: 67994
diff changeset
   859
67525
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
   860
* Clarifed theorem names:
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
   861
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
   862
  Min.antimono ~> Min.subset_imp
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
   863
  Max.antimono ~> Max.subset_imp
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
   864
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
   865
Minor INCOMPATIBILITY.
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
   866
66663
fdab65297bd6 real oracle
blanchet
parents: 66653
diff changeset
   867
* SMT module:
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   868
66663
fdab65297bd6 real oracle
blanchet
parents: 66653
diff changeset
   869
  - The 'smt_oracle' option is now necessary when using the 'smt' method
66664
4b10fa05423b document incompatibility
blanchet
parents: 66663
diff changeset
   870
    with a solver other than Z3. INCOMPATIBILITY.
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   871
66844
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   872
  - The encoding to first-order logic is now more complete in the
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   873
    presence of higher-order quantifiers. An 'smt_explicit_application'
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   874
    option has been added to control this. INCOMPATIBILITY.
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   875
66804
3f9bb52082c4 avoid name clashes on interpretation of abstract locales
haftmann
parents: 66803
diff changeset
   876
* Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
66844
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   877
sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   878
interpretation of abstract locales. INCOMPATIBILITY.
66804
3f9bb52082c4 avoid name clashes on interpretation of abstract locales
haftmann
parents: 66803
diff changeset
   879
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   880
* Predicate coprime is now a real definition, not a mere abbreviation.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   881
INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   882
66803
dd8922885a68 avoid trivial definition
haftmann
parents: 66801
diff changeset
   883
* Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
dd8922885a68 avoid trivial definition
haftmann
parents: 66801
diff changeset
   884
INCOMPATIBILITY.
dd8922885a68 avoid trivial definition
haftmann
parents: 66801
diff changeset
   885
68373
f254e383bfe9 NEWS: infinite products
paulson <lp15@cam.ac.uk>
parents: 68371
diff changeset
   886
* The relator rel_filter on filters has been strengthened to its
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   887
canonical categorical definition with better properties.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   888
INCOMPATIBILITY.
67615
1d005f514417 strengthen filter relator to canonical categorical definition with better properties
Andreas Lochbihler
parents: 67591
diff changeset
   889
68071
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents: 67999
diff changeset
   890
* Generalized linear algebra involving linear, span, dependent, dim
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents: 67999
diff changeset
   891
from type class real_vector to locales module and vector_space.
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents: 67999
diff changeset
   892
Renamed:
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   893
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   894
  span_inc ~> span_superset
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   895
  span_superset ~> span_base
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   896
  span_eq ~> span_eq_iff
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   897
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   898
INCOMPATIBILITY.
66844
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   899
66937
a1a4a5e2933a rule out pathologic instances
haftmann
parents: 66909
diff changeset
   900
* Class linordered_semiring_1 covers zero_less_one also, ruling out
a1a4a5e2933a rule out pathologic instances
haftmann
parents: 66909
diff changeset
   901
pathologic instances. Minor INCOMPATIBILITY.
a1a4a5e2933a rule out pathologic instances
haftmann
parents: 66909
diff changeset
   902
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   903
* Theory HOL.List: functions "sorted_wrt" and "sorted" now compare every
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   904
element in a list to all following elements, not just the next one.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   905
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   906
* Theory HOL.List syntax:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   907
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   908
  - filter-syntax "[x <- xs. P]" is no longer output syntax, but only
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   909
    input syntax
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   910
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   911
  - list comprehension syntax now supports tuple patterns in "pat <- xs"
68250
949d93804740 First step to remove nonstandard "[x <- xs. P]" syntax: only input
nipkow
parents: 68247
diff changeset
   912
68450
41de07c7a0f3 Map.empty now qualified to avoid name clashes
nipkow
parents: 68404
diff changeset
   913
* Theory Map: "empty" must now be qualified as "Map.empty".
41de07c7a0f3 Map.empty now qualified to avoid name clashes
nipkow
parents: 68404
diff changeset
   914
67051
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 67043
diff changeset
   915
* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 67043
diff changeset
   916
68103
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   917
* Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   918
clash with fact mod_mult_self4 (on more generic semirings).
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   919
INCOMPATIBILITY.
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   920
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   921
* Eliminated some theorem aliasses:
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   922
  even_times_iff ~> even_mult_iff
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   923
  mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   924
  even_of_nat ~> even_int_iff
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   925
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   926
INCOMPATIBILITY.
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   927
68157
057d5b4ce47e removed some non-essential rules
haftmann
parents: 68125
diff changeset
   928
* Eliminated some theorem duplicate variations:
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   929
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   930
  - dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   931
  - mod_Suc_eq_Suc_mod can be replaced by mod_Suc
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   932
  - mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   933
  - mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   934
  - the witness of mod_eqD can be given directly as "_ div _"
68157
057d5b4ce47e removed some non-essential rules
haftmann
parents: 68125
diff changeset
   935
057d5b4ce47e removed some non-essential rules
haftmann
parents: 68125
diff changeset
   936
INCOMPATIBILITY.
057d5b4ce47e removed some non-essential rules
haftmann
parents: 68125
diff changeset
   937
68260
61188c781cdd avoid overaggressive classical rule
haftmann
parents: 68250
diff changeset
   938
* Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   939
longer aggresively destroyed to "\<exists>q. m = d * q". INCOMPATIBILITY, adding
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   940
"elim!: dvd" to classical proof methods in most situations restores
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   941
broken proofs.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   942
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   943
* Theory HOL-Library.Conditional_Parametricity provides command
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   944
'parametric_constant' for proving parametricity of non-recursive
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   945
definitions. For constants that are not fully parametric the command
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   946
will infer conditions on relations (e.g., bi_unique, bi_total, or type
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   947
class conditions such as "respects 0") sufficient for parametricity. See
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   948
theory HOL-ex.Conditional_Parametricity_Examples for some examples.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   949
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   950
* Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   951
generator to generate code for algebraic types with lazy evaluation
68639
357fca99a65a more examples for Code_Lazy
Andreas Lochbihler
parents: 68568
diff changeset
   952
semantics even in call-by-value target languages. See the theories
68647
wenzelm
parents: 68640
diff changeset
   953
HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for some
wenzelm
parents: 68640
diff changeset
   954
examples.
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   955
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   956
* Theory HOL-Library.Landau_Symbols has been moved here from AFP.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   957
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   958
* Theory HOL-Library.Old_Datatype no longer provides the legacy command
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   959
'old_datatype'. INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   960
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   961
* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   962
instances of rat, real, complex as factorial rings etc. Import
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   963
HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   964
INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   965
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   966
* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   967
infix/prefix notation.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   968
68543
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   969
* Session HOL-Algebra: revamped with much new material. The set of
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   970
isomorphisms between two groups is now denoted iso rather than iso_set.
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   971
INCOMPATIBILITY.
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   972
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   973
* Session HOL-Analysis: the Arg function now respects the same interval
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
   974
as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi.
68495
d4312962161a Rationalisation of complex transcendentals, esp the Arg function
paulson <lp15@cam.ac.uk>
parents: 68484
diff changeset
   975
INCOMPATIBILITY.
d4312962161a Rationalisation of complex transcendentals, esp the Arg function
paulson <lp15@cam.ac.uk>
parents: 68484
diff changeset
   976
68548
wenzelm
parents: 68547
diff changeset
   977
* Session HOL-Analysis: the functions zorder, zer_poly, porder and
wenzelm
parents: 68547
diff changeset
   978
pol_poly have been redefined. All related lemmas have been reworked.
68532
7c6f812afdc4 NEWS and CONTRIBUTORS
Wenda Li <wl302@cam.ac.uk>
parents: 68523
diff changeset
   979
INCOMPATIBILITY.
7c6f812afdc4 NEWS and CONTRIBUTORS
Wenda Li <wl302@cam.ac.uk>
parents: 68523
diff changeset
   980
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   981
* Session HOL-Analysis: infinite products, Moebius functions, the
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   982
Riemann mapping theorem, the Vitali covering theorem,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
   983
change-of-variables results for integration and measures.
68260
61188c781cdd avoid overaggressive classical rule
haftmann
parents: 68250
diff changeset
   984
68647
wenzelm
parents: 68640
diff changeset
   985
* Session HOL-Real_Asymp: proof method "real_asymp" proves asymptotics
wenzelm
parents: 68640
diff changeset
   986
or real-valued functions (limits, "Big-O", etc.) automatically.
68681
wenzelm
parents: 68665
diff changeset
   987
See also ~~/src/HOL/Real_Asymp/Manual for some documentation.
68647
wenzelm
parents: 68640
diff changeset
   988
68545
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68543
diff changeset
   989
* Session HOL-Types_To_Sets: more tool support (unoverload_type combines
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68543
diff changeset
   990
internalize_sorts and unoverload) and larger experimental application
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68543
diff changeset
   991
(type based linear algebra transferred to linear algebra on subspaces).
68522
d9cbc1e8644d example for Types_To_Sets: transfer from type-based linear algebra to subspaces
immler
parents: 68515
diff changeset
   992
66653
435cb8d69e27 back to post-release mode -- after fork point;
wenzelm
parents: 66652
diff changeset
   993
68121
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68103
diff changeset
   994
*** ML ***
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68103
diff changeset
   995
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68103
diff changeset
   996
* Operation Export.export emits theory exports (arbitrary blobs), which
70142
eff4ff8ba515 NEWS for proper Isabelle version;
wenzelm
parents: 70108
diff changeset
   997
are stored persistently in the session build database.
68121
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68103
diff changeset
   998
68281
cbee43ff4ceb added command 'ML_export';
wenzelm
parents: 68260
diff changeset
   999
* Command 'ML_export' exports ML toplevel bindings to the global
cbee43ff4ceb added command 'ML_export';
wenzelm
parents: 68260
diff changeset
  1000
bootstrap environment of the ML process. This allows ML evaluation
cbee43ff4ceb added command 'ML_export';
wenzelm
parents: 68260
diff changeset
  1001
without a formal theory context, e.g. in command-line tools like
cbee43ff4ceb added command 'ML_export';
wenzelm
parents: 68260
diff changeset
  1002
"isabelle process".
cbee43ff4ceb added command 'ML_export';
wenzelm
parents: 68260
diff changeset
  1003
68121
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68103
diff changeset
  1004
66729
wenzelm
parents: 66712
diff changeset
  1005
*** System ***
wenzelm
parents: 66712
diff changeset
  1006
67088
89e82aed7813 Mac OS X 10.10 Yosemite is baseline;
wenzelm
parents: 67069
diff changeset
  1007
* Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no
89e82aed7813 Mac OS X 10.10 Yosemite is baseline;
wenzelm
parents: 67069
diff changeset
  1008
longer supported.
89e82aed7813 Mac OS X 10.10 Yosemite is baseline;
wenzelm
parents: 67069
diff changeset
  1009
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1010
* Linux and Windows/Cygwin is for x86_64 only, old 32bit platform
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1011
support has been discontinued.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1012
66906
03a96b8c7c06 updated to jdk-8u152, which is for x86_64 only;
wenzelm
parents: 66851
diff changeset
  1013
* Java runtime is for x86_64 only. Corresponding Isabelle settings have
03a96b8c7c06 updated to jdk-8u152, which is for x86_64 only;
wenzelm
parents: 66851
diff changeset
  1014
been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS,
03a96b8c7c06 updated to jdk-8u152, which is for x86_64 only;
wenzelm
parents: 66851
diff changeset
  1015
instead of former 32/64 variants. INCOMPATIBILITY.
03a96b8c7c06 updated to jdk-8u152, which is for x86_64 only;
wenzelm
parents: 66851
diff changeset
  1016
68004
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1017
* Old settings ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM should be
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1018
phased out due to unclear preference of 32bit vs. 64bit architecture.
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1019
Explicit GNU bash expressions are now preferred, for example (with
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1020
quotes):
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1021
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1022
  #Posix executables (Unix or Cygwin), with preference for 64bit
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1023
  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1024
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1025
  #native Windows or Unix executables, with preference for 64bit
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1026
  "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1027
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1028
  #native Windows (32bit) or Unix executables (preference for 64bit)
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1029
  "${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}"
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
  1030
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66739
diff changeset
  1031
* Command-line tool "isabelle build" supports new options:
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66739
diff changeset
  1032
  - option -B NAME: include session NAME and all descendants
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66739
diff changeset
  1033
  - option -S: only observe changes of sources, not heap images
66841
5c32a072ca8b added isablle build option -f;
wenzelm
parents: 66826
diff changeset
  1034
  - option -f: forces a fresh build
66737
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66729
diff changeset
  1035
68734
c14a2cc9b5ef isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents: 68690
diff changeset
  1036
* Command-line tool "isabelle build" options -c -x -B refer to
c14a2cc9b5ef isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents: 68690
diff changeset
  1037
descendants wrt. the session parent or import graph. Subtle
c14a2cc9b5ef isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents: 68690
diff changeset
  1038
INCOMPATIBILITY: options -c -x used to refer to the session parent graph
c14a2cc9b5ef isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents: 68690
diff changeset
  1039
only.
c14a2cc9b5ef isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents: 68690
diff changeset
  1040
66843
be08a7691c62 clarified meta_digest;
wenzelm
parents: 66841
diff changeset
  1041
* Command-line tool "isabelle build" takes "condition" options with the
be08a7691c62 clarified meta_digest;
wenzelm
parents: 66841
diff changeset
  1042
corresponding environment values into account, when determining the
be08a7691c62 clarified meta_digest;
wenzelm
parents: 66841
diff changeset
  1043
up-to-date status of a session.
be08a7691c62 clarified meta_digest;
wenzelm
parents: 66841
diff changeset
  1044
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1045
* The command-line tool "dump" dumps information from the cumulative
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1046
PIDE session database: many sessions may be loaded into a given logic
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1047
image, results from all loaded theories are written to the output
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1048
directory.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1049
66851
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66844
diff changeset
  1050
* Command-line tool "isabelle imports -I" also reports actual session
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66844
diff changeset
  1051
imports. This helps to minimize the session dependency graph.
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66844
diff changeset
  1052
70142
eff4ff8ba515 NEWS for proper Isabelle version;
wenzelm
parents: 70108
diff changeset
  1053
* The command-line tool "export" and 'export_files' in session ROOT
eff4ff8ba515 NEWS for proper Isabelle version;
wenzelm
parents: 70108
diff changeset
  1054
entries retrieve theory exports from the session build database.
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1055
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1056
* The command-line tools "isabelle server" and "isabelle client" provide
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1057
access to the Isabelle Server: it supports responsive session management
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1058
and concurrent use of theories, based on Isabelle/PIDE infrastructure.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1059
See also the "system" manual.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1060
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1061
* The command-line tool "isabelle update_comments" normalizes formal
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1062
comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1063
approximate the appearance in document output). This is more specific
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1064
than former "isabelle update_cartouches -c": the latter tool option has
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1065
been discontinued.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1066
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1067
* The command-line tool "isabelle mkroot" now always produces a document
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1068
outline: its options have been adapted accordingly. INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1069
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1070
* The command-line tool "isabelle mkroot -I" initializes a Mercurial
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1071
repository for the generated session files.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1072
68523
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
  1073
* Settings ISABELLE_HEAPS + ISABELLE_BROWSER_INFO (or
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
  1074
ISABELLE_HEAPS_SYSTEM + ISABELLE_BROWSER_INFO_SYSTEM in "system build
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
  1075
mode") determine the directory locations of the main build artefacts --
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
  1076
instead of hard-wired directories in ISABELLE_HOME_USER (or
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
  1077
ISABELLE_HOME).
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
  1078
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1079
* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1080
heap images and session databases are always stored in
68523
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
  1081
$ISABELLE_HEAPS/$ML_IDENTIFIER (command-line default) or
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
  1082
$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER (main Isabelle application or
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1083
"isabelle jedit -s" or "isabelle build -s").
67099
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 67088
diff changeset
  1084
67199
wenzelm
parents: 67194
diff changeset
  1085
* ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific
wenzelm
parents: 67194
diff changeset
  1086
options for improved error reporting. Potential INCOMPATIBILITY with
wenzelm
parents: 67194
diff changeset
  1087
unusual LaTeX installations, may have to adapt these settings.
wenzelm
parents: 67194
diff changeset
  1088
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1089
* Update to Poly/ML 5.7.1 with slightly improved performance and PIDE
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1090
markup for identifier bindings. It now uses The GNU Multiple Precision
67591
wenzelm
parents: 67525
diff changeset
  1091
Arithmetic Library (libgmp) on all platforms, notably Mac OS X with
wenzelm
parents: 67525
diff changeset
  1092
32/64 bit.
wenzelm
parents: 67525
diff changeset
  1093
67099
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 67088
diff changeset
  1094
66729
wenzelm
parents: 66712
diff changeset
  1095
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1096
New in Isabelle2017 (October 2017)
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1097
----------------------------------
64439
2bafda87b524 back to post-release mode -- after fork point;
wenzelm
parents: 64391
diff changeset
  1098
64986
b81a048960a3 more uniform use of Reconstruct.clean_proof_of;
wenzelm
parents: 64917
diff changeset
  1099
*** General ***
b81a048960a3 more uniform use of Reconstruct.clean_proof_of;
wenzelm
parents: 64917
diff changeset
  1100
66238
wenzelm
parents: 66181
diff changeset
  1101
* Experimental support for Visual Studio Code (VSCode) as alternative
wenzelm
parents: 66181
diff changeset
  1102
Isabelle/PIDE front-end, see also
66601
34b20f7236ea proper URL;
wenzelm
parents: 66576
diff changeset
  1103
https://marketplace.visualstudio.com/items?itemName=makarius.Isabelle2017
66238
wenzelm
parents: 66181
diff changeset
  1104
wenzelm
parents: 66181
diff changeset
  1105
VSCode is a new type of application that continues the concepts of
wenzelm
parents: 66181
diff changeset
  1106
"programmer's editor" and "integrated development environment" towards
wenzelm
parents: 66181
diff changeset
  1107
fully semantic editing and debugging -- in a relatively light-weight
wenzelm
parents: 66181
diff changeset
  1108
manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure.
wenzelm
parents: 66181
diff changeset
  1109
Technically, VSCode is based on the Electron application framework
wenzelm
parents: 66181
diff changeset
  1110
(Node.js + Chromium browser + V8), which is implemented in JavaScript
wenzelm
parents: 66181
diff changeset
  1111
and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala
wenzelm
parents: 66181
diff changeset
  1112
modules around a Language Server implementation.
wenzelm
parents: 66181
diff changeset
  1113
65504
b80477da30eb some documentation;
wenzelm
parents: 65465
diff changeset
  1114
* Theory names are qualified by the session name that they belong to.
66454
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
  1115
This affects imports, but not the theory name space prefix (which is
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
  1116
just the theory base name as before).
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
  1117
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
  1118
In order to import theories from other sessions, the ROOT file format
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
  1119
provides a new 'sessions' keyword. In contrast, a theory that is
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
  1120
imported in the old-fashioned manner via an explicit file-system path
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1121
belongs to the current session, and might cause theory name conflicts
66454
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
  1122
later on. Theories that are imported from other sessions are excluded
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
  1123
from the current session document. The command-line tool "isabelle
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
  1124
imports" helps to update theory imports.
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
  1125
65451
wenzelm
parents: 65448
diff changeset
  1126
* The main theory entry points for some non-HOL sessions have changed,
wenzelm
parents: 65448
diff changeset
  1127
to avoid confusion with the global name "Main" of the session HOL. This
wenzelm
parents: 65448
diff changeset
  1128
leads to the follow renamings:
wenzelm
parents: 65448
diff changeset
  1129
wenzelm
parents: 65448
diff changeset
  1130
  CTT/Main.thy    ~>  CTT/CTT.thy
wenzelm
parents: 65448
diff changeset
  1131
  ZF/Main.thy     ~>  ZF/ZF.thy
wenzelm
parents: 65448
diff changeset
  1132
  ZF/Main_ZF.thy  ~>  ZF/ZF.thy
wenzelm
parents: 65448
diff changeset
  1133
  ZF/Main_ZFC.thy ~>  ZF/ZFC.thy
wenzelm
parents: 65448
diff changeset
  1134
  ZF/ZF.thy       ~>  ZF/ZF_Base.thy
wenzelm
parents: 65448
diff changeset
  1135
wenzelm
parents: 65448
diff changeset
  1136
INCOMPATIBILITY.
wenzelm
parents: 65448
diff changeset
  1137
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1138
* Commands 'alias' and 'type_alias' introduce aliases for constants and
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1139
type constructors, respectively. This allows adhoc changes to name-space
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1140
accesses within global or local theory contexts, e.g. within a 'bundle'.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1141
64986
b81a048960a3 more uniform use of Reconstruct.clean_proof_of;
wenzelm
parents: 64917
diff changeset
  1142
* Document antiquotations @{prf} and @{full_prf} output proof terms
b81a048960a3 more uniform use of Reconstruct.clean_proof_of;
wenzelm
parents: 64917
diff changeset
  1143
(again) in the same way as commands 'prf' and 'full_prf'.
b81a048960a3 more uniform use of Reconstruct.clean_proof_of;
wenzelm
parents: 64917
diff changeset
  1144
65055
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
  1145
* Computations generated by the code generator can be embedded directly
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
  1146
into ML, alongside with @{code} antiquotations, using the following
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
  1147
antiquotations:
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
  1148
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
  1149
  @{computation ... terms: ... datatypes: ...} :
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
  1150
    ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
  1151
  @{computation_conv ... terms: ... datatypes: ...} :
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
  1152
    (Proof.context -> 'ml -> conv) -> Proof.context -> conv
65045
b69ef432438d avoid Unicode that conflicts with Isabelle symbol rendering;
wenzelm
parents: 65042
diff changeset
  1153
  @{computation_check terms: ... datatypes: ...} : Proof.context -> conv
65041
2525e680f94f basic documentation for computations
haftmann
parents: 65027
diff changeset
  1154
65055
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
  1155
See src/HOL/ex/Computations.thy,
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
  1156
src/HOL/Decision_Procs/Commutative_Ring.thy and
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
  1157
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
  1158
tutorial on code generation.
65041
2525e680f94f basic documentation for computations
haftmann
parents: 65027
diff changeset
  1159
64986
b81a048960a3 more uniform use of Reconstruct.clean_proof_of;
wenzelm
parents: 64917
diff changeset
  1160
64602
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 64593
diff changeset
  1161
*** Prover IDE -- Isabelle/Scala/jEdit ***
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 64593
diff changeset
  1162
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1163
* Session-qualified theory imports allow the Prover IDE to process
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1164
arbitrary theory hierarchies independently of the underlying logic
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1165
session image (e.g. option "isabelle jedit -l"), but the directory
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1166
structure needs to be known in advance (e.g. option "isabelle jedit -d"
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1167
or a line in the file $ISABELLE_HOME_USER/ROOTS).
64602
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 64593
diff changeset
  1168
64842
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
  1169
* The PIDE document model maintains file content independently of the
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
  1170
status of jEdit editor buffers. Reloading jEdit buffers no longer causes
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
  1171
changes of formal document content. Theory dependencies are always
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
  1172
resolved internally, without the need for corresponding editor buffers.
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
  1173
The system option "jedit_auto_load" has been discontinued: it is
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
  1174
effectively always enabled.
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
  1175
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64846
diff changeset
  1176
* The Theories dockable provides a "Purge" button, in order to restrict
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64846
diff changeset
  1177
the document model to theories that are required for open editor
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64846
diff changeset
  1178
buffers.
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64846
diff changeset
  1179
66426
wenzelm
parents: 66348
diff changeset
  1180
* The Theories dockable indicates the overall status of checking of each
wenzelm
parents: 66348
diff changeset
  1181
entry. When all forked tasks of a theory are finished, the border is
wenzelm
parents: 66348
diff changeset
  1182
painted with thick lines; remaining errors in this situation are
wenzelm
parents: 66348
diff changeset
  1183
represented by a different border color.
wenzelm
parents: 66348
diff changeset
  1184
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1185
* Automatic indentation is more careful to avoid redundant spaces in
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1186
intermediate situations. Keywords are indented after input (via typed
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1187
characters or completion); see also option "jedit_indent_input".
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1188
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1189
* Action "isabelle.preview" opens an HTML preview of the current theory
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1190
document in the default web browser.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1191
66576
e16b27bd3f76 reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
wenzelm
parents: 66555
diff changeset
  1192
* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
e16b27bd3f76 reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
wenzelm
parents: 66555
diff changeset
  1193
entry of the specified logic session in the editor, while its parent is
e16b27bd3f76 reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
wenzelm
parents: 66555
diff changeset
  1194
used for formal checking.
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1195
66463
0a8277e9cfd6 officially allow restart of Isabelle plugin;
wenzelm
parents: 66455
diff changeset
  1196
* The main Isabelle/jEdit plugin may be restarted manually (using the
0a8277e9cfd6 officially allow restart of Isabelle plugin;
wenzelm
parents: 66455
diff changeset
  1197
jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
0a8277e9cfd6 officially allow restart of Isabelle plugin;
wenzelm
parents: 66455
diff changeset
  1198
enabled at all times.
0a8277e9cfd6 officially allow restart of Isabelle plugin;
wenzelm
parents: 66455
diff changeset
  1199
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1200
* Update to current jedit-5.4.0.
65329
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 65170
diff changeset
  1201
64602
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 64593
diff changeset
  1202
66149
4bf16fb7c14d deleting a code equation never leads to unimplemented function
haftmann
parents: 66135
diff changeset
  1203
*** Pure ***
4bf16fb7c14d deleting a code equation never leads to unimplemented function
haftmann
parents: 66135
diff changeset
  1204
4bf16fb7c14d deleting a code equation never leads to unimplemented function
haftmann
parents: 66135
diff changeset
  1205
* Deleting the last code equations for a particular function using
4bf16fb7c14d deleting a code equation never leads to unimplemented function
haftmann
parents: 66135
diff changeset
  1206
[code del] results in function with no equations (runtime abort) rather
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1207
than an unimplemented function (generation time abort). Use explicit
66667
ec78c84bfc44 spelling
haftmann
parents: 66652
diff changeset
  1208
[[code drop:]] to enforce the latter. Minor INCOMPATIBILITY.
66149
4bf16fb7c14d deleting a code equation never leads to unimplemented function
haftmann
parents: 66135
diff changeset
  1209
66313
e8d2862ec203 simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents: 66298
diff changeset
  1210
* Proper concept of code declarations in code.ML:
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1211
  - Regular code declarations act only on the global theory level, being
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1212
    ignored with warnings if syntactically malformed.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1213
  - Explicitly global code declarations yield errors if syntactically
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1214
    malformed.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1215
  - Default code declarations are silently ignored if syntactically
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1216
    malformed.
66313
e8d2862ec203 simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents: 66298
diff changeset
  1217
Minor INCOMPATIBILITY.
e8d2862ec203 simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents: 66298
diff changeset
  1218
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1219
* Clarified and standardized internal data bookkeeping of code
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1220
declarations: history of serials allows to track potentially
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1221
non-monotonous declarations appropriately. Minor INCOMPATIBILITY.
66313
e8d2862ec203 simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents: 66298
diff changeset
  1222
66149
4bf16fb7c14d deleting a code equation never leads to unimplemented function
haftmann
parents: 66135
diff changeset
  1223
64593
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
  1224
*** HOL ***
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
  1225
66616
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents: 66601
diff changeset
  1226
* The Nunchaku model finder is now part of "Main".
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents: 66601
diff changeset
  1227
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1228
* SMT module:
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1229
  - A new option, 'smt_nat_as_int', has been added to translate 'nat' to
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1230
    'int' and benefit from the SMT solver's theory reasoning. It is
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1231
    disabled by default.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1232
  - The legacy module "src/HOL/Library/Old_SMT.thy" has been removed.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1233
  - Several small issues have been rectified in the 'smt' command.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1234
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1235
* (Co)datatype package: The 'size_gen_o_map' lemma is no longer
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1236
generated for datatypes with type class annotations. As a result, the
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1237
tactic that derives it no longer fails on nested datatypes. Slight
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1238
INCOMPATIBILITY.
66450
a8299195ed82 NEWS: Removed constant subseq; subsumed by strict_mono
eberlm <eberlm@in.tum.de>
parents: 66449
diff changeset
  1239
66348
882abe912da9 do not fall back on nbe if plain evaluation fails
haftmann
parents: 66313
diff changeset
  1240
* Command and antiquotation "value" with modified default strategy:
882abe912da9 do not fall back on nbe if plain evaluation fails
haftmann
parents: 66313
diff changeset
  1241
terms without free variables are always evaluated using plain evaluation
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1242
only, with no fallback on normalization by evaluation. Minor
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1243
INCOMPATIBILITY.
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 65841
diff changeset
  1244
65552
f533820e7248 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents: 65544
diff changeset
  1245
* Theories "GCD" and "Binomial" are already included in "Main" (instead
65575
wenzelm
parents: 65572
diff changeset
  1246
of "Complex_Main").
65552
f533820e7248 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents: 65544
diff changeset
  1247
65170
53675f36820d restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents: 65099
diff changeset
  1248
* Constant "surj" is a full input/output abbreviation (again).
53675f36820d restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents: 65099
diff changeset
  1249
Minor INCOMPATIBILITY.
53675f36820d restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents: 65099
diff changeset
  1250
64632
9df24b8b6c0a dropped aliasses
haftmann
parents: 64603
diff changeset
  1251
* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
9df24b8b6c0a dropped aliasses
haftmann
parents: 64603
diff changeset
  1252
INCOMPATIBILITY.
9df24b8b6c0a dropped aliasses
haftmann
parents: 64603
diff changeset
  1253
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1254
* Renamed ii to imaginary_unit in order to free up ii as a variable
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1255
name. The syntax \<i> remains available. INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1256
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1257
* Dropped abbreviations transP, antisymP, single_valuedP; use constants
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1258
transp, antisymp, single_valuedp instead. INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1259
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1260
* Constant "subseq" in Topological_Spaces has been removed -- it is
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1261
subsumed by "strict_mono". Some basic lemmas specific to "subseq" have
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1262
been renamed accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1263
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1264
* Theory List: "sublist" renamed to "nths" in analogy with "nth", and
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1265
"sublisteq" renamed to "subseq". Minor INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1266
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1267
* Theory List: new generic function "sorted_wrt".
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1268
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1269
* Named theorems mod_simps covers various congruence rules concerning
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1270
mod, replacing former zmod_simps. INCOMPATIBILITY.
64787
067cacdd1117 tuned NEWS
haftmann
parents: 64786
diff changeset
  1271
64593
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
  1272
* Swapped orientation of congruence rules mod_add_left_eq,
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
  1273
mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
  1274
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1275
mod_diff_eq. INCOMPATIBILITY.
64593
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
  1276
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
  1277
* Generalized some facts:
64876
65a247444100 generalized types in lemmas
blanchet
parents: 64867
diff changeset
  1278
    measure_induct_rule
65a247444100 generalized types in lemmas
blanchet
parents: 64867
diff changeset
  1279
    measure_induct
64593
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
  1280
    zminus_zmod ~> mod_minus_eq
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
  1281
    zdiff_zmod_left ~> mod_diff_left_eq
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
  1282
    zdiff_zmod_right ~> mod_diff_right_eq
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
  1283
    zmod_eq_dvd_iff ~> mod_eq_dvd_iff
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
  1284
INCOMPATIBILITY.
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
  1285
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1286
* Algebraic type class hierarchy of euclidean (semi)rings in HOL:
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1287
euclidean_(semi)ring, euclidean_(semi)ring_cancel,
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1288
unique_euclidean_(semi)ring; instantiation requires provision of a
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1289
euclidean size.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1290
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1291
* Theory "HOL-Number_Theory.Euclidean_Algorithm" has been reworked:
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1292
  - Euclidean induction is available as rule eucl_induct.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1293
  - Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1294
    Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1295
    easy instantiation of euclidean (semi)rings as GCD (semi)rings.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1296
  - Coefficients obtained by extended euclidean algorithm are
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1297
    available as "bezout_coefficients".
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1298
INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1299
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1300
* Theory "Number_Theory.Totient" introduces basic notions about Euler's
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1301
totient function previously hidden as solitary example in theory
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1302
Residues. Definition changed so that "totient 1 = 1" in agreement with
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1303
the literature. Minor INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1304
66542
075bbb78d33c proper theory name;
wenzelm
parents: 66541
diff changeset
  1305
* New styles in theory "HOL-Library.LaTeXsugar":
66541
nipkow
parents: 66487
diff changeset
  1306
  - "dummy_pats" for printing equations with "_" on the lhs;
nipkow
parents: 66487
diff changeset
  1307
  - "eta_expand" for printing eta-expanded terms.
nipkow
parents: 66487
diff changeset
  1308
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1309
* Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1310
been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1311
66645
f7e38b8583a0 Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents: 66643
diff changeset
  1312
* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F"
66487
9d83e8fe3de3 HOL-Library: going_to filter
Manuel Eberl <eberlm@in.tum.de>
parents: 66481
diff changeset
  1313
filter for describing points x such that f(x) is in the filter F.
9d83e8fe3de3 HOL-Library: going_to filter
Manuel Eberl <eberlm@in.tum.de>
parents: 66481
diff changeset
  1314
66480
4b8d1df8933b HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents: 66474
diff changeset
  1315
* Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been
4b8d1df8933b HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents: 66474
diff changeset
  1316
renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1317
space. INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1318
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1319
* Theory "HOL-Library.FinFun" has been moved to AFP (again).
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1320
INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1321
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1322
* Theory "HOL-Library.FuncSet": some old and rarely used ASCII
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1323
replacement syntax has been removed. INCOMPATIBILITY, standard syntax
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1324
with symbols should be used instead. The subsequent commands help to
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1325
reproduce the old forms, e.g. to simplify porting old theories:
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1326
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1327
syntax (ASCII)
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1328
  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1329
  "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1330
  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1331
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1332
* Theory "HOL-Library.Multiset": the simprocs on subsets operators of
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1333
multisets have been renamed:
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1334
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1335
  msetless_cancel_numerals ~> msetsubset_cancel
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1336
  msetle_cancel_numerals ~> msetsubset_eq_cancel
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1337
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1338
INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1339
66481
d35f7a9f92e2 output syntax for pattern aliases
Lars Hupel <lars.hupel@mytum.de>
parents: 66480
diff changeset
  1340
* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax
d35f7a9f92e2 output syntax for pattern aliases
Lars Hupel <lars.hupel@mytum.de>
parents: 66480
diff changeset
  1341
for pattern aliases as known from Haskell, Scala and ML.
65515
f595b7532dc9 removed Old_SMT legacy module
blanchet
parents: 65511
diff changeset
  1342
66555
87b9eb69d5ba add type of unordered pairs
Andreas Lochbihler
parents: 66542
diff changeset
  1343
* Theory "HOL-Library.Uprod" formalizes the type of unordered pairs.
87b9eb69d5ba add type of unordered pairs
Andreas Lochbihler
parents: 66542
diff changeset
  1344
64898
49aa13b1b592 tuned whitespace;
wenzelm
parents: 64876
diff changeset
  1345
* Session HOL-Analysis: more material involving arcs, paths, covering
66652
wenzelm
parents: 66645
diff changeset
  1346
spaces, innessential maps, retracts, infinite products, simplicial
wenzelm
parents: 66645
diff changeset
  1347
complexes. Baire Category theorem. Major results include the Jordan
wenzelm
parents: 66645
diff changeset
  1348
Curve Theorem and the Great Picard Theorem.
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1349
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1350
* Session HOL-Algebra has been extended by additional lattice theory:
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1351
the Knaster-Tarski fixed point theorem and Galois Connections.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1352
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1353
* Sessions HOL-Computational_Algebra and HOL-Number_Theory: new notions
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1354
of squarefreeness, n-th powers, and prime powers.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1355
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1356
* Session "HOL-Computional_Algebra" covers many previously scattered
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1357
theories, notably Euclidean_Algorithm, Factorial_Ring,
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1358
Formal_Power_Series, Fraction_Field, Fundamental_Theorem_Algebra,
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1359
Normalized_Fraction, Polynomial_FPS, Polynomial, Primes. Minor
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1360
INCOMPATIBILITY.
65027
2b8583507891 renaming multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64986
diff changeset
  1361
60331
f215fd466e30 discontinued legacy;
wenzelm
parents: 60310
diff changeset
  1362
64844
bb70dc05cd38 NEWS for VSCode;
wenzelm
parents: 64842
diff changeset
  1363
*** System ***
bb70dc05cd38 NEWS for VSCode;
wenzelm
parents: 64842
diff changeset
  1364
66474
wenzelm
parents: 66473
diff changeset
  1365
* Isabelle/Scala: the SQL module supports access to relational
wenzelm
parents: 66473
diff changeset
  1366
databases, either as plain file (SQLite) or full-scale server
wenzelm
parents: 66473
diff changeset
  1367
(PostgreSQL via local port or remote ssh connection).
wenzelm
parents: 66473
diff changeset
  1368
wenzelm
parents: 66473
diff changeset
  1369
* Results of "isabelle build" are recorded as SQLite database (i.e.
wenzelm
parents: 66473
diff changeset
  1370
"Application File Format" in the sense of
wenzelm
parents: 66473
diff changeset
  1371
https://www.sqlite.org/appfileformat.html). This allows systematic
wenzelm
parents: 66473
diff changeset
  1372
access via operations from module Sessions.Store in Isabelle/Scala.
wenzelm
parents: 66473
diff changeset
  1373
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1374
* System option "parallel_proofs" is 1 by default (instead of more
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1375
aggressive 2). This requires less heap space and avoids burning parallel
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1376
CPU cycles, while full subproof parallelization is enabled for repeated
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1377
builds (according to parallel_subproofs_threshold).
65072
36c650d1a90d more detailed platform information;
wenzelm
parents: 65064
diff changeset
  1378
65448
9bc3b57c1fa7 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents: 65417
diff changeset
  1379
* System option "record_proofs" allows to change the global
9bc3b57c1fa7 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents: 65417
diff changeset
  1380
Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;
9bc3b57c1fa7 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents: 65417
diff changeset
  1381
a negative value means the current state in the ML heap image remains
9bc3b57c1fa7 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents: 65417
diff changeset
  1382
unchanged.
9bc3b57c1fa7 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents: 65417
diff changeset
  1383
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1384
* Isabelle settings variable ISABELLE_SCALA_BUILD_OPTIONS has been
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66463
diff changeset
  1385
renamed to ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY.