NEWS
author wenzelm
Fri, 24 Sep 2021 13:40:14 +0200
changeset 74360 9e71155e3666
parent 74349 4974c3697fee
permissions -rw-r--r--
grant access to sun.tools.jconsole, as required for Java 17;
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.)
60006
wenzelm
parents: 59998
diff changeset
     5
73272
haftmann
parents: 73270
diff changeset
     6
haftmann
parents: 73270
diff changeset
     7
New in this Isabelle version
haftmann
parents: 73270
diff changeset
     8
----------------------------
haftmann
parents: 73270
diff changeset
     9
73387
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73378
diff changeset
    10
*** General ***
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73378
diff changeset
    11
74335
wenzelm
parents: 74317
diff changeset
    12
* Commands 'syntax' and 'no_syntax' now work in a local theory context,
wenzelm
parents: 74317
diff changeset
    13
but there is no proper way to refer to local entities --- in contrast to
wenzelm
parents: 74317
diff changeset
    14
'notation' and 'no_notation'. Local syntax works well with 'bundle',
wenzelm
parents: 74317
diff changeset
    15
e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory Main of
wenzelm
parents: 74317
diff changeset
    16
Isabelle/HOL.
wenzelm
parents: 74317
diff changeset
    17
74156
ecf80e37ed1a support configuration options "show_results";
wenzelm
parents: 74123
diff changeset
    18
* Configuration option "show_results" controls output of final results
ecf80e37ed1a support configuration options "show_results";
wenzelm
parents: 74123
diff changeset
    19
in commands like 'definition' or 'theorem'. Output is normally enabled
ecf80e37ed1a support configuration options "show_results";
wenzelm
parents: 74123
diff changeset
    20
in interactive mode, but it could occasionally cause unnecessary
ecf80e37ed1a support configuration options "show_results";
wenzelm
parents: 74123
diff changeset
    21
slowdown. It can be disabled like this:
ecf80e37ed1a support configuration options "show_results";
wenzelm
parents: 74123
diff changeset
    22
74349
4974c3697fee proper NEWS;
wenzelm
parents: 74348
diff changeset
    23
  context notes [[show_results = false]]
74156
ecf80e37ed1a support configuration options "show_results";
wenzelm
parents: 74123
diff changeset
    24
  begin
ecf80e37ed1a support configuration options "show_results";
wenzelm
parents: 74123
diff changeset
    25
    definition "test = True"
ecf80e37ed1a support configuration options "show_results";
wenzelm
parents: 74123
diff changeset
    26
    theorem test by (simp add: test_def)
ecf80e37ed1a support configuration options "show_results";
wenzelm
parents: 74123
diff changeset
    27
  end
ecf80e37ed1a support configuration options "show_results";
wenzelm
parents: 74123
diff changeset
    28
73387
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73378
diff changeset
    29
* Timeouts for Isabelle/ML tools are subject to system option
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73378
diff changeset
    30
"timeout_scale" --- this already used for the overall session build
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73378
diff changeset
    31
process before, and allows to adapt to slow machines. The underlying
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73378
diff changeset
    32
Timeout.apply in Isabelle/ML treats an original timeout specification 0
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73378
diff changeset
    33
as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73378
diff changeset
    34
in boundary cases.
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73378
diff changeset
    35
73436
e92f2e44e4d8 removed spurious references to perl / libwww-perl;
wenzelm
parents: 73411
diff changeset
    36
* Remote provers from SystemOnTPTP (notably for Sledgehammer) are now
e92f2e44e4d8 removed spurious references to perl / libwww-perl;
wenzelm
parents: 73411
diff changeset
    37
managed via Isabelle/Scala instead of perl; the dependency on
e92f2e44e4d8 removed spurious references to perl / libwww-perl;
wenzelm
parents: 73411
diff changeset
    38
libwww-perl has been eliminated (notably on Linux). Rare
e92f2e44e4d8 removed spurious references to perl / libwww-perl;
wenzelm
parents: 73411
diff changeset
    39
INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties
e92f2e44e4d8 removed spurious references to perl / libwww-perl;
wenzelm
parents: 73411
diff changeset
    40
https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html
e92f2e44e4d8 removed spurious references to perl / libwww-perl;
wenzelm
parents: 73411
diff changeset
    41
73446
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 73436
diff changeset
    42
* More symbol definitions for the Z Notation (Isabelle fonts and LaTeX).
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 73436
diff changeset
    43
See also the group "Z Notation" in the Symbols dockable of
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 73436
diff changeset
    44
Isabelle/jEdit.
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 73436
diff changeset
    45
73387
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73378
diff changeset
    46
73616
b0ea03e837b1 support nested cases;
wenzelm
parents: 73595
diff changeset
    47
*** Isabelle/jEdit Prover IDE ***
b0ea03e837b1 support nested cases;
wenzelm
parents: 73595
diff changeset
    48
b0ea03e837b1 support nested cases;
wenzelm
parents: 73595
diff changeset
    49
* More robust 'proof' outline for method "induct": support nested cases.
b0ea03e837b1 support nested cases;
wenzelm
parents: 73595
diff changeset
    50
73876
e6c9c1c3f580 support for jEdit font substitution;
wenzelm
parents: 73869
diff changeset
    51
* Support for built-in font substitution of jEdit text area.
e6c9c1c3f580 support for jEdit font substitution;
wenzelm
parents: 73869
diff changeset
    52
74003
wenzelm
parents: 73935
diff changeset
    53
* The main plugin for Isabelle/jEdit can be deactivated and reactivated
wenzelm
parents: 73935
diff changeset
    54
as documented --- was broken at least since Isabelle2018.
wenzelm
parents: 73935
diff changeset
    55
73616
b0ea03e837b1 support nested cases;
wenzelm
parents: 73595
diff changeset
    56
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 73394
diff changeset
    57
*** Document preparation ***
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 73394
diff changeset
    58
73830
wenzelm
parents: 73829
diff changeset
    59
* More predefined symbols: \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (LaTeX package
73828
201200b549fc proper NEWS after Isabelle2021;
wenzelm
parents: 73826
diff changeset
    60
"pifont").
201200b549fc proper NEWS after Isabelle2021;
wenzelm
parents: 73826
diff changeset
    61
73830
wenzelm
parents: 73829
diff changeset
    62
* High-quality blackboard-bold symbols from font "txmia" (LaTeX package
73828
201200b549fc proper NEWS after Isabelle2021;
wenzelm
parents: 73826
diff changeset
    63
"pxfonts"): \<bbbA>\<bool>\<complex>\<bbbD>\<bbbE>\<bbbF>\<bbbG>\<bbbH>\<bbbI>\<bbbJ>\<bbbK>\<bbbL>\<bbbM>\<nat>\<bbbO>\<bbbP>\<rat>\<real>\<bbbS>\<bbbT>\<bbbU>\<bbbV>\<bbbW>\<bbbX>\<bbbY>\<int>.
201200b549fc proper NEWS after Isabelle2021;
wenzelm
parents: 73826
diff changeset
    64
73771
wenzelm
parents: 73743
diff changeset
    65
* Document antiquotations for ML text have been refined: "def" and "ref"
wenzelm
parents: 73743
diff changeset
    66
variants support index entries, e.g. @{ML} (no entry) vs. @{ML_def}
wenzelm
parents: 73743
diff changeset
    67
(bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit
wenzelm
parents: 73743
diff changeset
    68
type arguments for constructors (only relevant for index), e.g.
wenzelm
parents: 73743
diff changeset
    69
@{ML_type \<open>'a list\<close>} vs. @{ML_type 'a \<open>list\<close>}; @{ML_op} has been renamed
wenzelm
parents: 73743
diff changeset
    70
to @{ML_infix}. Minor INCOMPATIBILITY concerning name and syntax.
wenzelm
parents: 73743
diff changeset
    71
73723
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73721
diff changeset
    72
* Option "document_logo" determines if an instance of the Isabelle logo
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73721
diff changeset
    73
should be created in the document output directory. The given string
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73721
diff changeset
    74
specifies the name of the logo variant, while "_" (underscore) refers to
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73721
diff changeset
    75
the unnamed variant. The output file name is always "isabelle_logo.pdf".
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73721
diff changeset
    76
73741
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
    77
* Option "document_preprocessor" specifies the name of an executable
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
    78
that is run within the document output directory, after preparing the
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
    79
document sources and before the actual build process. This allows to
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
    80
apply adhoc patches, without requiring a separate "build" script.
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
    81
73721
52030acb19ac option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents: 73682
diff changeset
    82
* Option "document_build" determines the document build engine, as
52030acb19ac option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents: 73682
diff changeset
    83
defined in Isabelle/Scala (as system service). The subsequent engines
52030acb19ac option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents: 73682
diff changeset
    84
are provided by the Isabelle distribution:
52030acb19ac option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents: 73682
diff changeset
    85
73741
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
    86
  - "lualatex" (default): use ISABELLE_LUALATEX for a standard LaTeX
73721
52030acb19ac option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents: 73682
diff changeset
    87
    build with optional ISABELLE_BIBTEX and ISABELLE_MAKEINDEX
52030acb19ac option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents: 73682
diff changeset
    88
73741
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
    89
  - "pdflatex": as above, but use ISABELLE_PDFLATEX (legacy mode for
73721
52030acb19ac option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents: 73682
diff changeset
    90
    special LaTeX styles)
52030acb19ac option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents: 73682
diff changeset
    91
73741
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
    92
  - "build": delegate to the executable "./build pdf"
73721
52030acb19ac option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents: 73682
diff changeset
    93
52030acb19ac option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents: 73682
diff changeset
    94
The presence of a "build" command within the document output directory
52030acb19ac option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents: 73682
diff changeset
    95
explicitly requires document_build=build. Minor INCOMPATIBILITY, need to
52030acb19ac option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents: 73682
diff changeset
    96
adjust session ROOT options.
52030acb19ac option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents: 73682
diff changeset
    97
73741
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
    98
* The command-line tool "isabelle latex" has been discontinued,
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
    99
INCOMPATIBILITY for old document build scripts.
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   100
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   101
  - Former "isabelle latex -o sty" has become obsolete: Isabelle .sty
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   102
    files are automatically generated within the document output
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   103
    directory.
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   104
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   105
  - Former "isabelle latex -o pdf" should be replaced by
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   106
    "$ISABELLE_LUALATEX root" or "$ISABELLE_PDFLATEX root" (without
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   107
    quotes), according to the intended LaTeX engine.
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   108
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   109
  - Former "isabelle latex -o bbl" should be replaced by
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   110
    "$ISABELLE_BIBTEX root" (without quotes).
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   111
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   112
  - Former "isabelle latex -o idx" should be replaced by
941915a3b811 discontinued obsolete "isabelle latex";
wenzelm
parents: 73737
diff changeset
   113
    "$ISABELLE_MAKEINDEX root" (without quotes).
73724
5a3a2a52648d clarified treatment of Isabelle .sty files;
wenzelm
parents: 73723
diff changeset
   114
73743
813a08dff3fd explicit option document_bibliography;
wenzelm
parents: 73741
diff changeset
   115
* Option "document_bibliography" explicitly enables the use of bibtex;
813a08dff3fd explicit option document_bibliography;
wenzelm
parents: 73741
diff changeset
   116
the default is to check the presence of root.bib, but it could have a
813a08dff3fd explicit option document_bibliography;
wenzelm
parents: 73741
diff changeset
   117
different name.
813a08dff3fd explicit option document_bibliography;
wenzelm
parents: 73741
diff changeset
   118
73409
wenzelm
parents: 73404
diff changeset
   119
* Improved LaTeX typesetting of \<open>...\<close> using \guilsinglleft ...
wenzelm
parents: 73404
diff changeset
   120
\guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 73394
diff changeset
   121
(which is now also the default in "isabelle mkroot").
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 73394
diff changeset
   122
73595
aece5cc9efb7 simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm
parents: 73586
diff changeset
   123
* Simplified typesetting of \<guillemotleft>...\<guillemotright> using \guillemotleft ...
aece5cc9efb7 simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm
parents: 73586
diff changeset
   124
\guillemotright from \usepackage[T1]{fontenc} --- \usepackage{babel} is
aece5cc9efb7 simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm
parents: 73586
diff changeset
   125
no longer required.
aece5cc9efb7 simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm
parents: 73586
diff changeset
   126
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 73394
diff changeset
   127
73846
9447668d1b77 global interpretation into nested targets
haftmann
parents: 73842
diff changeset
   128
*** Pure ***
9447668d1b77 global interpretation into nested targets
haftmann
parents: 73842
diff changeset
   129
9447668d1b77 global interpretation into nested targets
haftmann
parents: 73842
diff changeset
   130
* "global_interpretation" is applicable in instantiation and overloading
9447668d1b77 global interpretation into nested targets
haftmann
parents: 73842
diff changeset
   131
targets and in any nested target built on top of a target supporting
9447668d1b77 global interpretation into nested targets
haftmann
parents: 73842
diff changeset
   132
"global_interpretation".
9447668d1b77 global interpretation into nested targets
haftmann
parents: 73842
diff changeset
   133
9447668d1b77 global interpretation into nested targets
haftmann
parents: 73842
diff changeset
   134
73270
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73253
diff changeset
   135
*** HOL ***
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73253
diff changeset
   136
74335
wenzelm
parents: 74317
diff changeset
   137
* Theory HOL-Library.Lattice_Syntax has been superseded by bundle
wenzelm
parents: 74317
diff changeset
   138
"lattice_syntax": it can be used in a local context via 'include' or in
wenzelm
parents: 74317
diff changeset
   139
a global theory via 'unbundle'. The opposite declarations are bundled as
74348
cdf8952a86d5 tuned NEWS;
wenzelm
parents: 74341
diff changeset
   140
"no_lattice_syntax". Minor INCOMPATIBILITY.
74335
wenzelm
parents: 74317
diff changeset
   141
73829
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   142
* Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   143
use explict expression instead. Minor INCOMPATIBILITY.
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   144
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   145
* Theory "HOL-Library.Multiset": consolidated abbreviations Mempty,
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   146
Melem, not_Melem to empty_mset, member_mset, not_member_mset
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   147
respectively. Minor INCOMPATIBILITY.
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   148
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   149
* Theory "HOL-Library.Multiset": consolidated operation and fact names:
73393
716d256259d5 consolidated names
haftmann
parents: 73387
diff changeset
   150
    inf_subset_mset ~> inter_mset
716d256259d5 consolidated names
haftmann
parents: 73387
diff changeset
   151
    sup_subset_mset ~> union_mset
716d256259d5 consolidated names
haftmann
parents: 73387
diff changeset
   152
    multiset_inter_def ~> inter_mset_def
716d256259d5 consolidated names
haftmann
parents: 73387
diff changeset
   153
    sup_subset_mset_def ~> union_mset_def
716d256259d5 consolidated names
haftmann
parents: 73387
diff changeset
   154
    multiset_inter_count ~> count_inter_mset
716d256259d5 consolidated names
haftmann
parents: 73387
diff changeset
   155
    sup_subset_mset_count ~> count_union_mset
716d256259d5 consolidated names
haftmann
parents: 73387
diff changeset
   156
73829
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   157
* Theory "HOL-Library.Multiset": syntax precendence for membership
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   158
operations has been adjusted to match the corresponding precendences on
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   159
sets. Rare INCOMPATIBILITY.
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   160
73886
93ba8e3fdcdf move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents: 73876
diff changeset
   161
* Theory "HOL-Library.Cardinality": code generator setup based on the
93ba8e3fdcdf move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents: 73876
diff changeset
   162
type classes finite_UNIV and card_UNIV has been moved to
93ba8e3fdcdf move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents: 73876
diff changeset
   163
"HOL-Library.Code_Cardinality", to avoid incompatibilities with
93ba8e3fdcdf move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents: 73876
diff changeset
   164
other code setups for sets in AFP/Containers. Applications relying on
93ba8e3fdcdf move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents: 73876
diff changeset
   165
this code setup should import "HOL-Library.Code_Cardinality". Minor
93ba8e3fdcdf move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents: 73876
diff changeset
   166
INCOMPATIBILITY.
93ba8e3fdcdf move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents: 73876
diff changeset
   167
73829
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   168
* Session "HOL-Analysis" and "HOL-Probability": indexed products of
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   169
discrete distributions, negative binomial distribution, Hoeffding's
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   170
inequality, Chernoff bounds, Cauchy–Schwarz inequality for nn_integral,
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   171
and some more small lemmas. Some theorems that were stated awkwardly
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   172
before were corrected. Minor INCOMPATIBILITY.
73253
f6bb31879698 HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents: 73247
diff changeset
   173
73928
3b76524f5a85 Imported lots of material from Stirling_Formula/Gamma_Asymptotics
paulson <lp15@cam.ac.uk>
parents: 73886
diff changeset
   174
* Session "HOL-Analysis": the complex Arg function has been identified
3b76524f5a85 Imported lots of material from Stirling_Formula/Gamma_Asymptotics
paulson <lp15@cam.ac.uk>
parents: 73886
diff changeset
   175
with the function "arg" of Complex_Main, renaming arg->Arg also in the
3b76524f5a85 Imported lots of material from Stirling_Formula/Gamma_Asymptotics
paulson <lp15@cam.ac.uk>
parents: 73886
diff changeset
   176
names of arg_bounded. Minor INCOMPATIBILITY.
3b76524f5a85 Imported lots of material from Stirling_Formula/Gamma_Asymptotics
paulson <lp15@cam.ac.uk>
parents: 73886
diff changeset
   177
73411
1f1366966296 avoid name clash
haftmann
parents: 73409
diff changeset
   178
* Theorems "antisym" and "eq_iff" in class "order" have been renamed to
1f1366966296 avoid name clash
haftmann
parents: 73409
diff changeset
   179
"order.antisym" and "order.eq_iff", to coexist locally with "antisym"
73829
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   180
and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant
73411
1f1366966296 avoid name clash
haftmann
parents: 73409
diff changeset
   181
potential for change can be avoided if interpretations of type class
1f1366966296 avoid name clash
haftmann
parents: 73409
diff changeset
   182
"order" are replaced or augmented by interpretations of locale
1f1366966296 avoid name clash
haftmann
parents: 73409
diff changeset
   183
"ordering".
1f1366966296 avoid name clash
haftmann
parents: 73409
diff changeset
   184
73829
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   185
* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor
73466
ee1c4962671c more lemmas
haftmann
parents: 73465
diff changeset
   186
INCOMPATIBILITY; note that for most applications less elementary lemmas
ee1c4962671c more lemmas
haftmann
parents: 73465
diff changeset
   187
exists.
73411
1f1366966296 avoid name clash
haftmann
parents: 73409
diff changeset
   188
73829
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   189
* Theory "HOL-Library.Permutation" has been renamed to the more specific
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   190
"HOL-Library.List_Permutation". Note that most notions from that theory
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   191
are already present in theory "HOL-Combinatorics.Permutations".
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   192
INCOMPATIBILITY.
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   193
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   194
* Dedicated session "HOL-Combinatorics". INCOMPATIBILITY: theories
73477
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73469
diff changeset
   195
"Permutations", "List_Permutation" (formerly "Permutation"), "Stirling",
73622
4dc3baf45d6a more appropriate location
haftmann
parents: 73616
diff changeset
   196
"Multiset_Permutations", "Perm" have been moved there from session
73681
3708884bfa8a obsolete
haftmann
parents: 73671
diff changeset
   197
HOL-Library.
73477
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73469
diff changeset
   198
73829
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   199
* Theory "HOL-Combinatorics.Transposition" provides elementary swap
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   200
operation "transpose".
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   201
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   202
* Lemma "permutes_induct" has been given stronger hypotheses and named
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   203
premises. INCOMPATIBILITY.
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   204
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   205
* Combinator "Fun.swap" resolved into a mere input abbreviation in
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   206
separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY.
73623
5020054b3a16 tuned theory structure
haftmann
parents: 73622
diff changeset
   207
74097
6d7be1227d02 organize syntax for word operations in bundles
haftmann
parents: 74071
diff changeset
   208
* Infix syntax for bit operations AND, OR, XOR is now organized in
74101
d804e93ae9ff moved theory Bit_Operations into Main corpus
haftmann
parents: 74097
diff changeset
   209
bundle bit_operations_syntax. INCOMPATIBILITY.
74097
6d7be1227d02 organize syntax for word operations in bundles
haftmann
parents: 74071
diff changeset
   210
73682
78044b2f001c explicit type class operations for type-specific implementations
haftmann
parents: 73681
diff changeset
   211
* Bit operations set_bit, unset_bit and flip_bit are now class
73829
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   212
operations. INCOMPATIBILITY.
73682
78044b2f001c explicit type class operations for type-specific implementations
haftmann
parents: 73681
diff changeset
   213
74101
d804e93ae9ff moved theory Bit_Operations into Main corpus
haftmann
parents: 74097
diff changeset
   214
* Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY.
d804e93ae9ff moved theory Bit_Operations into Main corpus
haftmann
parents: 74097
diff changeset
   215
74123
7c5842b06114 clarified abstract and concrete boolean algebras
haftmann
parents: 74110
diff changeset
   216
* Simplified class hierarchy for bit operations: bit operations reside
7c5842b06114 clarified abstract and concrete boolean algebras
haftmann
parents: 74110
diff changeset
   217
in classes (semi)ring_bit_operations, class semiring_bit_shifts is
7c5842b06114 clarified abstract and concrete boolean algebras
haftmann
parents: 74110
diff changeset
   218
gone.
7c5842b06114 clarified abstract and concrete boolean algebras
haftmann
parents: 74110
diff changeset
   219
74163
afe3c8ae1624 consolidation of rules for bit operations
haftmann
parents: 74156
diff changeset
   220
* Expressions of the form "NOT (numeral _)" are not simplified by
afe3c8ae1624 consolidation of rules for bit operations
haftmann
parents: 74156
diff changeset
   221
default any longer.  INCOMPATIBILITY, use not_one_eq and not_numeral_eq
afe3c8ae1624 consolidation of rules for bit operations
haftmann
parents: 74156
diff changeset
   222
as simp rule explicitly if needed.
afe3c8ae1624 consolidation of rules for bit operations
haftmann
parents: 74156
diff changeset
   223
73816
0510c7a4256a moved more legacy to AFP
haftmann
parents: 73788
diff changeset
   224
* Abbreviation "max_word" has been moved to session Word_Lib in the AFP,
0510c7a4256a moved more legacy to AFP
haftmann
parents: 73788
diff changeset
   225
as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1",
73829
aefa7d210725 more formal theory and session names;
wenzelm
parents: 73828
diff changeset
   226
"setBit", "clearBit". See there further the changelog in theory Guide.
73816
0510c7a4256a moved more legacy to AFP
haftmann
parents: 73788
diff changeset
   227
INCOMPATIBILITY.
73788
35217bf33215 max word moved to Word_Lib in AFP
haftmann
parents: 73777
diff changeset
   228
74123
7c5842b06114 clarified abstract and concrete boolean algebras
haftmann
parents: 74110
diff changeset
   229
* Reorganized classes and locales for boolean algebras.
7c5842b06114 clarified abstract and concrete boolean algebras
haftmann
parents: 74110
diff changeset
   230
INCOMPATIBILITY.
7c5842b06114 clarified abstract and concrete boolean algebras
haftmann
parents: 74110
diff changeset
   231
73869
7181130f5872 more default simp rules
haftmann
parents: 73846
diff changeset
   232
* New simp rules: less_exp, min.absorb1, min.absorb2, min.absorb3,
74101
d804e93ae9ff moved theory Bit_Operations into Main corpus
haftmann
parents: 74097
diff changeset
   233
min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor
73869
7181130f5872 more default simp rules
haftmann
parents: 73846
diff changeset
   234
INCOMPATIBILITY.
7181130f5872 more default simp rules
haftmann
parents: 73846
diff changeset
   235
73935
269b2f976100 added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents: 73928
diff changeset
   236
* Sledgehammer:
74110
6c7feeef0ff2 fixed typo
desharna
parents: 74101
diff changeset
   237
 - Removed legacy "lam_lifting" (synonym for "lifting") from option
73935
269b2f976100 added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents: 73928
diff changeset
   238
   "lam_trans". Minor INCOMPATIBILITY.
269b2f976100 added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents: 73928
diff changeset
   239
 - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans".
269b2f976100 added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents: 73928
diff changeset
   240
   Minor INCOMPATIBILITY.
269b2f976100 added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents: 73928
diff changeset
   241
 - Added "opaque_combs" to option "lam_trans": lambda expressions are rewritten
269b2f976100 added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents: 73928
diff changeset
   242
   using combinators, but the combinators are kept opaque, i.e. without
269b2f976100 added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents: 73928
diff changeset
   243
   definitions.
269b2f976100 added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents: 73928
diff changeset
   244
269b2f976100 added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents: 73928
diff changeset
   245
* Metis:
269b2f976100 added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents: 73928
diff changeset
   246
 - Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY.
73253
f6bb31879698 HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents: 73247
diff changeset
   247
74101
d804e93ae9ff moved theory Bit_Operations into Main corpus
haftmann
parents: 74097
diff changeset
   248
73287
wenzelm
parents: 73272
diff changeset
   249
*** ML ***
wenzelm
parents: 73272
diff changeset
   250
74283
wenzelm
parents: 74163
diff changeset
   251
* ML structures TFrees, TVars, Frees, Vars, Names provide scalable
wenzelm
parents: 74163
diff changeset
   252
operations to accumulate items from types and terms, using a fast
wenzelm
parents: 74163
diff changeset
   253
syntactic order. The original order of occurrences may be recovered as
wenzelm
parents: 74163
diff changeset
   254
well, e.g. via TFrees.list_set.
wenzelm
parents: 74163
diff changeset
   255
wenzelm
parents: 74163
diff changeset
   256
* Thm.instantiate, Thm.generalize and related operations require
wenzelm
parents: 74163
diff changeset
   257
scalable datastructures from structure TVars, Vars, Names etc.
wenzelm
parents: 74163
diff changeset
   258
INCOMPATIBILITY: e.g. use TVars.empty and TVars.make for immediate
wenzelm
parents: 74163
diff changeset
   259
adoption; better use TVars.add, TVars.add_tfrees etc. for scalable
wenzelm
parents: 74163
diff changeset
   260
accumulation of items.
wenzelm
parents: 74163
diff changeset
   261
74290
b2ad24b5a42c more antiquotations;
wenzelm
parents: 74289
diff changeset
   262
* ML antiquotations \<^tvar>\<open>?'a::sort\<close> and \<^var>\<open>?x::type\<close> inline
b2ad24b5a42c more antiquotations;
wenzelm
parents: 74289
diff changeset
   263
corresponding ML values, notably as arguments for Thm.instantiate etc.
b2ad24b5a42c more antiquotations;
wenzelm
parents: 74289
diff changeset
   264
74341
edf8b141a8c4 ML antiquotations for object-logic judgment;
wenzelm
parents: 74335
diff changeset
   265
* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to
edf8b141a8c4 ML antiquotations for object-logic judgment;
wenzelm
parents: 74335
diff changeset
   266
corresponding functions for the object-logic of the ML compilation
edf8b141a8c4 ML antiquotations for object-logic judgment;
wenzelm
parents: 74335
diff changeset
   267
context. This supersedes older mk_Trueprop / dest_Trueprop operations.
edf8b141a8c4 ML antiquotations for object-logic judgment;
wenzelm
parents: 74335
diff changeset
   268
74291
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   269
* ML antiquotations for type constructors and term constants:
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   270
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   271
    \<^Type>\<open>c\<close>
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   272
    \<^Type>\<open>c T \<dots>\<close>       \<comment> \<open>same with type arguments\<close>
74317
0a4e93250e44 support ML antiquotations with fn abstraction;
wenzelm
parents: 74291
diff changeset
   273
    \<^Type>_fn\<open>c T \<dots>\<close>    \<comment> \<open>fn abstraction, failure via exception TYPE\<close>
74291
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   274
    \<^Const>\<open>c\<close>
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   275
    \<^Const>\<open>c T \<dots>\<close>      \<comment> \<open>same with type arguments\<close>
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   276
    \<^Const>\<open>c for t \<dots>\<close>  \<comment> \<open>same with term arguments\<close>
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   277
    \<^Const_>\<open>c \<dots>\<close>       \<comment> \<open>same for patterns: case, let, fn\<close>
74317
0a4e93250e44 support ML antiquotations with fn abstraction;
wenzelm
parents: 74291
diff changeset
   278
    \<^Const>_fn\<open>c T \<dots>\<close>   \<comment> \<open>fn abstraction, failure via exception TERM\<close>
74291
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   279
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   280
Examples in HOL:
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   281
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   282
  val natT = \<^Type>\<open>nat\<close>;
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   283
  fun mk_funT (A, B) = \<^Type>\<open>fun A B\<close>;
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   284
  val dest_funT = fn \<^Type>\<open>fun A B\<close> => (A, B);
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   285
  fun mk_conj (A, B) = \<^Const>\<open>conj for A B\<close>;
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   286
  val dest_conj = fn \<^Const_>\<open>conj for A B\<close> => (A, B);
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   287
  fun mk_eq T (t, u) = \<^Const>\<open>HOL.eq T for t u\<close>;
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   288
  val dest_eq = fn \<^Const_>\<open>HOL.eq T for t u\<close> => (T, (t, u));
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   289
74288
wenzelm
parents: 74283
diff changeset
   290
* The "build" combinators of various data structures help to build
wenzelm
parents: 74283
diff changeset
   291
content from bottom-up, by applying an "add" function the "empty" value.
wenzelm
parents: 74283
diff changeset
   292
For example:
wenzelm
parents: 74283
diff changeset
   293
wenzelm
parents: 74283
diff changeset
   294
  - type 'a Symtab.table etc.: build
74289
wenzelm
parents: 74288
diff changeset
   295
  - type 'a Names.table etc.: build
74288
wenzelm
parents: 74283
diff changeset
   296
  - type 'a list: build and build_rev
wenzelm
parents: 74283
diff changeset
   297
  - type Buffer.T: build and build_content
wenzelm
parents: 74283
diff changeset
   298
wenzelm
parents: 74283
diff changeset
   299
For example, see src/Pure/PIDE/xml.ML:
wenzelm
parents: 74283
diff changeset
   300
wenzelm
parents: 74283
diff changeset
   301
  val content_of = Buffer.build_content o fold add_content;
wenzelm
parents: 74283
diff changeset
   302
73550
2f6855142a8c support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents: 73481
diff changeset
   303
* ML antiquotations \<^try>\<open>expr\<close> and \<^can>\<open>expr\<close> operate directly on
2f6855142a8c support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents: 73481
diff changeset
   304
the given ML expression, in contrast to functions "try" and "can" that
2f6855142a8c support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents: 73481
diff changeset
   305
modify application of a function.
2f6855142a8c support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents: 73481
diff changeset
   306
73586
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73550
diff changeset
   307
* ML antiquotations for conditional ML text:
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73550
diff changeset
   308
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73550
diff changeset
   309
    \<^if_linux>\<open>...\<close>
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73550
diff changeset
   310
    \<^if_macos>\<open>...\<close>
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73550
diff changeset
   311
    \<^if_windows>\<open>...\<close>
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73550
diff changeset
   312
    \<^if_unix>\<open>...\<close>
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73550
diff changeset
   313
73287
wenzelm
parents: 73272
diff changeset
   314
* External bash processes are always managed by Isabelle/Scala, in
wenzelm
parents: 73272
diff changeset
   315
contrast to Isabelle2021 where this was only done for macOS on Apple
wenzelm
parents: 73272
diff changeset
   316
Silicon.
wenzelm
parents: 73272
diff changeset
   317
wenzelm
parents: 73272
diff changeset
   318
The main Isabelle/ML interface is Isabelle_System.bash_process with
wenzelm
parents: 73272
diff changeset
   319
result type Process_Result.T (resembling class Process_Result in Scala);
wenzelm
parents: 73272
diff changeset
   320
derived operations Isabelle_System.bash and Isabelle_System.bash_output
wenzelm
parents: 73272
diff changeset
   321
provide similar functionality as before. Rare INCOMPATIBILITY due to
wenzelm
parents: 73272
diff changeset
   322
subtle semantic differences:
wenzelm
parents: 73272
diff changeset
   323
wenzelm
parents: 73272
diff changeset
   324
  - Processes invoked from Isabelle/ML actually run in the context of
wenzelm
parents: 73272
diff changeset
   325
    the Java VM of Isabelle/Scala. The settings environment and current
wenzelm
parents: 73272
diff changeset
   326
    working directory are usually the same on both sides, but there can be
wenzelm
parents: 73272
diff changeset
   327
    subtle corner cases (e.g. unexpected uses of "cd" or "putenv" in ML).
wenzelm
parents: 73272
diff changeset
   328
wenzelm
parents: 73272
diff changeset
   329
  - Output via stdout and stderr is line-oriented: Unix vs. Windows
wenzelm
parents: 73272
diff changeset
   330
    line-endings are normalized towards Unix; presence or absence of a
wenzelm
parents: 73272
diff changeset
   331
    final newline is irrelevant. The original lines are available as
wenzelm
parents: 73272
diff changeset
   332
    Process_Result.out_lines/err_lines; the concatenated versions
wenzelm
parents: 73272
diff changeset
   333
    Process_Result.out/err *omit* a trailing newline (using
wenzelm
parents: 73272
diff changeset
   334
    Library.trim_line, which was occasional seen in applications before,
wenzelm
parents: 73272
diff changeset
   335
    but is no longer necessary).
wenzelm
parents: 73272
diff changeset
   336
wenzelm
parents: 73272
diff changeset
   337
  - Output needs to be plain text encoded in UTF-8: Isabelle/Scala
wenzelm
parents: 73272
diff changeset
   338
    recodes it temporarily as UTF-16. This works for well-formed Unicode
wenzelm
parents: 73272
diff changeset
   339
    text, but not for arbitrary byte strings. In such cases, the bash
wenzelm
parents: 73272
diff changeset
   340
    script should write tempory files, managed by Isabelle/ML operations
wenzelm
parents: 73272
diff changeset
   341
    like Isabelle_System.with_tmp_file to create a file name and
wenzelm
parents: 73272
diff changeset
   342
    File.read to retrieve its content.
wenzelm
parents: 73272
diff changeset
   343
73298
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73297
diff changeset
   344
  - Just like any other Scala function invoked from ML,
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73297
diff changeset
   345
    Isabelle_System.bash_process requires a proper PIDE session context.
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73297
diff changeset
   346
    This could be a regular batch session (e.g. "isabelle build"), a
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73297
diff changeset
   347
    PIDE editor session (e.g. "isabelle jedit"), or headless PIDE (e.g.
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73297
diff changeset
   348
    "isabelle dump" or "isabelle server"). Note that old "isabelle
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73297
diff changeset
   349
    console" or raw "isabelle process" don't have that.
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73297
diff changeset
   350
73287
wenzelm
parents: 73272
diff changeset
   351
New Process_Result.timing works as in Isabelle/Scala, based on direct
wenzelm
parents: 73272
diff changeset
   352
measurements of the bash_process wrapper in C: elapsed time is always
wenzelm
parents: 73272
diff changeset
   353
available, CPU time is only available on Linux and macOS, GC time is
wenzelm
parents: 73272
diff changeset
   354
unavailable.
wenzelm
parents: 73272
diff changeset
   355
73322
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73298
diff changeset
   356
* Likewise, the following Isabelle/ML system operations are run in the
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73298
diff changeset
   357
context of Isabelle/Scala:
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73298
diff changeset
   358
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73298
diff changeset
   359
  - Isabelle_System.make_directory
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73298
diff changeset
   360
  - Isabelle_System.copy_dir
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73298
diff changeset
   361
  - Isabelle_System.copy_file
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73298
diff changeset
   362
  - Isabelle_System.copy_base_file
73324
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73323
diff changeset
   363
  - Isabelle_System.rm_tree
73323
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73322
diff changeset
   364
  - Isabelle_System.download
73322
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73298
diff changeset
   365
73287
wenzelm
parents: 73272
diff changeset
   366
73480
0e880b793db1 support repository archives (without full .hg directory);
wenzelm
parents: 73477
diff changeset
   367
*** System ***
0e880b793db1 support repository archives (without full .hg directory);
wenzelm
parents: 73477
diff changeset
   368
74042
wenzelm
parents: 74003
diff changeset
   369
* Each Isabelle component may specify a Scala/Java jar module
74043
wenzelm
parents: 74042
diff changeset
   370
declaratively via etc/build.props (file names are relative to the
74042
wenzelm
parents: 74003
diff changeset
   371
component directory). E.g. see $ISABELLE_HOME/etc/build.props with
wenzelm
parents: 74003
diff changeset
   372
further explanations in the "system" manual.
wenzelm
parents: 74003
diff changeset
   373
wenzelm
parents: 74003
diff changeset
   374
* Command-line tool "isabelle scala_build" allows to invoke the build
wenzelm
parents: 74003
diff changeset
   375
process of all Scala/Java modules explicitly. Normally this is done
wenzelm
parents: 74003
diff changeset
   376
implicitly on demand, e.g. for "isabelle scala" or "isabelle jedit".
wenzelm
parents: 74003
diff changeset
   377
74071
b25b7c264a93 various improvements of "isabelle scala_project";
wenzelm
parents: 74043
diff changeset
   378
* Command-line tool "isabelle scala_project" is has been improved in
b25b7c264a93 various improvements of "isabelle scala_project";
wenzelm
parents: 74043
diff changeset
   379
various ways:
b25b7c264a93 various improvements of "isabelle scala_project";
wenzelm
parents: 74043
diff changeset
   380
  - sources from all components with etc/build.props are included,
b25b7c264a93 various improvements of "isabelle scala_project";
wenzelm
parents: 74043
diff changeset
   381
  - sources of for the jEdit text editor and the Isabelle/jEdit
b25b7c264a93 various improvements of "isabelle scala_project";
wenzelm
parents: 74043
diff changeset
   382
    plugins (jedit_base and jedit_main) are included by default,
b25b7c264a93 various improvements of "isabelle scala_project";
wenzelm
parents: 74043
diff changeset
   383
  - more sources may be given on the command-line,
b25b7c264a93 various improvements of "isabelle scala_project";
wenzelm
parents: 74043
diff changeset
   384
  - options -f and -D make the tool more convenient.
74042
wenzelm
parents: 74003
diff changeset
   385
wenzelm
parents: 74003
diff changeset
   386
* Isabelle/jEdit is now composed more conventionally from the original
74043
wenzelm
parents: 74042
diff changeset
   387
jEdit text editor in $JEDIT_HOME (with minor patches), plus two Isabelle
wenzelm
parents: 74042
diff changeset
   388
plugins that are produced in $JEDIT_SETTINGS/jars on demand. The main
wenzelm
parents: 74042
diff changeset
   389
isabelle.jedit module is now part of Isabelle/Scala (as one big
wenzelm
parents: 74042
diff changeset
   390
$ISABELLE_SCALA_JAR).
74042
wenzelm
parents: 74003
diff changeset
   391
73842
wenzelm
parents: 73830
diff changeset
   392
* ML profiling has been updated and reactivated, after some degration in
wenzelm
parents: 73830
diff changeset
   393
Isabelle2021:
wenzelm
parents: 73830
diff changeset
   394
wenzelm
parents: 73830
diff changeset
   395
  - "isabelle build -o threads=1 -o profiling=..." works properly
wenzelm
parents: 73830
diff changeset
   396
    within the PIDE session context;
wenzelm
parents: 73830
diff changeset
   397
wenzelm
parents: 73830
diff changeset
   398
  - "isabelle profiling_report" now uses the session build database
wenzelm
parents: 73830
diff changeset
   399
    (like "isabelle log");
wenzelm
parents: 73830
diff changeset
   400
wenzelm
parents: 73830
diff changeset
   401
  - output uses non-intrusive tracing messages, instead of warnings.
wenzelm
parents: 73830
diff changeset
   402
73777
52e43a93d51f clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
wenzelm
parents: 73774
diff changeset
   403
* System option "system_log" specifies an optional log file for internal
73826
72900f34dbb3 allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents: 73816
diff changeset
   404
messages produced by Output.system_message in Isabelle/ML; the value
72900f34dbb3 allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents: 73816
diff changeset
   405
"true" refers to console progress of the build job. This works for
72900f34dbb3 allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents: 73816
diff changeset
   406
"isabelle build" or any derivative of it.
72900f34dbb3 allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents: 73816
diff changeset
   407
72900f34dbb3 allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents: 73816
diff changeset
   408
* System options of type string may be set to "true" using the short
72900f34dbb3 allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents: 73816
diff changeset
   409
notation of type bool. E.g. "isabelle build -o system_log".
72900f34dbb3 allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents: 73816
diff changeset
   410
72900f34dbb3 allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents: 73816
diff changeset
   411
* System option "document=true" is an alias for "document=pdf" and thus
72900f34dbb3 allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents: 73816
diff changeset
   412
can be used in the short form. E.g. "isabelle build -o document".
73774
734d5d3fbd9d syslog option for "isabelle build";
wenzelm
parents: 73771
diff changeset
   413
73480
0e880b793db1 support repository archives (without full .hg directory);
wenzelm
parents: 73477
diff changeset
   414
* Command-line tool "isabelle version" supports repository archives
73481
92db3e31fae3 clarified output;
wenzelm
parents: 73480
diff changeset
   415
(without full .hg directory). More options.
73480
0e880b793db1 support repository archives (without full .hg directory);
wenzelm
parents: 73477
diff changeset
   416
73671
7404f2e1d092 clarified platforms;
wenzelm
parents: 73648
diff changeset
   417
* Obsolete settings variable ISABELLE_PLATFORM32 has been discontinued.
7404f2e1d092 clarified platforms;
wenzelm
parents: 73648
diff changeset
   418
Note that only Windows supports old 32 bit executables, via settings
7404f2e1d092 clarified platforms;
wenzelm
parents: 73648
diff changeset
   419
variable ISABELLE_WINDOWS_PLATFORM32. Everything else should be
7404f2e1d092 clarified platforms;
wenzelm
parents: 73648
diff changeset
   420
ISABELLE_PLATFORM64 (generic Posix) or ISABELLE_WINDOWS_PLATFORM64
7404f2e1d092 clarified platforms;
wenzelm
parents: 73648
diff changeset
   421
(native Windows) or ISABELLE_APPLE_PLATFORM64 (Apple Silicon).
7404f2e1d092 clarified platforms;
wenzelm
parents: 73648
diff changeset
   422
73480
0e880b793db1 support repository archives (without full .hg directory);
wenzelm
parents: 73477
diff changeset
   423
73287
wenzelm
parents: 73272
diff changeset
   424
72972
31ff3c962937 misc tuning for release;
wenzelm
parents: 72971
diff changeset
   425
New in Isabelle2021 (February 2021)
31ff3c962937 misc tuning for release;
wenzelm
parents: 72971
diff changeset
   426
-----------------------------------
71557
61ba52af28e3 back to post-release mode;
wenzelm
parents: 71551
diff changeset
   427
72232
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
   428
*** General ***
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
   429
73194
c0d6d57a9a31 more NEWS;
wenzelm
parents: 73174
diff changeset
   430
* On macOS, the IsabelleXYZ.app directory layout now follows the other
c0d6d57a9a31 more NEWS;
wenzelm
parents: 73174
diff changeset
   431
platforms, without indirection via Contents/Resources/. INCOMPATIBILITY,
c0d6d57a9a31 more NEWS;
wenzelm
parents: 73174
diff changeset
   432
use e.g. IsabelleXYZ.app/bin/isabelle instead of former
c0d6d57a9a31 more NEWS;
wenzelm
parents: 73174
diff changeset
   433
IsabelleXYZ.app/Isabelle/bin/isabelle or
c0d6d57a9a31 more NEWS;
wenzelm
parents: 73174
diff changeset
   434
IsabelleXYZ.app/Isabelle/Contents/Resources/IsabelleXYZ/bin/isabelle.
c0d6d57a9a31 more NEWS;
wenzelm
parents: 73174
diff changeset
   435
73078
824815ec52aa more NEWS;
wenzelm
parents: 73052
diff changeset
   436
* HTML presentation uses rich markup produced by Isabelle/PIDE,
824815ec52aa more NEWS;
wenzelm
parents: 73052
diff changeset
   437
resulting in more colors and links.
824815ec52aa more NEWS;
wenzelm
parents: 73052
diff changeset
   438
824815ec52aa more NEWS;
wenzelm
parents: 73052
diff changeset
   439
* HTML presentation includes auxiliary files (e.g. ML) for each theory.
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   440
72232
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
   441
* Proof method "subst" is confined to the original subgoal range: its
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
   442
included distinct_subgoals_tac no longer affects unrelated subgoals.
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
   443
Rare INCOMPATIBILITY.
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
   444
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   445
* Theory_Data extend operation is obsolete and needs to be the identity
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   446
function; merge should be conservative and not reset to the empty value.
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   447
Subtle INCOMPATIBILITY and change of semantics (due to
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   448
Theory.join_theory from Isabelle2020). Special extend/merge behaviour at
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   449
the begin of a new theory can be achieved via Theory.at_begin.
72996
cdcd2785db94 more NEWS;
wenzelm
parents: 72987
diff changeset
   450
72232
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
   451
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 71927
diff changeset
   452
*** Isabelle/jEdit Prover IDE ***
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 71927
diff changeset
   453
73116
b84887a67cc6 clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents: 73112
diff changeset
   454
* Improved GUI look-and-feel: the portable and scalable "FlatLaf Light"
b84887a67cc6 clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents: 73112
diff changeset
   455
is used by default on all platforms (appearance similar to IntelliJ
b84887a67cc6 clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents: 73112
diff changeset
   456
IDEA).
73112
efc58b56a6c7 clarified default L&F;
wenzelm
parents: 73108
diff changeset
   457
72946
9329abcdd651 improved markup for theory header imports;
wenzelm
parents: 72932
diff changeset
   458
* Improved markup for theory header imports: hyperlinks for theory files
9329abcdd651 improved markup for theory header imports;
wenzelm
parents: 72932
diff changeset
   459
work without formal checking of content.
9329abcdd651 improved markup for theory header imports;
wenzelm
parents: 72932
diff changeset
   460
72950
ac6457a70db5 download auxiliary files via "curl";
wenzelm
parents: 72946
diff changeset
   461
* The prover process can download auxiliary files (e.g. 'ML_file') for
ac6457a70db5 download auxiliary files via "curl";
wenzelm
parents: 72946
diff changeset
   462
theories with remote URL. This requires the external "curl" program.
ac6457a70db5 download auxiliary files via "curl";
wenzelm
parents: 72946
diff changeset
   463
72930
0cc298e29aff added action isabelle.goto-entity to follow links in a narrow formal sense;
wenzelm
parents: 72879
diff changeset
   464
* Action "isabelle.goto-entity" (shortcut CS+d) jumps to the definition
0cc298e29aff added action isabelle.goto-entity to follow links in a narrow formal sense;
wenzelm
parents: 72879
diff changeset
   465
of the formal entity at the caret position.
0cc298e29aff added action isabelle.goto-entity to follow links in a narrow formal sense;
wenzelm
parents: 72879
diff changeset
   466
72932
f7954a960890 more NEWS;
wenzelm
parents: 72930
diff changeset
   467
* The visual feedback on caret entity focus is normally restricted to
f7954a960890 more NEWS;
wenzelm
parents: 72930
diff changeset
   468
definitions within the visible text area. The keyboard modifier "CS"
f7954a960890 more NEWS;
wenzelm
parents: 72930
diff changeset
   469
overrides this: then all defining and referencing positions are shown.
f7954a960890 more NEWS;
wenzelm
parents: 72930
diff changeset
   470
See also option "jedit_focus_modifier".
f7954a960890 more NEWS;
wenzelm
parents: 72930
diff changeset
   471
72249
4bf8a8a2d2ad more uniform JVM vs. ML status widget;
wenzelm
parents: 72247
diff changeset
   472
* The jEdit status line includes widgets both for JVM and ML heap usage.
4bf8a8a2d2ad more uniform JVM vs. ML status widget;
wenzelm
parents: 72247
diff changeset
   473
Ongoing ML ongoing garbage collection is shown as "ML cleanup".
72150
510ebf846696 more documentation;
wenzelm
parents: 72120
diff changeset
   474
510ebf846696 more documentation;
wenzelm
parents: 72120
diff changeset
   475
* The Monitor dockable provides buttons to request a full garbage
510ebf846696 more documentation;
wenzelm
parents: 72120
diff changeset
   476
collection and sharing of live data on the ML heap. It also includes
510ebf846696 more documentation;
wenzelm
parents: 72120
diff changeset
   477
information about the Java Runtime system.
510ebf846696 more documentation;
wenzelm
parents: 72120
diff changeset
   478
72837
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72810
diff changeset
   479
* PIDE support for session ROOTS: markup for directories.
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72810
diff changeset
   480
72247
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 72232
diff changeset
   481
* Update to jedit-5.6.0, the latest release. This version works properly
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 72232
diff changeset
   482
on macOS by default, without the special MacOSX plugin.
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 71927
diff changeset
   483
73121
6345ad861a36 more documentation;
wenzelm
parents: 73116
diff changeset
   484
* Action "full-screen-mode" (shortcut F11 or S+F11) has been modified
6345ad861a36 more documentation;
wenzelm
parents: 73116
diff changeset
   485
for better approximate window size on macOS and Linux/X11.
6345ad861a36 more documentation;
wenzelm
parents: 73116
diff changeset
   486
73162
c4b688abe2c4 clarified documentation concerning macOS Big Sur;
wenzelm
parents: 73156
diff changeset
   487
* Improved GUI support for macOS 11.1 Big Sur: native fullscreen mode,
c4b688abe2c4 clarified documentation concerning macOS Big Sur;
wenzelm
parents: 73156
diff changeset
   488
but non-native look-and-feel (FlatLaf).
c4b688abe2c4 clarified documentation concerning macOS Big Sur;
wenzelm
parents: 73156
diff changeset
   489
73247
d92409f8203a tuned NEWS;
wenzelm
parents: 73232
diff changeset
   490
* Hyperlinks to various file-formats (.pdf, .png, etc.) open an external
d92409f8203a tuned NEWS;
wenzelm
parents: 73232
diff changeset
   491
viewer, instead of re-using the jEdit text editor.
d92409f8203a tuned NEWS;
wenzelm
parents: 73232
diff changeset
   492
73174
ab3fa0abc119 IDE support for Naproche-SAD;
wenzelm
parents: 73172
diff changeset
   493
* IDE support for Naproche-SAD: Proof Checking of Natural Mathematical
ab3fa0abc119 IDE support for Naproche-SAD;
wenzelm
parents: 73172
diff changeset
   494
Documents. See also $NAPROCHE_HOME/examples for files with .ftl or
73247
d92409f8203a tuned NEWS;
wenzelm
parents: 73232
diff changeset
   495
.ftl.tex extension. The corresponding Naproche-SAD server process can be
d92409f8203a tuned NEWS;
wenzelm
parents: 73232
diff changeset
   496
disabled by setting the system option naproche_server=false and
d92409f8203a tuned NEWS;
wenzelm
parents: 73232
diff changeset
   497
restarting the Isabelle application.
73224
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73194
diff changeset
   498
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 71927
diff changeset
   499
71902
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 71901
diff changeset
   500
*** Document preparation ***
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 71901
diff changeset
   501
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72581
diff changeset
   502
* Keyword 'document_theories' within ROOT specifies theories from other
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72581
diff changeset
   503
sessions that should be included in the generated document source
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72581
diff changeset
   504
directory. This does not affect the generated session.tex: \input{...}
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72581
diff changeset
   505
needs to be used separately.
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72581
diff changeset
   506
72314
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
   507
* The standard LaTeX engine is now lualatex, according to settings
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
   508
variable ISABELLE_PDFLATEX. This is mostly upwards compatible with old
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
   509
pdflatex, but text encoding needs to conform strictly to utf8. Rare
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
   510
INCOMPATIBILITY.
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
   511
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
   512
* Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
   513
document output is always PDF.
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
   514
72763
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72749
diff changeset
   515
* Antiquotation @{tool} refers to Isabelle command-line tools, with
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72749
diff changeset
   516
completion and formal reference to the source (external script or
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72749
diff changeset
   517
internal Scala function).
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72749
diff changeset
   518
71908
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
   519
* Antiquotation @{bash_function} refers to GNU bash functions that are
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
   520
checked within the Isabelle settings environment.
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
   521
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
   522
* Antiquotations @{scala}, @{scala_object}, @{scala_type},
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
   523
@{scala_method} refer to checked Isabelle/Scala entities.
71902
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 71901
diff changeset
   524
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 71901
diff changeset
   525
71901
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   526
*** Pure ***
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   527
71924
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents: 71923
diff changeset
   528
* Session Pure-Examples contains notable examples for Isabelle/Pure
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents: 71923
diff changeset
   529
(former entries of HOL-Isar_Examples).
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents: 71923
diff changeset
   530
72739
e7c2848b78e8 refined syntax for bundle mixins for locale and class specifications
haftmann
parents: 72728
diff changeset
   531
* Named contexts (locale and class specifications, locale and class
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   532
context blocks) allow bundle mixins for the surface context. This allows
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   533
syntax notations to be organized within bundles conveniently. See theory
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   534
"HOL-ex.Specifications_with_bundle_mixins" for examples and the isar-ref
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   535
manual for syntax descriptions.
72739
e7c2848b78e8 refined syntax for bundle mixins for locale and class specifications
haftmann
parents: 72728
diff changeset
   536
71901
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   537
* Definitions in locales produce rule which can be added as congruence
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   538
rule to protect foundational terms during simplification.
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   539
72450
24bd1316eaae consolidated names and operations
haftmann
parents: 72388
diff changeset
   540
* Consolidated terminology and function signatures for nested targets:
24bd1316eaae consolidated names and operations
haftmann
parents: 72388
diff changeset
   541
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   542
  - Local_Theory.begin_nested replaces Local_Theory.open_target
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   543
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   544
  - Local_Theory.end_nested replaces Local_Theory.close_target
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   545
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   546
  - Combination of Local_Theory.begin_nested and
72451
e51f1733618d replaced combinators by more conventional nesting pattern
haftmann
parents: 72450
diff changeset
   547
    Local_Theory.end_nested(_result) replaces
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   548
    Local_Theory.subtarget(_result)
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   549
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   550
INCOMPATIBILITY.
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   551
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   552
* Local_Theory.init replaces Generic_Target.init. Minor INCOMPATIBILITY.
72516
17dc99589a91 unified Local_Theory.init with Generic_Target.init
haftmann
parents: 72515
diff changeset
   553
71901
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   554
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   555
*** HOL ***
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   556
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   557
* Session HOL-Examples contains notable examples for Isabelle/HOL
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   558
(former entries of HOL-Isar_Examples, HOL-ex etc.).
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   559
72478
b452242dce36 proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents: 72470
diff changeset
   560
* An updated version of the veriT solver is now included as Isabelle
b452242dce36 proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents: 72470
diff changeset
   561
component. It can be used in the "smt" proof method via "smt (verit)" or
b452242dce36 proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents: 72470
diff changeset
   562
via "declare [[smt_solver = verit]]" in the context; see also session
b452242dce36 proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents: 72470
diff changeset
   563
HOL-Word-SMT_Examples.
b452242dce36 proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents: 72470
diff changeset
   564
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   565
* Zipperposition 2.0 is now included as Isabelle component for
72971
162b71f7e554 rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;
wenzelm
parents: 72969
diff changeset
   566
experimentation, e.g. in "sledgehammer [prover = zipperposition]".
162b71f7e554 rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;
wenzelm
parents: 72969
diff changeset
   567
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   568
* Sledgehammer:
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   569
  - support veriT in proof preplay
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   570
  - take adventage of more cores in proof preplay
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   571
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   572
* Updated the Metis prover underlying the "metis" proof method to
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   573
version 2.4 (release 20180810). The new version fixes one soundness
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   574
defect and two incompleteness defects. Very slight INCOMPATIBILITY.
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   575
72208
wenzelm
parents: 72163
diff changeset
   576
* Nitpick/Kodkod may be invoked directly within the running
wenzelm
parents: 72163
diff changeset
   577
Isabelle/Scala session (instead of an external Java process): this
wenzelm
parents: 72163
diff changeset
   578
improves reactivity and saves resources. This experimental feature is
73008
dacf2598bb27 proper NEWS according to current situation;
wenzelm
parents: 73007
diff changeset
   579
guarded by system option "kodkod_scala" (default: true in PIDE
dacf2598bb27 proper NEWS according to current situation;
wenzelm
parents: 73007
diff changeset
   580
interaction, false in batch builds).
72208
wenzelm
parents: 72163
diff changeset
   581
72070
wenzelm
parents: 72060
diff changeset
   582
* Simproc "defined_all" and rewrite rule "subst_all" perform more
wenzelm
parents: 72060
diff changeset
   583
aggressive substitution with variables from assumptions.
wenzelm
parents: 72060
diff changeset
   584
INCOMPATIBILITY, consider repairing proofs locally like this:
wenzelm
parents: 72060
diff changeset
   585
wenzelm
parents: 72060
diff changeset
   586
  supply subst_all [simp del] [[simproc del: defined_all]]
wenzelm
parents: 72060
diff changeset
   587
71901
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   588
* Simproc "datatype_no_proper_subterm" rewrites equalities "lhs = rhs"
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   589
on datatypes to "False" if either side is a proper subexpression of the
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   590
other (for any datatype with a reasonable size function).
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   591
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   592
* Syntax for state monad combinators fcomp and scomp is organized in
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   593
bundle state_combinator_syntax.  Minor INCOMPATIBILITY.
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   594
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   595
* Syntax for reflected term syntax is organized in bundle term_syntax,
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   596
discontinuing previous locale term_syntax.  Minor INCOMPATIBILITY.
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   597
71901
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   598
* New constant "power_int" for exponentiation with integer exponent,
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   599
written as "x powi n".
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   600
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   601
* Added the "at most 1" quantifier, Uniq.
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   602
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   603
* For the natural numbers, "Sup {} = 0".
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 72001
diff changeset
   604
73108
981a383610df HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents: 73094
diff changeset
   605
* New constant semiring_char gives the characteristic of any type of
981a383610df HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents: 73094
diff changeset
   606
class semiring_1, with the convenient notation CHAR('a). For example,
981a383610df HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents: 73094
diff changeset
   607
CHAR(nat) = CHAR(int) = CHAR(real) = 0, CHAR(17) = 17.
981a383610df HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents: 73094
diff changeset
   608
981a383610df HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents: 73094
diff changeset
   609
* HOL-Computational_Algebra.Polynomial: Definition and basic properties
981a383610df HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents: 73094
diff changeset
   610
of algebraic integers.
981a383610df HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents: 73094
diff changeset
   611
71956
a4bffc0de967 bit operations as distinctive library theory
haftmann
parents: 71949
diff changeset
   612
* Library theory "Bit_Operations" with generic bit operations.
a4bffc0de967 bit operations as distinctive library theory
haftmann
parents: 71949
diff changeset
   613
72281
beeadb35e357 more thorough treatment of division, particularly signed division on int and word
haftmann
parents: 72264
diff changeset
   614
* Library theory "Signed_Division" provides operations for signed
beeadb35e357 more thorough treatment of division, particularly signed division on int and word
haftmann
parents: 72264
diff changeset
   615
division, instantiated for type int.
beeadb35e357 more thorough treatment of division, particularly signed division on int and word
haftmann
parents: 72264
diff changeset
   616
73047
ab9e27da0e85 HOL-Library: Changed notation for sum_mset
Manuel Eberl <eberlm@in.tum.de>
parents: 73009
diff changeset
   617
* Theory "Multiset": removed misleading notation \<Union># for sum_mset;
73094
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   618
replaced with \<Sum>\<^sub>#. Analogous notation for prod_mset also exists now.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   619
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   620
* New theory "HOL-Library.Word" takes over material from former session
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   621
"HOL-Word". INCOMPATIBILITY: need to adjust imports.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   622
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   623
* Theory "HOL-Library.Word": Type word is restricted to bit strings
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   624
consisting of at least one bit. INCOMPATIBILITY.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   625
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   626
* Theory "HOL-Library.Word": Bit operations NOT, AND, OR, XOR are based
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   627
on generic algebraic bit operations from theory
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   628
"HOL-Library.Bit_Operations". INCOMPATIBILITY.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   629
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   630
* Theory "HOL-Library.Word": Most operations on type word are set up for
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   631
transfer and lifting. INCOMPATIBILITY.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   632
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   633
* Theory "HOL-Library.Word": Generic type conversions. INCOMPATIBILITY,
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   634
sometimes additional rewrite rules must be added to applications to get
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   635
a confluent system again.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   636
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   637
* Theory "HOL-Library.Word": Uniform polymorphic "mask" operation for
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   638
both types int and word. INCOMPATIBILITY.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   639
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   640
* Theory "HOL-Library.Word": Syntax for signed compare operators has
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73078
diff changeset
   641
been consolidated with syntax of regular compare operators. Minor
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   642
INCOMPATIBILITY.
72388
633d14bd1e59 consolidated for the sake of documentation
haftmann
parents: 72332
diff changeset
   643
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   644
* Former session "HOL-Word": Various operations dealing with bit values
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   645
represented as reversed lists of bools are separated into theory
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   646
Reversed_Bit_Lists in session Word_Lib in the AFP. INCOMPATIBILITY.
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   647
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   648
* Former session "HOL-Word": Theory "Word_Bitwise" has been moved to AFP
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   649
entry Word_Lib as theory "Bitwise". INCOMPATIBILITY.
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   650
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   651
* Former session "HOL-Word": Compound operation "bin_split" simplifies
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   652
by default into its components "drop_bit" and "take_bit".
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   653
INCOMPATIBILITY.
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   654
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   655
* Former session "HOL-Word": Operations lsb, msb and set_bit are
72546
58b1826354c9 NEWS and CONTRIBUTORS
haftmann
parents: 72521
diff changeset
   656
separated into theories Least_significant_bit, Most_significant_bit and
58b1826354c9 NEWS and CONTRIBUTORS
haftmann
parents: 72521
diff changeset
   657
Generic_set_bit respectively in session Word_Lib in the AFP.
58b1826354c9 NEWS and CONTRIBUTORS
haftmann
parents: 72521
diff changeset
   658
INCOMPATIBILITY.
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   659
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   660
* Former session "HOL-Word": Ancient int numeral representation has been
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   661
factored out in separate theory "Ancient_Numeral" in session Word_Lib in
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   662
the AFP. INCOMPATIBILITY.
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   663
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   664
* Former session "HOL-Word": Operations "bin_last", "bin_rest",
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   665
"bin_nth", "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   666
"max_word" are now mere input abbreviations. Minor INCOMPATIBILITY.
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   667
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   668
* Former session "HOL-Word": Misc ancient material has been factored out
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   669
into separate theories and moved to session Word_Lib in the AFP. See
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   670
theory "Guide" there for further information. INCOMPATIBILITY.
71987
ec17263ec38d removed superfluous dependency
haftmann
parents: 71986
diff changeset
   671
72070
wenzelm
parents: 72060
diff changeset
   672
* Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands
wenzelm
parents: 72060
diff changeset
   673
are in working order again, as opposed to outputting "GaveUp" on nearly
wenzelm
parents: 72060
diff changeset
   674
all problems.
71959
ee2c7f0dd1be prefer single name
haftmann
parents: 71957
diff changeset
   675
72987
b1be35908165 clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents: 72972
diff changeset
   676
* Session "HOL-Hoare": concrete syntax only for Hoare triples, not
b1be35908165 clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents: 72972
diff changeset
   677
abstract language constructors.
b1be35908165 clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents: 72972
diff changeset
   678
b1be35908165 clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents: 72972
diff changeset
   679
* Session "HOL-Hoare": now provides a total correctness logic as well.
b1be35908165 clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents: 72972
diff changeset
   680
71901
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   681
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   682
*** FOL ***
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   683
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   684
* Added the "at most 1" quantifier, Uniq, as in HOL.
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   685
72070
wenzelm
parents: 72060
diff changeset
   686
* Simproc "defined_all" and rewrite rule "subst_all" have been changed
wenzelm
parents: 72060
diff changeset
   687
as in HOL.
71923
haftmann
parents: 71909
diff changeset
   688
71901
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   689
71908
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
   690
*** ML ***
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
   691
72332
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72316
diff changeset
   692
* Antiquotations @{scala_function}, @{scala}, @{scala_thread} refer to
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72316
diff changeset
   693
registered Isabelle/Scala functions (of type String => String):
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72316
diff changeset
   694
invocation works via the PIDE protocol.
71908
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
   695
72511
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72510
diff changeset
   696
* Path.append is available as overloaded "+" operator, similar to
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72510
diff changeset
   697
corresponding Isabelle/Scala operation.
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72510
diff changeset
   698
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   699
* ML statistics via an external Poly/ML process: this allows monitoring
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   700
the runtime system while the ML program sleeps.
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   701
71908
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
   702
71715
wenzelm
parents: 71666
diff changeset
   703
*** System ***
wenzelm
parents: 71666
diff changeset
   704
73007
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   705
* Isabelle server allows user-defined commands via
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   706
isabelle_scala_service.
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   707
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   708
* Update/rebuild external provers on currently supported OS platforms,
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   709
notably CVC4 1.8, E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
11140980a6b5 updated for release;
wenzelm
parents: 72996
diff changeset
   710
72879
b3e9e9e4ff74 clarified session log file: avoid erratic messages;
wenzelm
parents: 72876
diff changeset
   711
* The command-line tool "isabelle log" prints prover messages from the
b3e9e9e4ff74 clarified session log file: avoid erratic messages;
wenzelm
parents: 72876
diff changeset
   712
build database of the given session, following the the order of theory
b3e9e9e4ff74 clarified session log file: avoid erratic messages;
wenzelm
parents: 72876
diff changeset
   713
sources, instead of erratic parallel evaluation. Consequently, the
b3e9e9e4ff74 clarified session log file: avoid erratic messages;
wenzelm
parents: 72876
diff changeset
   714
session log file is restricted to system messages of the overall build
b3e9e9e4ff74 clarified session log file: avoid erratic messages;
wenzelm
parents: 72876
diff changeset
   715
process, and thus becomes more informative.
72876
626fcaebd049 NEWS and documentation for "isabelle log";
wenzelm
parents: 72837
diff changeset
   716
72309
564012e31db1 discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents: 72299
diff changeset
   717
* Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
564012e31db1 discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents: 72299
diff changeset
   718
variable.
564012e31db1 discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents: 72299
diff changeset
   719
72316
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72314
diff changeset
   720
* The command-line tool "isabelle logo" only outputs PDF; obsolete EPS
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72314
diff changeset
   721
(for DVI documents) has been discontinued. Former option -n has been
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72314
diff changeset
   722
turned into -o with explicit file name. Minor INCOMPATIBILITY.
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72314
diff changeset
   723
73172
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 73162
diff changeset
   724
* The command-line tool "isabelle components" supports new options -u
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 73162
diff changeset
   725
and -x to manage $ISABELLE_HOME_USER/etc/components without manual
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 73162
diff changeset
   726
editing of Isabelle configuration files.
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 73162
diff changeset
   727
72162
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72150
diff changeset
   728
* The shell function "isabelle_directory" (within etc/settings of
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72150
diff changeset
   729
components) augments the list of special directories for persistent
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72150
diff changeset
   730
symbolic path names. This improves portability of heap images and
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72150
diff changeset
   731
session databases. It used to be hard-wired for Isabelle + AFP, but
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72150
diff changeset
   732
other projects may now participate on equal terms.
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72150
diff changeset
   733
72681
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   734
* The command-line tool "isabelle process" now prints output to
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   735
stdout/stderr separately and incrementally, instead of just one bulk to
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   736
stdout after termination. Potential INCOMPATIBILITY for external tools.
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   737
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   738
* The command-line tool "isabelle console" now supports interrupts
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   739
properly (on Linux and macOS).
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   740
72103
7b318273a4aa discontinued old batch-build functionality;
wenzelm
parents: 72088
diff changeset
   741
* Batch-builds via "isabelle build" use a PIDE session with special
7b318273a4aa discontinued old batch-build functionality;
wenzelm
parents: 72088
diff changeset
   742
protocol: this allows to invoke Isabelle/Scala operations from
7b318273a4aa discontinued old batch-build functionality;
wenzelm
parents: 72088
diff changeset
   743
Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for the
7b318273a4aa discontinued old batch-build functionality;
wenzelm
parents: 72088
diff changeset
   744
java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings:
71976
80d7f004089d clarified NEWS;
wenzelm
parents: 71975
diff changeset
   745
80d7f004089d clarified NEWS;
wenzelm
parents: 71975
diff changeset
   746
  ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx8g"
71975
2d658beb815b enable pide_session by default (again), with extra JVM heap for AFP tests (see also 86e429abd38d, 026de3424c39);
wenzelm
parents: 71964
diff changeset
   747
72728
caa182bdab7a clarified options: batch-build has pide_reports disabled by default (requires significant resources);
wenzelm
parents: 72684
diff changeset
   748
This includes full PIDE markup, if option "build_pide_reports" is
caa182bdab7a clarified options: batch-build has pide_reports disabled by default (requires significant resources);
wenzelm
parents: 72684
diff changeset
   749
enabled.
caa182bdab7a clarified options: batch-build has pide_reports disabled by default (requires significant resources);
wenzelm
parents: 72684
diff changeset
   750
72679
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   751
* The command-line tool "isabelle build" provides option -P DIR to
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   752
produce PDF/HTML presentation in the specified directory; -P: refers to
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   753
the standard directory according to ISABELLE_BROWSER_INFO /
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   754
ISABELLE_BROWSER_INFO_SYSTEM settings. Generated PDF documents are taken
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   755
from the build database -- from this or earlier builds with option
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   756
document=pdf.
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   757
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72557
diff changeset
   758
* The command-line tool "isabelle document" generates theory documents
72679
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   759
on the spot, using the underlying session build database (exported
72681
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   760
LaTeX sources or existing PDF files). INCOMPATIBILITY, the former
72679
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   761
"isabelle document" tool was rather different and has been discontinued.
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72557
diff changeset
   762
71808
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71788
diff changeset
   763
* The command-line tool "isabelle sessions" explores the structure of
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71788
diff changeset
   764
Isabelle sessions and prints result names in topological order (on
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71788
diff changeset
   765
stdout).
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71788
diff changeset
   766
71733
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71728
diff changeset
   767
* The Isabelle/Scala "Progress" interface changed slightly and
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71728
diff changeset
   768
"No_Progress" has been discontinued. INCOMPATIBILITY, use "new Progress"
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71728
diff changeset
   769
instead.
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71728
diff changeset
   770
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71728
diff changeset
   771
* General support for Isabelle/Scala system services, configured via the
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71728
diff changeset
   772
shell function "isabelle_scala_service" in etc/settings (e.g. of an
71741
wenzelm
parents: 71736
diff changeset
   773
Isabelle component); see implementations of class
wenzelm
parents: 71736
diff changeset
   774
Isabelle_System.Service in Isabelle/Scala. This supersedes former
wenzelm
parents: 71736
diff changeset
   775
"isabelle_scala_tools" and "isabelle_file_format": minor
wenzelm
parents: 71736
diff changeset
   776
INCOMPATIBILITY.
71728
wenzelm
parents: 71715
diff changeset
   777
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   778
* The syntax of theory load commands (for auxiliary files) is now
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   779
specified in Isabelle/Scala, as instance of class
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   780
isabelle.Command_Span.Load_Command registered via isabelle_scala_service
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   781
in etc/settings. This allows more flexible schemes than just a list of
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   782
file extensions. Minor INCOMPATIBILITY, e.g. see theory
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   783
HOL-SPARK.SPARK_Setup to emulate the old behaviour.
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   784
73116
b84887a67cc6 clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents: 73112
diff changeset
   785
* JVM system property "isabelle.laf" has been discontinued; the default
b84887a67cc6 clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents: 73112
diff changeset
   786
Swing look-and-feel is ""FlatLaf Light".
b84887a67cc6 clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents: 73112
diff changeset
   787
72521
354bfab78cbf Isabelle/Phabricator supports Ubuntu 20.04 LTS;
wenzelm
parents: 72518
diff changeset
   788
* Isabelle/Phabricator supports Ubuntu 20.04 LTS.
354bfab78cbf Isabelle/Phabricator supports Ubuntu 20.04 LTS;
wenzelm
parents: 72518
diff changeset
   789
71845
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 71839
diff changeset
   790
* Isabelle/Phabricator setup has been updated to follow ongoing
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 71839
diff changeset
   791
development: libphutil has been discontinued. Minor INCOMPATIBILITY:
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 71839
diff changeset
   792
existing server installations should remove libphutil from
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 71839
diff changeset
   793
/usr/local/bin/isabelle-phabricator-upgrade and each installation root
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 71839
diff changeset
   794
directory (e.g. /var/www/phabricator-vcs/libphutil).
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 71839
diff changeset
   795
72510
wenzelm
parents: 72478
diff changeset
   796
* Experimental support for arm64-linux platform. The reference platform
wenzelm
parents: 72478
diff changeset
   797
is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
wenzelm
parents: 72478
diff changeset
   798
73232
030b930d1ac8 updated for release;
wenzelm
parents: 73224
diff changeset
   799
* Support for Apple Silicon, using mostly x86_64-darwin runtime
030b930d1ac8 updated for release;
wenzelm
parents: 73224
diff changeset
   800
translation via Rosetta 2 (e.g. Poly/ML and external provers), but also
030b930d1ac8 updated for release;
wenzelm
parents: 73224
diff changeset
   801
some native arm64-darwin executables (e.g. Java).
73154
56107393f2ef more NEWS;
wenzelm
parents: 73143
diff changeset
   802
71557
61ba52af28e3 back to post-release mode;
wenzelm
parents: 71551
diff changeset
   803
71839
0bbe0866b7e6 The Uniq quantifier for FOL too
paulson <lp15@cam.ac.uk>
parents: 71837
diff changeset
   804
71485
29e297fd5473 updated for release;
wenzelm
parents: 71484
diff changeset
   805
New in Isabelle2020 (April 2020)
29e297fd5473 updated for release;
wenzelm
parents: 71484
diff changeset
   806
--------------------------------
70265
a8238fd25541 back to post-release mode;
wenzelm
parents: 70260
diff changeset
   807
70562
wenzelm
parents: 70525
diff changeset
   808
*** General ***
wenzelm
parents: 70525
diff changeset
   809
70677
56d70f7ce4a4 more documentation;
wenzelm
parents: 70608
diff changeset
   810
* Session ROOT files need to specify explicit 'directories' for import
70681
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70677
diff changeset
   811
of theory files. Directories cannot be shared by different sessions.
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70677
diff changeset
   812
(Recall that import of theories from other sessions works via
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70677
diff changeset
   813
session-qualified theory names, together with suitable 'sessions'
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70677
diff changeset
   814
declarations in the ROOT.)
70677
56d70f7ce4a4 more documentation;
wenzelm
parents: 70608
diff changeset
   815
70562
wenzelm
parents: 70525
diff changeset
   816
* Internal derivations record dependencies on oracles and other theorems
wenzelm
parents: 70525
diff changeset
   817
accurately, including the implicit type-class reasoning wrt. proven
wenzelm
parents: 70525
diff changeset
   818
class relations and type arities. In particular, the formal tagging with
wenzelm
parents: 70525
diff changeset
   819
"Pure.skip_proofs" of results stemming from "instance ... sorry" is now
wenzelm
parents: 70525
diff changeset
   820
propagated properly to theorems depending on such type instances.
wenzelm
parents: 70525
diff changeset
   821
wenzelm
parents: 70525
diff changeset
   822
* Command 'sorry' (oracle "Pure.skip_proofs") is more precise about the
wenzelm
parents: 70525
diff changeset
   823
actual proposition that is assumed in the goal and proof context. This
wenzelm
parents: 70525
diff changeset
   824
requires at least Proofterm.proofs = 1 to show up in theorem
wenzelm
parents: 70525
diff changeset
   825
dependencies.
wenzelm
parents: 70525
diff changeset
   826
wenzelm
parents: 70525
diff changeset
   827
* Command 'thm_oracles' prints all oracles used in given theorems,
wenzelm
parents: 70525
diff changeset
   828
covering the full graph of transitive dependencies.
wenzelm
parents: 70525
diff changeset
   829
70605
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70599
diff changeset
   830
* Command 'thm_deps' prints immediate theorem dependencies of the given
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70599
diff changeset
   831
facts. The former graph visualization has been discontinued, because it
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70599
diff changeset
   832
was hardly usable.
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70599
diff changeset
   833
71446
wenzelm
parents: 71438
diff changeset
   834
* Refined treatment of proof terms, including type-class proofs for
wenzelm
parents: 71438
diff changeset
   835
minor object-logics (FOL, FOLP, Sequents).
wenzelm
parents: 71438
diff changeset
   836
71448
wenzelm
parents: 71446
diff changeset
   837
* The inference kernel is now confined to one main module: structure
wenzelm
parents: 71446
diff changeset
   838
Thm, without the former circular dependency on structure Axclass.
wenzelm
parents: 71446
diff changeset
   839
71545
b0b16088ccf2 allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
wenzelm
parents: 71543
diff changeset
   840
* Mixfix annotations may use "' " (single quote followed by space) to
b0b16088ccf2 allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
wenzelm
parents: 71543
diff changeset
   841
separate delimiters (as documented in the isar-ref manual), without
71547
d350aabace23 proper escape for literal single quotes;
wenzelm
parents: 71545
diff changeset
   842
requiring an auxiliary empty block. A literal single quote needs to be
71551
wenzelm
parents: 71547
diff changeset
   843
escaped properly. Minor INCOMPATIBILITY.
71545
b0b16088ccf2 allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
wenzelm
parents: 71543
diff changeset
   844
70562
wenzelm
parents: 70525
diff changeset
   845
70522
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   846
*** Isar ***
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   847
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   848
* The proof method combinator (subproofs m) applies the method
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   849
expression m consecutively to each subgoal, constructing individual
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   850
subproofs internally. This impacts the internal construction of proof
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   851
terms: it makes a cascade of let-expressions within the derivation tree
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   852
and may thus improve scalability.
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   853
71427
wenzelm
parents: 71378
diff changeset
   854
* Attribute "trace_locales" activates tracing of locale instances during
wenzelm
parents: 71378
diff changeset
   855
roundup. It replaces the diagnostic command 'print_dependencies', which
wenzelm
parents: 71378
diff changeset
   856
has been discontinued.
70608
d997c7ba3305 Tracing of locale activation.
ballarin
parents: 70605
diff changeset
   857
70522
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   858
70683
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   859
*** Isabelle/jEdit Prover IDE ***
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   860
71543
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   861
* Prover IDE startup is now much faster, because theory dependencies are
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   862
no longer explored in advance. The overall session structure with its
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   863
declarations of 'directories' is sufficient to locate theory files. Thus
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   864
the "session focus" of option "isabelle jedit -S" has become obsolete
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   865
(likewise for "isabelle vscode_server -S"). Existing option "-R" is both
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   866
sufficient and more convenient to start editing a particular session.
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   867
71497
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71493
diff changeset
   868
* Actions isabelle.tooltip (CS+b) and isabelle.message (CS+m) display
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71493
diff changeset
   869
tooltip message popups, corresponding to mouse hovering with/without the
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71493
diff changeset
   870
CONTROL/COMMAND key pressed.
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71493
diff changeset
   871
71499
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71497
diff changeset
   872
* The following actions allow to navigate errors within the current
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71497
diff changeset
   873
document snapshot:
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71497
diff changeset
   874
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71497
diff changeset
   875
  isabelle.first-error (CS+a)
71505
ae3399b05e9b more documentation;
wenzelm
parents: 71499
diff changeset
   876
  isabelle.last-error (CS+z)
ae3399b05e9b more documentation;
wenzelm
parents: 71499
diff changeset
   877
  isabelle.next-error (CS+n)
ae3399b05e9b more documentation;
wenzelm
parents: 71499
diff changeset
   878
  isabelle.prev-error (CS+p)
71499
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71497
diff changeset
   879
71430
wenzelm
parents: 71429
diff changeset
   880
* Support more brackets: \<llangle> \<rrangle> (intended for implicit argument syntax).
wenzelm
parents: 71429
diff changeset
   881
71520
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71505
diff changeset
   882
* Action isabelle.jconsole (menu item Plugins / Isabelle / Java/VM
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71505
diff changeset
   883
Monitor) applies the jconsole tool on the running Isabelle/jEdit
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71505
diff changeset
   884
process. This allows to monitor resource usage etc.
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71505
diff changeset
   885
71543
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   886
* More adequate default font sizes for Linux on HD / UHD displays:
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   887
automatic font scaling is usually absent on Linux, in contrast to
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   888
Windows and macOS.
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   889
71575
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   890
* The default value for the jEdit property "view.antiAlias" (menu item
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   891
Utilities / Global Options / Text Area / Anti Aliased smooth text) is
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   892
now "subpixel HRGB", instead of former "standard". Especially on Linux
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   893
this often leads to faster text rendering, but can also cause problems
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   894
with odd color shades. An alternative is to switch back to "standard"
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   895
here, and set the following Java system property:
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   896
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   897
    isabelle jedit -Dsun.java2d.opengl=true
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   898
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   899
This can be made persistent via JEDIT_JAVA_OPTIONS in
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   900
$ISABELLE_HOME_USER/etc/settings. For the "Isabelle2020" desktop
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   901
application there is a corresponding options file in the same directory.
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   902
70683
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   903
71473
be84312a2d53 update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents: 71448
diff changeset
   904
*** Isabelle/VSCode Prover IDE ***
be84312a2d53 update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents: 71448
diff changeset
   905
71484
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   906
* Update of State and Preview panels to use new WebviewPanel API of
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   907
VSCode.
71473
be84312a2d53 update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents: 71448
diff changeset
   908
be84312a2d53 update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents: 71448
diff changeset
   909
70337
48609a6af1a0 removed relics of ASCII syntax for indexed big operators
haftmann
parents: 70300
diff changeset
   910
*** HOL ***
48609a6af1a0 removed relics of ASCII syntax for indexed big operators
haftmann
parents: 70300
diff changeset
   911
71427
wenzelm
parents: 71378
diff changeset
   912
* Improvements of the 'lift_bnf' command:
71264
0c454a5d125d NEWS, CONTRIBUTORS, and documentation
traytel
parents: 71259
diff changeset
   913
  - Add support for quotient types.
71427
wenzelm
parents: 71378
diff changeset
   914
  - Generate transfer rules for the lifted map/set/rel/pred constants
wenzelm
parents: 71378
diff changeset
   915
    (theorems "<type>.<constant>_transfer_raw").
71264
0c454a5d125d NEWS, CONTRIBUTORS, and documentation
traytel
parents: 71259
diff changeset
   916
70784
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
   917
* Term_XML.Encode/Decode.term uses compact representation of Const
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
   918
"typargs" from the given declaration environment. This also makes more
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
   919
sense for translations to lambda-calculi with explicit polymorphism.
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
   920
INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
   921
applications.
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
   922
70524
7783bece74b4 tuned whitespace;
wenzelm
parents: 70522
diff changeset
   923
* ASCII membership syntax concerning big operators for infimum and
71427
wenzelm
parents: 71378
diff changeset
   924
supremum has been discontinued. INCOMPATIBILITY.
70524
7783bece74b4 tuned whitespace;
wenzelm
parents: 70522
diff changeset
   925
71543
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   926
* Removed multiplicativity assumption from class
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   927
"normalization_semidom". Introduced various new intermediate classes
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   928
with the multiplicativity assumption; many theorem statements
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   929
(especially involving GCD/LCM) had to be adapted. This allows for a more
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   930
natural instantiation of the algebraic typeclasses for e.g. Gaussian
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   931
integers. INCOMPATIBILITY.
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   932
70524
7783bece74b4 tuned whitespace;
wenzelm
parents: 70522
diff changeset
   933
* Clear distinction between types for bits (False / True) and Z2 (0 /
71427
wenzelm
parents: 71378
diff changeset
   934
1): theory HOL-Library.Bit has been renamed accordingly.
wenzelm
parents: 71378
diff changeset
   935
INCOMPATIBILITY.
wenzelm
parents: 71378
diff changeset
   936
wenzelm
parents: 71378
diff changeset
   937
* Dynamic facts "algebra_split_simps" and "field_split_simps" correspond
70817
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70784
diff changeset
   938
to algebra_simps and field_simps but contain more aggressive rules
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70784
diff changeset
   939
potentially splitting goals; algebra_split_simps roughly replaces
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70784
diff changeset
   940
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: 70784
diff changeset
   941
INCOMPATIBILITY.
70524
7783bece74b4 tuned whitespace;
wenzelm
parents: 70522
diff changeset
   942
71428
wenzelm
parents: 71427
diff changeset
   943
* Theory HOL.Complete_Lattices:
wenzelm
parents: 71427
diff changeset
   944
renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf
wenzelm
parents: 71427
diff changeset
   945
71434
6c52b1d71f8b proper symbols;
wenzelm
parents: 71433
diff changeset
   946
* Theory HOL-Library.Monad_Syntax: infix operation "bind" (\<bind>)
70524
7783bece74b4 tuned whitespace;
wenzelm
parents: 70522
diff changeset
   947
associates to the left now as is customary.
7783bece74b4 tuned whitespace;
wenzelm
parents: 70522
diff changeset
   948
71259
09aee7f5b447 Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents: 71166
diff changeset
   949
* Theory HOL-Library.Ramsey: full finite Ramsey's theorem with
09aee7f5b447 Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents: 71166
diff changeset
   950
multiple colours and arbitrary exponents.
09aee7f5b447 Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents: 71166
diff changeset
   951
71484
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   952
* Session HOL-Proofs: build faster thanks to better treatment of proof
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   953
terms in Isabelle/Pure.
71147
wenzelm
parents: 71134
diff changeset
   954
71438
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   955
* Session HOL-Word: bitwise NOT-operator has proper prefix syntax. Minor
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   956
INCOMPATIBILITY.
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   957
71484
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   958
* Session HOL-Analysis: proof method "metric" implements a decision
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   959
procedure for simple linear statements in metric spaces.
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   960
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   961
* Session HOL-Complex_Analysis has been split off from HOL-Analysis.
71149
a7d1fb0c9e16 proper prefix syntax
haftmann
parents: 71147
diff changeset
   962
71150
9e7d40d67258 tuned whitespace
haftmann
parents: 71149
diff changeset
   963
70525
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   964
*** ML ***
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   965
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   966
* Theory construction may be forked internally, the operation
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   967
Theory.join_theory recovers a single result theory. See also the example
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   968
in theory "HOL-ex.Join_Theory".
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   969
70565
d0b75c59beca added ML antiquotation @{oracle_name};
wenzelm
parents: 70562
diff changeset
   970
* Antiquotation @{oracle_name} inlines a formally checked oracle name.
d0b75c59beca added ML antiquotation @{oracle_name};
wenzelm
parents: 70562
diff changeset
   971
71436
2e1b0ee920f5 updated for release;
wenzelm
parents: 71434
diff changeset
   972
* Minimal support for a soft-type system within the Isabelle logical
2e1b0ee920f5 updated for release;
wenzelm
parents: 71434
diff changeset
   973
framework (module Soft_Type_System).
2e1b0ee920f5 updated for release;
wenzelm
parents: 71434
diff changeset
   974
71750
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71662
diff changeset
   975
* Former Variable.auto_fixes has been replaced by slightly more general
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71662
diff changeset
   976
Proof_Context.augment: it is subject to an optional soft-type system of
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71662
diff changeset
   977
the underlying object-logic. Minor INCOMPATIBILITY.
71436
2e1b0ee920f5 updated for release;
wenzelm
parents: 71434
diff changeset
   978
71438
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   979
* More scalable Export.export using XML.tree to avoid premature string
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   980
allocations, with convenient shortcut XML.blob. Minor INCOMPATIBILITY.
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   981
71493
wenzelm
parents: 71485
diff changeset
   982
* Prover IDE support for the underlying Poly/ML compiler (not the basis
wenzelm
parents: 71485
diff changeset
   983
library). Open $ML_SOURCES/ROOT.ML in Isabelle/jEdit to browse the
wenzelm
parents: 71485
diff changeset
   984
implementation with full markup.
wenzelm
parents: 71485
diff changeset
   985
70525
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   986
70599
wenzelm
parents: 70565
diff changeset
   987
*** System ***
wenzelm
parents: 70565
diff changeset
   988
71433
wenzelm
parents: 71432
diff changeset
   989
* Standard rendering for more Isabelle symbols: \<llangle> \<rrangle> \<bbar> \<sqdot>
wenzelm
parents: 71432
diff changeset
   990
71378
820cf124dced added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents: 71343
diff changeset
   991
* The command-line tool "isabelle scala_project" creates a Gradle
820cf124dced added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents: 71343
diff changeset
   992
project configuration for Isabelle/Scala/jEdit, to support Scala IDEs
820cf124dced added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents: 71343
diff changeset
   993
such as IntelliJ IDEA.
820cf124dced added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents: 71343
diff changeset
   994
71293
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
   995
* The command-line tool "isabelle phabricator_setup" facilitates
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
   996
self-hosting of the Phabricator software-development platform, with
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
   997
support for Git, Mercurial, Subversion repositories. This helps to avoid
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
   998
monoculture and to escape the gravity of centralized version control by
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
   999
Github and/or Bitbucket. For further documentation, see chapter
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
  1000
"Phabricator server administration" in the "system" manual. A notable
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
  1001
example installation is https://isabelle-dev.sketis.net/.
71134
wenzelm
parents: 70957
diff changeset
  1002
71325
wenzelm
parents: 71293
diff changeset
  1003
* The command-line tool "isabelle hg_setup" simplifies the setup of
wenzelm
parents: 71293
diff changeset
  1004
Mercurial repositories, with hosting via Phabricator or SSH file server
wenzelm
parents: 71293
diff changeset
  1005
access.
wenzelm
parents: 71293
diff changeset
  1006
70686
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70683
diff changeset
  1007
* The command-line tool "isabelle imports" has been discontinued: strict
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70683
diff changeset
  1008
checking of session directories enforces session-qualified theory names
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70683
diff changeset
  1009
in applications -- users are responsible to specify session ROOT entries
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70683
diff changeset
  1010
properly.
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70683
diff changeset
  1011
71429
wenzelm
parents: 71428
diff changeset
  1012
* The command-line tool "isabelle dump" and its underlying
wenzelm
parents: 71428
diff changeset
  1013
Isabelle/Scala module isabelle.Dump has become more scalable, by
wenzelm
parents: 71428
diff changeset
  1014
splitting sessions and supporting a base logic image. Minor
wenzelm
parents: 71428
diff changeset
  1015
INCOMPATIBILITY in options and parameters.
wenzelm
parents: 71428
diff changeset
  1016
71750
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71662
diff changeset
  1017
* The command-line tool "isabelle build_docker" has been slightly
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71662
diff changeset
  1018
improved: it is now properly documented in the "system" manual.
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71662
diff changeset
  1019
71438
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
  1020
* Isabelle/Scala support for the Linux platform (Ubuntu): packages,
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
  1021
users, system services.
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
  1022
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
  1023
* Isabelle/Scala support for proof terms (with full type/term
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
  1024
information) in module isabelle.Term.
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
  1025
71662
263298eb68b2 more NEWS;
wenzelm
parents: 71581
diff changeset
  1026
* Isabelle/Scala: more scalable output of YXML files, e.g. relevant for
263298eb68b2 more NEWS;
wenzelm
parents: 71581
diff changeset
  1027
"isabelle dump".
263298eb68b2 more NEWS;
wenzelm
parents: 71581
diff changeset
  1028
70599
wenzelm
parents: 70565
diff changeset
  1029
* Theory export via Isabelle/Scala has been reworked. The former "fact"
wenzelm
parents: 70565
diff changeset
  1030
name space is now split into individual "thm" items: names are
wenzelm
parents: 70565
diff changeset
  1031
potentially indexed, such as "foo" for singleton facts, or "bar(1)",
wenzelm
parents: 70565
diff changeset
  1032
"bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now
wenzelm
parents: 70565
diff changeset
  1033
exported as well: this spans an overall dependency graph of internal
wenzelm
parents: 70565
diff changeset
  1034
inferences; it might help to reconstruct the formal structure of theory
71751
abf3e80bd815 tuned NEWS;
wenzelm
parents: 71750
diff changeset
  1035
libraries. See also the module isabelle.Export_Theory in Isabelle/Scala.
70599
wenzelm
parents: 70565
diff changeset
  1036
71484
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
  1037
* Theory export of structured specifications, based on internal
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
  1038
declarations of Spec_Rules by packages like 'definition', 'inductive',
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
  1039
'primrec', 'function'.
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
  1040
71428
wenzelm
parents: 71427
diff changeset
  1041
* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
wenzelm
parents: 71427
diff changeset
  1042
have been discontinued -- deprecated since Isabelle2018.
wenzelm
parents: 71427
diff changeset
  1043
71438
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
  1044
* More complete x86_64 platform support on macOS, notably Catalina where
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
  1045
old x86 has been discontinued.
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
  1046
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
  1047
* Update to GHC stack 2.1.3 with stackage lts-13.19/ghc-8.6.4.
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
  1048
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
  1049
* Update to OCaml Opam 2.0.6 (using ocaml 4.05.0 as before).
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
  1050
70265
a8238fd25541 back to post-release mode;
wenzelm
parents: 70260
diff changeset
  1051
70784
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
  1052
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1053
New in Isabelle2019 (June 2019)
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1054
-------------------------------
68683
d69127c6e80f back to post-release mode -- after fork point;
wenzelm
parents: 68681
diff changeset
  1055
69042
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
  1056
*** General ***
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
  1057
70032
0674c24afc5e updated for release;
wenzelm
parents: 70031
diff changeset
  1058
* The font collection "Isabelle DejaVu" is systematically derived from
0674c24afc5e updated for release;
wenzelm
parents: 70031
diff changeset
  1059
the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif"
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
  1060
and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
  1061
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: 69316
diff changeset
  1062
augmented by special Isabelle symbols, taken from the former
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
  1063
"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: 69316
diff changeset
  1064
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: 69316
diff changeset
  1065
INCOMPATIBILITY with display configuration expecting the old
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
  1066
"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: 69316
diff changeset
  1067
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
  1068
* The Isabelle fonts render "\<inverse>" properly as superscript "-1".
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
  1069
69042
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
  1070
* Old-style inner comments (* ... *) within the term language are no
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
  1071
longer supported (legacy feature in Isabelle2018).
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
  1072
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1073
* Old-style {* verbatim *} tokens are explicitly marked as legacy
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1074
feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1075
via "isabelle update_cartouches -t" (available since Isabelle2015).
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1076
70297
wenzelm
parents: 70281
diff changeset
  1077
* Infix operators that begin or end with a "*" are now parenthesized
wenzelm
parents: 70281
diff changeset
  1078
without additional spaces, e.g. "(*)" instead of "( * )". Minor
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1079
INCOMPATIBILITY.
69066
nipkow
parents: 69045
diff changeset
  1080
69580
6f755e3cd95d mixfix annotations may use cartouches;
wenzelm
parents: 69569
diff changeset
  1081
* Mixfix annotations may use cartouches instead of old-style double
69586
9171d1ce5a35 support for "isabelle update -u mixfix_cartouches";
wenzelm
parents: 69585
diff changeset
  1082
quotes, e.g. (infixl \<open>+\<close> 60). The command-line tool "isabelle update -u
9171d1ce5a35 support for "isabelle update -u mixfix_cartouches";
wenzelm
parents: 69585
diff changeset
  1083
mixfix_cartouches" allows to update existing theory sources
9171d1ce5a35 support for "isabelle update -u mixfix_cartouches";
wenzelm
parents: 69585
diff changeset
  1084
automatically.
69580
6f755e3cd95d mixfix annotations may use cartouches;
wenzelm
parents: 69569
diff changeset
  1085
69216
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: 69213
diff changeset
  1086
* 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: 69213
diff changeset
  1087
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: 69213
diff changeset
  1088
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: 69213
diff changeset
  1089
70057
0403b5127da1 documentation for generated files;
wenzelm
parents: 70032
diff changeset
  1090
* Commands 'generate_file', 'export_generated_files', and
0403b5127da1 documentation for generated files;
wenzelm
parents: 70032
diff changeset
  1091
'compile_generated_files' support a stateless (PIDE-conformant) model
0403b5127da1 documentation for generated files;
wenzelm
parents: 70032
diff changeset
  1092
for generated sources and compiled binaries of other languages. The
70060
wenzelm
parents: 70057
diff changeset
  1093
compilation process is managed in Isabelle/ML, and results exported to
70057
0403b5127da1 documentation for generated files;
wenzelm
parents: 70032
diff changeset
  1094
the session database for further use (e.g. with "isabelle export" or
0403b5127da1 documentation for generated files;
wenzelm
parents: 70032
diff changeset
  1095
"isabelle build -e").
0403b5127da1 documentation for generated files;
wenzelm
parents: 70032
diff changeset
  1096
69042
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
  1097
69189
wenzelm
parents: 69183
diff changeset
  1098
*** Isabelle/jEdit Prover IDE ***
wenzelm
parents: 69183
diff changeset
  1099
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1100
* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1101
DejaVu" collection by default, which provides uniform rendering quality
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1102
with the usual Isabelle symbols. Line spacing no longer needs to be
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1103
adjusted: properties for the old IsabelleText font had "Global Options /
70069
381035c03220 proper default;
wenzelm
parents: 70068
diff changeset
  1104
Text Area / Extra vertical line spacing (in pixels): -2", it now
381035c03220 proper default;
wenzelm
parents: 70068
diff changeset
  1105
defaults to 1, but 0 works as well.
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1106
69780
wenzelm
parents: 69778
diff changeset
  1107
* The jEdit File Browser is more prominent in the default GUI layout of
wenzelm
parents: 69778
diff changeset
  1108
Isabelle/jEdit: various virtual file-systems provide access to Isabelle
wenzelm
parents: 69778
diff changeset
  1109
resources, notably via "favorites:" (or "Edit Favorites").
wenzelm
parents: 69778
diff changeset
  1110
70061
5b75480f371a more NEWS;
wenzelm
parents: 70060
diff changeset
  1111
* Further markup and rendering for "plain text" (e.g. informal prose)
5b75480f371a more NEWS;
wenzelm
parents: 70060
diff changeset
  1112
and "raw text" (e.g. verbatim sources). This improves the visual
5b75480f371a more NEWS;
wenzelm
parents: 70060
diff changeset
  1113
appearance of formal comments inside the term language, or in general
5b75480f371a more NEWS;
wenzelm
parents: 70060
diff changeset
  1114
for repeated alternation of formal and informal text.
5b75480f371a more NEWS;
wenzelm
parents: 70060
diff changeset
  1115
69643
83f15deb2d36 added action "isabelle-export-browser";
wenzelm
parents: 69624
diff changeset
  1116
* Action "isabelle-export-browser" points the File Browser to the theory
69764
wenzelm
parents: 69755
diff changeset
  1117
exports of the current buffer, based on the "isabelle-export:" virtual
wenzelm
parents: 69755
diff changeset
  1118
file-system. The directory view needs to be reloaded manually to follow
wenzelm
parents: 69755
diff changeset
  1119
ongoing document processing.
wenzelm
parents: 69755
diff changeset
  1120
wenzelm
parents: 69755
diff changeset
  1121
* Action "isabelle-session-browser" points the File Browser to session
wenzelm
parents: 69755
diff changeset
  1122
information, based on the "isabelle-session:" virtual file-system. Its
wenzelm
parents: 69755
diff changeset
  1123
entries are structured according to chapter / session names, the open
wenzelm
parents: 69755
diff changeset
  1124
operation is redirected to the session ROOT file.
69643
83f15deb2d36 added action "isabelle-export-browser";
wenzelm
parents: 69624
diff changeset
  1125
69273
wenzelm
parents: 69269
diff changeset
  1126
* Support for user-defined file-formats via class isabelle.File_Format
69277
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69273
diff changeset
  1127
in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69273
diff changeset
  1128
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: 69273
diff changeset
  1129
Isabelle component).
69273
wenzelm
parents: 69269
diff changeset
  1130
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1131
* System option "jedit_text_overview" allows to disable the text
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1132
overview column.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1133
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69829
diff changeset
  1134
* 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: 69829
diff changeset
  1135
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: 69829
diff changeset
  1136
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: 69829
diff changeset
  1137
separated from option "-s".
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69829
diff changeset
  1138
70105
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
  1139
* The Isabelle/jEdit desktop application uses the same options as
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
  1140
"isabelle jedit" for its internal "isabelle build" process: the implicit
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
  1141
option "-o system_heaps" (or "-s") has been discontinued. This reduces
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
  1142
the potential for surprise wrt. command-line tools.
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
  1143
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
  1144
* The official download of the Isabelle/jEdit application already
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
  1145
contains heap images for Isabelle/HOL within its main directory: thus
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
  1146
the first encounter becomes faster and more robust (e.g. when run from a
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
  1147
read-only directory).
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
  1148
70072
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
  1149
* Isabelle DejaVu fonts are available with hinting by default, which is
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
  1150
relevant for low-resolution displays. This may be disabled via system
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
  1151
option "isabelle_fonts_hinted = false" in
70075
ee0b8e06b01c proper etc/preferences;
wenzelm
parents: 70072
diff changeset
  1152
$ISABELLE_HOME_USER/etc/preferences -- it occasionally yields better
70072
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
  1153
results.
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
  1154
70031
wenzelm
parents: 70026
diff changeset
  1155
* OpenJDK 11 has quite different font rendering, with better glyph
wenzelm
parents: 70026
diff changeset
  1156
shapes and improved sub-pixel anti-aliasing. In some situations results
70072
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
  1157
might be *worse* than Oracle Java 8, though -- a proper HiDPI / UHD
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
  1158
display is recommended.
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1159
70258
b4534d72dd22 more NEWS;
wenzelm
parents: 70237
diff changeset
  1160
* OpenJDK 11 supports GTK version 2.2 and 3 (according to system
b4534d72dd22 more NEWS;
wenzelm
parents: 70237
diff changeset
  1161
property jdk.gtk.version). The factory default is version 3, but
b4534d72dd22 more NEWS;
wenzelm
parents: 70237
diff changeset
  1162
ISABELLE_JAVA_SYSTEM_OPTIONS includes "-Djdk.gtk.version=2.2" to make
b4534d72dd22 more NEWS;
wenzelm
parents: 70237
diff changeset
  1163
this more conservative (as in Java 8). Depending on the GTK theme
b4534d72dd22 more NEWS;
wenzelm
parents: 70237
diff changeset
  1164
configuration, "-Djdk.gtk.version=3" might work better or worse.
b4534d72dd22 more NEWS;
wenzelm
parents: 70237
diff changeset
  1165
69189
wenzelm
parents: 69183
diff changeset
  1166
69962
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
  1167
*** Document preparation ***
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
  1168
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
  1169
* 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: 69960
diff changeset
  1170
are stripped from document output: the effect is to modify the semantic
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
  1171
presentation context or to emit markup to the PIDE document. Some
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
  1172
predefined markers are taken from the Dublin Core Metadata Initiative,
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
  1173
e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that
70281
wenzelm
parents: 70260
diff changeset
  1174
can be retrieved from the document database.
69962
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
  1175
70140
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
  1176
* Old-style command tags %name are re-interpreted as markers with
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
  1177
proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
  1178
before. Potential INCOMPATIBILITY: multiple markers are composed in
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
  1179
canonical order, resulting in a reversed list of tags in the
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
  1180
presentation context.
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
  1181
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
  1182
* Marker \<^marker>\<open>tag name\<close> does not apply to the proof of a top-level goal
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
  1183
statement by default (e.g. 'theorem', 'lemma'). This is a subtle change
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
  1184
of semantics wrt. old-style %name.
69962
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
  1185
70143
0cc7fe616924 more abbrevs;
wenzelm
parents: 70140
diff changeset
  1186
* In Isabelle/jEdit, the string "\tag" may be completed to a "\<^marker>\<open>tag \<close>"
0cc7fe616924 more abbrevs;
wenzelm
parents: 70140
diff changeset
  1187
template.
0cc7fe616924 more abbrevs;
wenzelm
parents: 70140
diff changeset
  1188
70121
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70106
diff changeset
  1189
* Document antiquotation option "cartouche" indicates if the output
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70106
diff changeset
  1190
should be delimited as cartouche; this takes precedence over the
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70106
diff changeset
  1191
analogous option "quotes".
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70106
diff changeset
  1192
70122
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: 70121
diff changeset
  1193
* 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: 70121
diff changeset
  1194
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: 70121
diff changeset
  1195
\<^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: 70121
diff changeset
  1196
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: 70121
diff changeset
  1197
"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: 70121
diff changeset
  1198
"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: 70121
diff changeset
  1199
69962
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
  1200
68879
wenzelm
parents: 68848
diff changeset
  1201
*** Isar ***
wenzelm
parents: 68848
diff changeset
  1202
69045
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
  1203
* Implicit cases goal1, goal2, goal3, etc. have been discontinued
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
  1204
(legacy feature since Isabelle2016).
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
  1205
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1206
* More robust treatment of structural errors: begin/end blocks take
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1207
precedence over goal/proof. This is particularly relevant for the
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1208
headless PIDE session and server.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1209
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1210
* Command keywords of kind thy_decl / thy_goal may be more specifically
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1211
fit into the traditional document model of "definition-statement-proof"
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1212
via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1213
69045
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
  1214
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
  1215
*** HOL ***
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
  1216
70009
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: 69962
diff changeset
  1217
* Command 'export_code' produces output as logical files within the
70011
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
  1218
theory context, as well as formal session exports that can be
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
  1219
materialized via command-line tools "isabelle export" or "isabelle build
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
  1220
-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
  1221
provides a virtual file-system "isabelle-export:" that can be explored
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
  1222
in the regular file-browser. A 'file_prefix' argument allows to specify
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
  1223
an explicit name prefix for the target file (SML, OCaml, Scala) or
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
  1224
directory (Haskell); the default is "export" with a consecutive number
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
  1225
within each theory.
70009
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: 69962
diff changeset
  1226
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: 69962
diff changeset
  1227
* 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: 69962
diff changeset
  1228
removed soon: writing to the physical file-system is not well-defined in
70011
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
  1229
a reactive/parallel application like Isabelle. The empty 'file' argument
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
  1230
has been discontinued already: it is superseded by the file-browser in
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
  1231
Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.
69624
e02bdf853a4c optional code export as theory export
haftmann
parents: 69609
diff changeset
  1232
70022
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70011
diff changeset
  1233
* Command 'code_reflect' no longer supports the 'file' argument: it has
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70011
diff changeset
  1234
been superseded by 'file_prefix' for stateless file management as in
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70011
diff changeset
  1235
'export_code'. Minor INCOMPATIBILITY.
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70011
diff changeset
  1236
69743
6a9a8ef5e4c6 prefer proper strings in OCaml
haftmann
parents: 69733
diff changeset
  1237
* Code generation for OCaml: proper strings are used for literals.
6a9a8ef5e4c6 prefer proper strings in OCaml
haftmann
parents: 69733
diff changeset
  1238
Minor INCOMPATIBILITY.
6a9a8ef5e4c6 prefer proper strings in OCaml
haftmann
parents: 69733
diff changeset
  1239
69926
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
  1240
* Code generation for OCaml: Zarith supersedes Nums as library for
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
  1241
proper integer arithmetic. The library is located via standard
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
  1242
invocations of "ocamlfind" (via ISABELLE_OCAMLFIND settings variable).
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
  1243
The environment provided by "isabelle ocaml_setup" already contains this
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
  1244
tool and the required packages. Minor INCOMPATIBILITY.
69906
55534affe445 migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents: 69903
diff changeset
  1245
69690
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69672
diff changeset
  1246
* Code generation for Haskell: code includes for Haskell must contain
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69672
diff changeset
  1247
proper module frame, nothing is added magically any longer.
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69672
diff changeset
  1248
INCOMPATIBILITY.
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69672
diff changeset
  1249
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1250
* Code generation: slightly more conventional syntax for 'code_stmts'
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1251
antiquotation. Minor INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1252
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1253
* Theory List: the precedence of the list_update operator has changed:
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1254
"f a [n := x]" now needs to be written "(f a)[n := x]".
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1255
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1256
* The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter> (not the corresponding binding operators)
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1257
now have the same precedence as any other prefix function symbol. Minor
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1258
INCOMPATIBILITY.
69861
62e47f06d22c avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents: 69854
diff changeset
  1259
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
  1260
* 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
  1261
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
  1262
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
  1263
SUPREMUM, UNION, INTER should now rarely occur in output and are just
70237
7e9269c188d6 more NEWS
haftmann
parents: 70215
diff changeset
  1264
retained as migration auxiliary. Abbreviations MINIMUM and MAXIMUM
7e9269c188d6 more NEWS
haftmann
parents: 70215
diff changeset
  1265
are gone INCOMPATIBILITY.
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
  1266
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1267
* The simplifier uses image_cong_simp as a congruence rule. The historic
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1268
and not really well-formed congruence rules INF_cong*, SUP_cong*, are
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1269
not used by default any longer. INCOMPATIBILITY; consider using declare
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1270
image_cong_simp [cong del] in extreme situations.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1271
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1272
* INF_image and SUP_image are no default simp rules any longer.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1273
INCOMPATIBILITY, prefer image_comp as simp rule if needed.
68938
a0b19a163f5e left-over rename from 3f9bb52082c4
haftmann
parents: 68883
diff changeset
  1274
69164
74f1b0f10b2b uniform naming of strong congruence rules
nipkow
parents: 69155
diff changeset
  1275
* Strong congruence rules (with =simp=> in the premises) for constant f
69546
27dae626822b prefer naming convention from datatype package for strong congruence rules
haftmann
parents: 69506
diff changeset
  1276
are now uniformly called f_cong_simp, in accordance with congruence
27dae626822b prefer naming convention from datatype package for strong congruence rules
haftmann
parents: 69506
diff changeset
  1277
rules produced for mappers by the datatype package. INCOMPATIBILITY.
69164
74f1b0f10b2b uniform naming of strong congruence rules
nipkow
parents: 69155
diff changeset
  1278
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1279
* Retired lemma card_Union_image; use the simpler card_UN_disjoint
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1280
instead. INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1281
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1282
* Facts sum_mset.commute and prod_mset.commute have been renamed to
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1283
sum_mset.swap and prod_mset.swap, similarly to sum.swap and prod.swap.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1284
INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1285
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1286
* ML structure Inductive: slightly more conventional naming schema.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1287
Minor INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1288
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1289
* ML: Various _global variants of specification tools have been removed.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1290
Minor INCOMPATIBILITY, prefer combinators
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1291
Named_Target.theory_map[_result] to lift specifications to the global
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1292
theory level.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1293
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1294
* Theory HOL-Library.Simps_Case_Conv: 'case_of_simps' now supports
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1295
overlapping and non-exhaustive patterns and handles arbitrarily nested
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1296
patterns. It uses on the same algorithm as HOL-Library.Code_Lazy, which
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1297
assumes sequential left-to-right pattern matching. The generated
69568
de09a7261120 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents: 69506
diff changeset
  1298
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: 69506
diff changeset
  1299
INCOMPATIBILITY.
de09a7261120 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents: 69506
diff changeset
  1300
70297
wenzelm
parents: 70281
diff changeset
  1301
* Theory HOL-Library.Multiset: the \<Union># operator now has the same
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1302
precedence as any other prefix function symbol.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1303
70080
traytel
parents: 70075
diff changeset
  1304
* Theory HOL-Library.Cardinal_Notations has been discontinued in favor
70168
e79bbf86a984 tuned for release;
wenzelm
parents: 70164
diff changeset
  1305
of the bundle cardinal_syntax (available in theory Main). Minor
e79bbf86a984 tuned for release;
wenzelm
parents: 70164
diff changeset
  1306
INCOMPATIBILITY.
70080
traytel
parents: 70075
diff changeset
  1307
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1308
* Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring,
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1309
used for computing powers in class "monoid_mult" and modular
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1310
exponentiation.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1311
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1312
* Session HOL-Computational_Algebra: Formal Laurent series and overhaul
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1313
of Formal power series.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1314
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1315
* Session HOL-Number_Theory: More material on residue rings in
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1316
Carmichael's function, primitive roots, more properties for "ord".
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1317
70125
b601c2c87076 type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents: 70106
diff changeset
  1318
* 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: 70106
diff changeset
  1319
at the level of abstract topological spaces.
b601c2c87076 type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents: 70106
diff changeset
  1320
70164
1f163f772da3 Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)
paulson <lp15@cam.ac.uk>
parents: 70143
diff changeset
  1321
* Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
70215
8371a25ca177 Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents: 70175
diff changeset
  1322
 algebraic closure of a field by de Vilhena and Baillon.
70032
0674c24afc5e updated for release;
wenzelm
parents: 70031
diff changeset
  1323
70168
e79bbf86a984 tuned for release;
wenzelm
parents: 70164
diff changeset
  1324
* Session HOL-Homology has been added. It is a port of HOL Light's
e79bbf86a984 tuned for release;
wenzelm
parents: 70164
diff changeset
  1325
homology library, with new proofs of "invariance of domain" and related
e79bbf86a984 tuned for release;
wenzelm
parents: 70164
diff changeset
  1326
results.
e79bbf86a984 tuned for release;
wenzelm
parents: 70164
diff changeset
  1327
69099
d44cb8a3e5e0 HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents: 69094
diff changeset
  1328
* 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: 69094
diff changeset
  1329
file-system, but exported to the session database. Results may be
70026
6ae9505d693a more convenient export;
wenzelm
parents: 70023
diff changeset
  1330
retrieved via "isabelle build -e HOL-SPARK-Examples" on the
6ae9505d693a more convenient export;
wenzelm
parents: 70023
diff changeset
  1331
command-line.
69099
d44cb8a3e5e0 HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents: 69094
diff changeset
  1332
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1333
* Sledgehammer:
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1334
  - The URL for SystemOnTPTP, which is used by remote provers, has been
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1335
    updated.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1336
  - The machine-learning-based filter MaSh has been optimized to take
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1337
    less time (in most cases).
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1338
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1339
* SMT: reconstruction is now possible using the SMT solver veriT.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1340
70174
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70168
diff changeset
  1341
* Session HOL-Word:
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70168
diff changeset
  1342
  * New theory More_Word as comprehensive entrance point.
70175
85fb1a585f52 eliminated type class
haftmann
parents: 70174
diff changeset
  1343
  * Merged type class bitss into type class bits.
70174
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70168
diff changeset
  1344
  INCOMPATIBILITY.
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70168
diff changeset
  1345
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
  1346
68803
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
  1347
*** ML ***
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
  1348
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1349
* Command 'generate_file' allows to produce sources for other languages,
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1350
with antiquotations in the Isabelle context (only the control-cartouche
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1351
form). The default "cartouche" antiquotation evaluates an ML expression
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1352
of type string and inlines the result as a string literal of the target
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1353
language. For example, this works for Haskell as follows:
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1354
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1355
  generate_file "Pure.hs" = \<open>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1356
  module Isabelle.Pure where
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1357
    allConst, impConst, eqConst :: String
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1358
    allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1359
    impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1360
    eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1361
  \<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1362
70082
4f936de6d9b8 tuned -- prefer Isar command 'compile_generated_files';
wenzelm
parents: 70080
diff changeset
  1363
See also commands 'export_generated_files' and 'compile_generated_files'
4f936de6d9b8 tuned -- prefer Isar command 'compile_generated_files';
wenzelm
parents: 70080
diff changeset
  1364
to use the results.
68803
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
  1365
70260
22cfcfcadd8b more documentation;
wenzelm
parents: 70258
diff changeset
  1366
* ML evaluation (notably via command 'ML' or 'ML_file') is subject to
68824
7414ce0256e1 some NEWS (instead of proper documentation);
wenzelm
parents: 68803
diff changeset
  1367
option ML_environment to select a named environment, such as "Isabelle"
70260
22cfcfcadd8b more documentation;
wenzelm
parents: 70258
diff changeset
  1368
for Isabelle/ML, or "SML" for official Standard ML.
68803
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
  1369
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69377
diff changeset
  1370
* 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: 69377
diff changeset
  1371
underlying theory, i.e. the directory of the theory file.
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69377
diff changeset
  1372
69470
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69381
diff changeset
  1373
* ML antiquotation @{verbatim} inlines its argument as string literal,
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69381
diff changeset
  1374
preserving newlines literally. The short form \<^verbatim>\<open>abc\<close> is particularly
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69381
diff changeset
  1375
useful.
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69381
diff changeset
  1376
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1377
* Local_Theory.reset is no longer available in user space. Regular
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1378
definitional packages should use balanced blocks of
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1379
Local_Theory.open_target versus Local_Theory.close_target instead, or
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1380
the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1381
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1382
* Original PolyML.pointerEq is retained as a convenience for tools that
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1383
don't use Isabelle/ML (where this is called "pointer_eq").
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69377
diff changeset
  1384
69282
94fa3376ba33 added ML antiquotation @{master_dir};
wenzelm
parents: 69277
diff changeset
  1385
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
  1386
*** System ***
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
  1387
70031
wenzelm
parents: 70026
diff changeset
  1388
* Update to OpenJDK 11: the current long-term support version of Java.
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1389
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1390
* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1391
the full overhead of 64-bit values everywhere. This special x86_64_32
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1392
mode provides up to 16GB ML heap, while program code and stacks are
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1393
allocated elsewhere. Thus approx. 5 times more memory is available for
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1394
applications compared to old x86 mode (which is no longer used by
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1395
Isabelle). The switch to the x86_64 CPU architecture also avoids
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1396
compatibility problems with Linux and macOS, where 32-bit applications
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1397
are gradually phased out.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1398
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1399
* System option "checkpoint" has been discontinued: obsolete thanks to
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1400
improved memory management in Poly/ML.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1401
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
  1402
* System option "system_heaps" determines where to store the session
69854
cc0b3e177b49 system option "system_heaps" supersedes various