NEWS
author haftmann
Wed, 12 May 2021 17:05:28 +0000
changeset 73937 3708884bfa8a
parent 73928 7404f2e1d092
child 73938 78044b2f001c
permissions -rw-r--r--
obsolete
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
57491
9eedaafc05c8 tuned grammar and spelling (cf. 0cf15843b82f);
wenzelm
parents: 57476
diff changeset
     1
Isabelle NEWS -- history of user-relevant changes
9eedaafc05c8 tuned grammar and spelling (cf. 0cf15843b82f);
wenzelm
parents: 57476
diff changeset
     2
=================================================
2553
ed941505cab7 Isabelle NEWS -- history of user-visible changes;
wenzelm
parents:
diff changeset
     3
62114
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents: 62111
diff changeset
     4
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
60007
wenzelm
parents: 59998
diff changeset
     5
73520
haftmann
parents: 73518
diff changeset
     6
haftmann
parents: 73518
diff changeset
     7
New in this Isabelle version
haftmann
parents: 73518
diff changeset
     8
----------------------------
haftmann
parents: 73518
diff changeset
     9
73635
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73626
diff changeset
    10
*** General ***
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73626
diff changeset
    11
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73626
diff changeset
    12
* Timeouts for Isabelle/ML tools are subject to system option
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73626
diff changeset
    13
"timeout_scale" --- this already used for the overall session build
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73626
diff changeset
    14
process before, and allows to adapt to slow machines. The underlying
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73626
diff changeset
    15
Timeout.apply in Isabelle/ML treats an original timeout specification 0
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73626
diff changeset
    16
as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73626
diff changeset
    17
in boundary cases.
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73626
diff changeset
    18
73688
e92f2e44e4d8 removed spurious references to perl / libwww-perl;
wenzelm
parents: 73663
diff changeset
    19
* Remote provers from SystemOnTPTP (notably for Sledgehammer) are now
e92f2e44e4d8 removed spurious references to perl / libwww-perl;
wenzelm
parents: 73663
diff changeset
    20
managed via Isabelle/Scala instead of perl; the dependency on
e92f2e44e4d8 removed spurious references to perl / libwww-perl;
wenzelm
parents: 73663
diff changeset
    21
libwww-perl has been eliminated (notably on Linux). Rare
e92f2e44e4d8 removed spurious references to perl / libwww-perl;
wenzelm
parents: 73663
diff changeset
    22
INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties
e92f2e44e4d8 removed spurious references to perl / libwww-perl;
wenzelm
parents: 73663
diff changeset
    23
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: 73663
diff changeset
    24
73699
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 73688
diff changeset
    25
* 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: 73688
diff changeset
    26
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: 73688
diff changeset
    27
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: 73688
diff changeset
    28
73635
3b5196dac4c8 clarified timeouts in Isabelle/ML;
wenzelm
parents: 73626
diff changeset
    29
73872
b0ea03e837b1 support nested cases;
wenzelm
parents: 73851
diff changeset
    30
*** Isabelle/jEdit Prover IDE ***
b0ea03e837b1 support nested cases;
wenzelm
parents: 73851
diff changeset
    31
b0ea03e837b1 support nested cases;
wenzelm
parents: 73851
diff changeset
    32
* More robust 'proof' outline for method "induct": support nested cases.
b0ea03e837b1 support nested cases;
wenzelm
parents: 73851
diff changeset
    33
b0ea03e837b1 support nested cases;
wenzelm
parents: 73851
diff changeset
    34
73656
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 73642
diff changeset
    35
*** Document preparation ***
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 73642
diff changeset
    36
73661
wenzelm
parents: 73656
diff changeset
    37
* Improved LaTeX typesetting of \<open>...\<close> using \guilsinglleft ...
wenzelm
parents: 73656
diff changeset
    38
\guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
73656
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 73642
diff changeset
    39
(which is now also the default in "isabelle mkroot").
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 73642
diff changeset
    40
73851
aece5cc9efb7 simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm
parents: 73842
diff changeset
    41
* Simplified typesetting of \<guillemotleft>...\<guillemotright> using \guillemotleft ...
aece5cc9efb7 simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm
parents: 73842
diff changeset
    42
\guillemotright from \usepackage[T1]{fontenc} --- \usepackage{babel} is
aece5cc9efb7 simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm
parents: 73842
diff changeset
    43
no longer required.
aece5cc9efb7 simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm
parents: 73842
diff changeset
    44
73656
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 73642
diff changeset
    45
73518
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73500
diff changeset
    46
*** HOL ***
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73500
diff changeset
    47
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73500
diff changeset
    48
* Theory Multiset: dedicated predicate "multiset" is gone, use
e2d03448d5b5 get rid of traditional predicate
haftmann
parents: 73500
diff changeset
    49
explict expression instead.  Minor INCOMPATIBILITY.
64603
a7f5e59378f7 tuned whitespace;
wenzelm
parents: 64602
diff changeset
    50
73641
716d256259d5 consolidated names
haftmann
parents: 73635
diff changeset
    51
* Theory Multiset: consolidated abbreviations Mempty, Melem, not_Melem
716d256259d5 consolidated names
haftmann
parents: 73635
diff changeset
    52
to empty_mset, member_mset, not_member_mset respectively.  Minor
716d256259d5 consolidated names
haftmann
parents: 73635
diff changeset
    53
INCOMPATIBILITY.
716d256259d5 consolidated names
haftmann
parents: 73635
diff changeset
    54
716d256259d5 consolidated names
haftmann
parents: 73635
diff changeset
    55
* Theory Multiset: consolidated operation and fact names:
716d256259d5 consolidated names
haftmann
parents: 73635
diff changeset
    56
    inf_subset_mset ~> inter_mset
716d256259d5 consolidated names
haftmann
parents: 73635
diff changeset
    57
    sup_subset_mset ~> union_mset
716d256259d5 consolidated names
haftmann
parents: 73635
diff changeset
    58
    multiset_inter_def ~> inter_mset_def
716d256259d5 consolidated names
haftmann
parents: 73635
diff changeset
    59
    sup_subset_mset_def ~> union_mset_def
716d256259d5 consolidated names
haftmann
parents: 73635
diff changeset
    60
    multiset_inter_count ~> count_inter_mset
716d256259d5 consolidated names
haftmann
parents: 73635
diff changeset
    61
    sup_subset_mset_count ~> count_union_mset
716d256259d5 consolidated names
haftmann
parents: 73635
diff changeset
    62
73642
2e6b2134956e follow corresponding precedence on sets
haftmann
parents: 73641
diff changeset
    63
* Theory Multiset: syntax precendence for membership operations has been
2e6b2134956e follow corresponding precedence on sets
haftmann
parents: 73641
diff changeset
    64
adjusted to match the corresponding precendences on sets.  Rare
2e6b2134956e follow corresponding precedence on sets
haftmann
parents: 73641
diff changeset
    65
INCOMPATIBILITY.
2e6b2134956e follow corresponding precedence on sets
haftmann
parents: 73641
diff changeset
    66
73500
f6bb31879698 HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents: 73493
diff changeset
    67
* HOL-Analysis/HOL-Probability: indexed products of discrete
f6bb31879698 HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents: 73493
diff changeset
    68
distributions, negative binomial distribution, Hoeffding's inequality,
f6bb31879698 HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents: 73493
diff changeset
    69
Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, and some
f6bb31879698 HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents: 73493
diff changeset
    70
more small lemmas. Some theorems that were stated awkwardly before were
f6bb31879698 HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents: 73493
diff changeset
    71
corrected. Minor INCOMPATIBILITY.
f6bb31879698 HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents: 73493
diff changeset
    72
73663
1f1366966296 avoid name clash
haftmann
parents: 73661
diff changeset
    73
* Theorems "antisym" and "eq_iff" in class "order" have been renamed to
1f1366966296 avoid name clash
haftmann
parents: 73661
diff changeset
    74
"order.antisym" and "order.eq_iff", to coexist locally with "antisym"
1f1366966296 avoid name clash
haftmann
parents: 73661
diff changeset
    75
and "eq_iff" from locale "ordering".  INCOMPATIBILITY: significant
1f1366966296 avoid name clash
haftmann
parents: 73661
diff changeset
    76
potential for change can be avoided if interpretations of type class
1f1366966296 avoid name clash
haftmann
parents: 73661
diff changeset
    77
"order" are replaced or augmented by interpretations of locale
1f1366966296 avoid name clash
haftmann
parents: 73661
diff changeset
    78
"ordering".
1f1366966296 avoid name clash
haftmann
parents: 73661
diff changeset
    79
73722
ee1c4962671c more lemmas
haftmann
parents: 73720
diff changeset
    80
* Theorem "swap_def" now is always qualified as "Fun.swap_def".  Minor
ee1c4962671c more lemmas
haftmann
parents: 73720
diff changeset
    81
INCOMPATIBILITY; note that for most applications less elementary lemmas
ee1c4962671c more lemmas
haftmann
parents: 73720
diff changeset
    82
exists.
73663
1f1366966296 avoid name clash
haftmann
parents: 73661
diff changeset
    83
73732
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73726
diff changeset
    84
* Dedicated session HOL-Combinatorics.  INCOMPATIBILITY: theories
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73726
diff changeset
    85
"Permutations", "List_Permutation" (formerly "Permutation"), "Stirling",
73878
4dc3baf45d6a more appropriate location
haftmann
parents: 73872
diff changeset
    86
"Multiset_Permutations", "Perm" have been moved there from session
73937
3708884bfa8a obsolete
haftmann
parents: 73928
diff changeset
    87
HOL-Library.
73732
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73726
diff changeset
    88
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73726
diff changeset
    89
* Theory "Permutation" in HOL-Library has been renamed to the more
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73726
diff changeset
    90
specific "List_Permutation".  Note that most notions from that
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73726
diff changeset
    91
theory are already present in theory "Permutations".  INCOMPATIBILITY.
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73726
diff changeset
    92
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73726
diff changeset
    93
* Lemma "permutes_induct" has been given stronger
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73726
diff changeset
    94
hypotheses and named premises.  INCOMPATIBILITY.
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73726
diff changeset
    95
73904
1bd3463e30b8 more elementary swap
haftmann
parents: 73879
diff changeset
    96
* Theory "Transposition" in HOL-Combinatorics provides elementary
1bd3463e30b8 more elementary swap
haftmann
parents: 73879
diff changeset
    97
swap operation "transpose".
1bd3463e30b8 more elementary swap
haftmann
parents: 73879
diff changeset
    98
1bd3463e30b8 more elementary swap
haftmann
parents: 73879
diff changeset
    99
* Combinator "Fun.swap" resolved into a mere input abbreviation
1bd3463e30b8 more elementary swap
haftmann
parents: 73879
diff changeset
   100
in separate theory "Transposition" in HOL-Combinatorics.
1bd3463e30b8 more elementary swap
haftmann
parents: 73879
diff changeset
   101
INCOMPATIBILITY.
73879
5020054b3a16 tuned theory structure
haftmann
parents: 73878
diff changeset
   102
73500
f6bb31879698 HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents: 73493
diff changeset
   103
73535
wenzelm
parents: 73520
diff changeset
   104
*** ML ***
wenzelm
parents: 73520
diff changeset
   105
73806
2f6855142a8c support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents: 73736
diff changeset
   106
* 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: 73736
diff changeset
   107
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: 73736
diff changeset
   108
modify application of a function.
2f6855142a8c support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents: 73736
diff changeset
   109
73842
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73806
diff changeset
   110
* ML antiquotations for conditional ML text:
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73806
diff changeset
   111
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73806
diff changeset
   112
    \<^if_linux>\<open>...\<close>
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73806
diff changeset
   113
    \<^if_macos>\<open>...\<close>
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73806
diff changeset
   114
    \<^if_windows>\<open>...\<close>
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73806
diff changeset
   115
    \<^if_unix>\<open>...\<close>
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73806
diff changeset
   116
73535
wenzelm
parents: 73520
diff changeset
   117
* External bash processes are always managed by Isabelle/Scala, in
wenzelm
parents: 73520
diff changeset
   118
contrast to Isabelle2021 where this was only done for macOS on Apple
wenzelm
parents: 73520
diff changeset
   119
Silicon.
wenzelm
parents: 73520
diff changeset
   120
wenzelm
parents: 73520
diff changeset
   121
The main Isabelle/ML interface is Isabelle_System.bash_process with
wenzelm
parents: 73520
diff changeset
   122
result type Process_Result.T (resembling class Process_Result in Scala);
wenzelm
parents: 73520
diff changeset
   123
derived operations Isabelle_System.bash and Isabelle_System.bash_output
wenzelm
parents: 73520
diff changeset
   124
provide similar functionality as before. Rare INCOMPATIBILITY due to
wenzelm
parents: 73520
diff changeset
   125
subtle semantic differences:
wenzelm
parents: 73520
diff changeset
   126
wenzelm
parents: 73520
diff changeset
   127
  - Processes invoked from Isabelle/ML actually run in the context of
wenzelm
parents: 73520
diff changeset
   128
    the Java VM of Isabelle/Scala. The settings environment and current
wenzelm
parents: 73520
diff changeset
   129
    working directory are usually the same on both sides, but there can be
wenzelm
parents: 73520
diff changeset
   130
    subtle corner cases (e.g. unexpected uses of "cd" or "putenv" in ML).
wenzelm
parents: 73520
diff changeset
   131
wenzelm
parents: 73520
diff changeset
   132
  - Output via stdout and stderr is line-oriented: Unix vs. Windows
wenzelm
parents: 73520
diff changeset
   133
    line-endings are normalized towards Unix; presence or absence of a
wenzelm
parents: 73520
diff changeset
   134
    final newline is irrelevant. The original lines are available as
wenzelm
parents: 73520
diff changeset
   135
    Process_Result.out_lines/err_lines; the concatenated versions
wenzelm
parents: 73520
diff changeset
   136
    Process_Result.out/err *omit* a trailing newline (using
wenzelm
parents: 73520
diff changeset
   137
    Library.trim_line, which was occasional seen in applications before,
wenzelm
parents: 73520
diff changeset
   138
    but is no longer necessary).
wenzelm
parents: 73520
diff changeset
   139
wenzelm
parents: 73520
diff changeset
   140
  - Output needs to be plain text encoded in UTF-8: Isabelle/Scala
wenzelm
parents: 73520
diff changeset
   141
    recodes it temporarily as UTF-16. This works for well-formed Unicode
wenzelm
parents: 73520
diff changeset
   142
    text, but not for arbitrary byte strings. In such cases, the bash
wenzelm
parents: 73520
diff changeset
   143
    script should write tempory files, managed by Isabelle/ML operations
wenzelm
parents: 73520
diff changeset
   144
    like Isabelle_System.with_tmp_file to create a file name and
wenzelm
parents: 73520
diff changeset
   145
    File.read to retrieve its content.
wenzelm
parents: 73520
diff changeset
   146
73546
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73545
diff changeset
   147
  - Just like any other Scala function invoked from ML,
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73545
diff changeset
   148
    Isabelle_System.bash_process requires a proper PIDE session context.
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73545
diff changeset
   149
    This could be a regular batch session (e.g. "isabelle build"), a
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73545
diff changeset
   150
    PIDE editor session (e.g. "isabelle jedit"), or headless PIDE (e.g.
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73545
diff changeset
   151
    "isabelle dump" or "isabelle server"). Note that old "isabelle
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73545
diff changeset
   152
    console" or raw "isabelle process" don't have that.
637e3e85cd6f more on Isabelle_System.bash;
wenzelm
parents: 73545
diff changeset
   153
73535
wenzelm
parents: 73520
diff changeset
   154
New Process_Result.timing works as in Isabelle/Scala, based on direct
wenzelm
parents: 73520
diff changeset
   155
measurements of the bash_process wrapper in C: elapsed time is always
wenzelm
parents: 73520
diff changeset
   156
available, CPU time is only available on Linux and macOS, GC time is
wenzelm
parents: 73520
diff changeset
   157
unavailable.
wenzelm
parents: 73520
diff changeset
   158
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73546
diff changeset
   159
* Likewise, the following Isabelle/ML system operations are run in the
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73546
diff changeset
   160
context of Isabelle/Scala:
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73546
diff changeset
   161
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73546
diff changeset
   162
  - Isabelle_System.make_directory
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73546
diff changeset
   163
  - Isabelle_System.copy_dir
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73546
diff changeset
   164
  - Isabelle_System.copy_file
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73546
diff changeset
   165
  - Isabelle_System.copy_base_file
73571
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73570
diff changeset
   166
  - Isabelle_System.rm_tree
73570
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73569
diff changeset
   167
  - Isabelle_System.download
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73546
diff changeset
   168
73535
wenzelm
parents: 73520
diff changeset
   169
73735
0e880b793db1 support repository archives (without full .hg directory);
wenzelm
parents: 73732
diff changeset
   170
*** System ***
0e880b793db1 support repository archives (without full .hg directory);
wenzelm
parents: 73732
diff changeset
   171
0e880b793db1 support repository archives (without full .hg directory);
wenzelm
parents: 73732
diff changeset
   172
* Command-line tool "isabelle version" supports repository archives
73736
92db3e31fae3 clarified output;
wenzelm
parents: 73735
diff changeset
   173
(without full .hg directory). More options.
73735
0e880b793db1 support repository archives (without full .hg directory);
wenzelm
parents: 73732
diff changeset
   174
73928
7404f2e1d092 clarified platforms;
wenzelm
parents: 73904
diff changeset
   175
* Obsolete settings variable ISABELLE_PLATFORM32 has been discontinued.
7404f2e1d092 clarified platforms;
wenzelm
parents: 73904
diff changeset
   176
Note that only Windows supports old 32 bit executables, via settings
7404f2e1d092 clarified platforms;
wenzelm
parents: 73904
diff changeset
   177
variable ISABELLE_WINDOWS_PLATFORM32. Everything else should be
7404f2e1d092 clarified platforms;
wenzelm
parents: 73904
diff changeset
   178
ISABELLE_PLATFORM64 (generic Posix) or ISABELLE_WINDOWS_PLATFORM64
7404f2e1d092 clarified platforms;
wenzelm
parents: 73904
diff changeset
   179
(native Windows) or ISABELLE_APPLE_PLATFORM64 (Apple Silicon).
7404f2e1d092 clarified platforms;
wenzelm
parents: 73904
diff changeset
   180
73735
0e880b793db1 support repository archives (without full .hg directory);
wenzelm
parents: 73732
diff changeset
   181
73535
wenzelm
parents: 73520
diff changeset
   182
73212
31ff3c962937 misc tuning for release;
wenzelm
parents: 73211
diff changeset
   183
New in Isabelle2021 (February 2021)
31ff3c962937 misc tuning for release;
wenzelm
parents: 73211
diff changeset
   184
-----------------------------------
71772
61ba52af28e3 back to post-release mode;
wenzelm
parents: 71765
diff changeset
   185
72464
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72439
diff changeset
   186
*** General ***
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72439
diff changeset
   187
73440
c0d6d57a9a31 more NEWS;
wenzelm
parents: 73419
diff changeset
   188
* On macOS, the IsabelleXYZ.app directory layout now follows the other
c0d6d57a9a31 more NEWS;
wenzelm
parents: 73419
diff changeset
   189
platforms, without indirection via Contents/Resources/. INCOMPATIBILITY,
c0d6d57a9a31 more NEWS;
wenzelm
parents: 73419
diff changeset
   190
use e.g. IsabelleXYZ.app/bin/isabelle instead of former
c0d6d57a9a31 more NEWS;
wenzelm
parents: 73419
diff changeset
   191
IsabelleXYZ.app/Isabelle/bin/isabelle or
c0d6d57a9a31 more NEWS;
wenzelm
parents: 73419
diff changeset
   192
IsabelleXYZ.app/Isabelle/Contents/Resources/IsabelleXYZ/bin/isabelle.
c0d6d57a9a31 more NEWS;
wenzelm
parents: 73419
diff changeset
   193
73320
824815ec52aa more NEWS;
wenzelm
parents: 73294
diff changeset
   194
* HTML presentation uses rich markup produced by Isabelle/PIDE,
824815ec52aa more NEWS;
wenzelm
parents: 73294
diff changeset
   195
resulting in more colors and links.
824815ec52aa more NEWS;
wenzelm
parents: 73294
diff changeset
   196
824815ec52aa more NEWS;
wenzelm
parents: 73294
diff changeset
   197
* HTML presentation includes auxiliary files (e.g. ML) for each theory.
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   198
72464
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72439
diff changeset
   199
* 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: 72439
diff changeset
   200
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: 72439
diff changeset
   201
Rare INCOMPATIBILITY.
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72439
diff changeset
   202
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   203
* Theory_Data extend operation is obsolete and needs to be the identity
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   204
function; merge should be conservative and not reset to the empty value.
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   205
Subtle INCOMPATIBILITY and change of semantics (due to
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   206
Theory.join_theory from Isabelle2020). Special extend/merge behaviour at
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   207
the begin of a new theory can be achieved via Theory.at_begin.
73237
cdcd2785db94 more NEWS;
wenzelm
parents: 73228
diff changeset
   208
72464
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72439
diff changeset
   209
72160
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 72155
diff changeset
   210
*** Isabelle/jEdit Prover IDE ***
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 72155
diff changeset
   211
73360
b84887a67cc6 clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents: 73356
diff changeset
   212
* Improved GUI look-and-feel: the portable and scalable "FlatLaf Light"
b84887a67cc6 clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents: 73356
diff changeset
   213
is used by default on all platforms (appearance similar to IntelliJ
b84887a67cc6 clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents: 73356
diff changeset
   214
IDEA).
73356
efc58b56a6c7 clarified default L&F;
wenzelm
parents: 73352
diff changeset
   215
73186
9329abcdd651 improved markup for theory header imports;
wenzelm
parents: 73172
diff changeset
   216
* Improved markup for theory header imports: hyperlinks for theory files
9329abcdd651 improved markup for theory header imports;
wenzelm
parents: 73172
diff changeset
   217
work without formal checking of content.
9329abcdd651 improved markup for theory header imports;
wenzelm
parents: 73172
diff changeset
   218
73190
ac6457a70db5 download auxiliary files via "curl";
wenzelm
parents: 73186
diff changeset
   219
* The prover process can download auxiliary files (e.g. 'ML_file') for
ac6457a70db5 download auxiliary files via "curl";
wenzelm
parents: 73186
diff changeset
   220
theories with remote URL. This requires the external "curl" program.
ac6457a70db5 download auxiliary files via "curl";
wenzelm
parents: 73186
diff changeset
   221
73170
0cc298e29aff added action isabelle.goto-entity to follow links in a narrow formal sense;
wenzelm
parents: 73116
diff changeset
   222
* 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: 73116
diff changeset
   223
of the formal entity at the caret position.
0cc298e29aff added action isabelle.goto-entity to follow links in a narrow formal sense;
wenzelm
parents: 73116
diff changeset
   224
73172
f7954a960890 more NEWS;
wenzelm
parents: 73170
diff changeset
   225
* The visual feedback on caret entity focus is normally restricted to
f7954a960890 more NEWS;
wenzelm
parents: 73170
diff changeset
   226
definitions within the visible text area. The keyboard modifier "CS"
f7954a960890 more NEWS;
wenzelm
parents: 73170
diff changeset
   227
overrides this: then all defining and referencing positions are shown.
f7954a960890 more NEWS;
wenzelm
parents: 73170
diff changeset
   228
See also option "jedit_focus_modifier".
f7954a960890 more NEWS;
wenzelm
parents: 73170
diff changeset
   229
72481
4bf8a8a2d2ad more uniform JVM vs. ML status widget;
wenzelm
parents: 72479
diff changeset
   230
* The jEdit status line includes widgets both for JVM and ML heap usage.
4bf8a8a2d2ad more uniform JVM vs. ML status widget;
wenzelm
parents: 72479
diff changeset
   231
Ongoing ML ongoing garbage collection is shown as "ML cleanup".
72380
510ebf846696 more documentation;
wenzelm
parents: 72350
diff changeset
   232
510ebf846696 more documentation;
wenzelm
parents: 72350
diff changeset
   233
* The Monitor dockable provides buttons to request a full garbage
510ebf846696 more documentation;
wenzelm
parents: 72350
diff changeset
   234
collection and sharing of live data on the ML heap. It also includes
510ebf846696 more documentation;
wenzelm
parents: 72350
diff changeset
   235
information about the Java Runtime system.
510ebf846696 more documentation;
wenzelm
parents: 72350
diff changeset
   236
73073
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 73044
diff changeset
   237
* PIDE support for session ROOTS: markup for directories.
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 73044
diff changeset
   238
72479
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 72464
diff changeset
   239
* Update to jedit-5.6.0, the latest release. This version works properly
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 72464
diff changeset
   240
on macOS by default, without the special MacOSX plugin.
72160
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 72155
diff changeset
   241
73365
6345ad861a36 more documentation;
wenzelm
parents: 73360
diff changeset
   242
* Action "full-screen-mode" (shortcut F11 or S+F11) has been modified
6345ad861a36 more documentation;
wenzelm
parents: 73360
diff changeset
   243
for better approximate window size on macOS and Linux/X11.
6345ad861a36 more documentation;
wenzelm
parents: 73360
diff changeset
   244
73407
c4b688abe2c4 clarified documentation concerning macOS Big Sur;
wenzelm
parents: 73401
diff changeset
   245
* Improved GUI support for macOS 11.1 Big Sur: native fullscreen mode,
c4b688abe2c4 clarified documentation concerning macOS Big Sur;
wenzelm
parents: 73401
diff changeset
   246
but non-native look-and-feel (FlatLaf).
c4b688abe2c4 clarified documentation concerning macOS Big Sur;
wenzelm
parents: 73401
diff changeset
   247
73493
d92409f8203a tuned NEWS;
wenzelm
parents: 73478
diff changeset
   248
* Hyperlinks to various file-formats (.pdf, .png, etc.) open an external
d92409f8203a tuned NEWS;
wenzelm
parents: 73478
diff changeset
   249
viewer, instead of re-using the jEdit text editor.
d92409f8203a tuned NEWS;
wenzelm
parents: 73478
diff changeset
   250
73419
ab3fa0abc119 IDE support for Naproche-SAD;
wenzelm
parents: 73417
diff changeset
   251
* IDE support for Naproche-SAD: Proof Checking of Natural Mathematical
ab3fa0abc119 IDE support for Naproche-SAD;
wenzelm
parents: 73417
diff changeset
   252
Documents. See also $NAPROCHE_HOME/examples for files with .ftl or
73493
d92409f8203a tuned NEWS;
wenzelm
parents: 73478
diff changeset
   253
.ftl.tex extension. The corresponding Naproche-SAD server process can be
d92409f8203a tuned NEWS;
wenzelm
parents: 73478
diff changeset
   254
disabled by setting the system option naproche_server=false and
d92409f8203a tuned NEWS;
wenzelm
parents: 73478
diff changeset
   255
restarting the Isabelle application.
73470
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73440
diff changeset
   256
72160
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 72155
diff changeset
   257
72129
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 72128
diff changeset
   258
*** Document preparation ***
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 72128
diff changeset
   259
72836
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72816
diff changeset
   260
* Keyword 'document_theories' within ROOT specifies theories from other
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72816
diff changeset
   261
sessions that should be included in the generated document source
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72816
diff changeset
   262
directory. This does not affect the generated session.tex: \input{...}
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72816
diff changeset
   263
needs to be used separately.
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72816
diff changeset
   264
72546
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72541
diff changeset
   265
* The standard LaTeX engine is now lualatex, according to settings
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72541
diff changeset
   266
variable ISABELLE_PDFLATEX. This is mostly upwards compatible with old
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72541
diff changeset
   267
pdflatex, but text encoding needs to conform strictly to utf8. Rare
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72541
diff changeset
   268
INCOMPATIBILITY.
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72541
diff changeset
   269
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72541
diff changeset
   270
* Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72541
diff changeset
   271
document output is always PDF.
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72541
diff changeset
   272
73000
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72987
diff changeset
   273
* Antiquotation @{tool} refers to Isabelle command-line tools, with
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72987
diff changeset
   274
completion and formal reference to the source (external script or
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72987
diff changeset
   275
internal Scala function).
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72987
diff changeset
   276
72135
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 72129
diff changeset
   277
* Antiquotation @{bash_function} refers to GNU bash functions that are
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 72129
diff changeset
   278
checked within the Isabelle settings environment.
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 72129
diff changeset
   279
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 72129
diff changeset
   280
* Antiquotations @{scala}, @{scala_object}, @{scala_type},
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 72129
diff changeset
   281
@{scala_method} refer to checked Isabelle/Scala entities.
72129
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 72128
diff changeset
   282
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 72128
diff changeset
   283
72128
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   284
*** Pure ***
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   285
72151
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents: 72150
diff changeset
   286
* Session Pure-Examples contains notable examples for Isabelle/Pure
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents: 72150
diff changeset
   287
(former entries of HOL-Isar_Examples).
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents: 72150
diff changeset
   288
72976
e7c2848b78e8 refined syntax for bundle mixins for locale and class specifications
haftmann
parents: 72966
diff changeset
   289
* Named contexts (locale and class specifications, locale and class
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   290
context blocks) allow bundle mixins for the surface context. This allows
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   291
syntax notations to be organized within bundles conveniently. See theory
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   292
"HOL-ex.Specifications_with_bundle_mixins" for examples and the isar-ref
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   293
manual for syntax descriptions.
72976
e7c2848b78e8 refined syntax for bundle mixins for locale and class specifications
haftmann
parents: 72966
diff changeset
   294
72128
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   295
* Definitions in locales produce rule which can be added as congruence
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   296
rule to protect foundational terms during simplification.
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   297
72682
24bd1316eaae consolidated names and operations
haftmann
parents: 72621
diff changeset
   298
* Consolidated terminology and function signatures for nested targets:
24bd1316eaae consolidated names and operations
haftmann
parents: 72621
diff changeset
   299
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   300
  - Local_Theory.begin_nested replaces Local_Theory.open_target
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   301
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   302
  - Local_Theory.end_nested replaces Local_Theory.close_target
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   303
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   304
  - Combination of Local_Theory.begin_nested and
72683
e51f1733618d replaced combinators by more conventional nesting pattern
haftmann
parents: 72682
diff changeset
   305
    Local_Theory.end_nested(_result) replaces
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   306
    Local_Theory.subtarget(_result)
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   307
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   308
INCOMPATIBILITY.
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   309
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   310
* Local_Theory.init replaces Generic_Target.init. Minor INCOMPATIBILITY.
72751
17dc99589a91 unified Local_Theory.init with Generic_Target.init
haftmann
parents: 72749
diff changeset
   311
72128
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   312
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   313
*** HOL ***
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   314
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   315
* Session HOL-Examples contains notable examples for Isabelle/HOL
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   316
(former entries of HOL-Isar_Examples, HOL-ex etc.).
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   317
72711
b452242dce36 proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents: 72703
diff changeset
   318
* 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: 72703
diff changeset
   319
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: 72703
diff changeset
   320
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: 72703
diff changeset
   321
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: 72703
diff changeset
   322
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   323
* Zipperposition 2.0 is now included as Isabelle component for
73211
162b71f7e554 rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;
wenzelm
parents: 73209
diff changeset
   324
experimentation, e.g. in "sledgehammer [prover = zipperposition]".
162b71f7e554 rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;
wenzelm
parents: 73209
diff changeset
   325
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   326
* Sledgehammer:
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   327
  - support veriT in proof preplay
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   328
  - take adventage of more cores in proof preplay
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   329
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   330
* Updated the Metis prover underlying the "metis" proof method to
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   331
version 2.4 (release 20180810). The new version fixes one soundness
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   332
defect and two incompleteness defects. Very slight INCOMPATIBILITY.
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   333
72439
wenzelm
parents: 72396
diff changeset
   334
* Nitpick/Kodkod may be invoked directly within the running
wenzelm
parents: 72396
diff changeset
   335
Isabelle/Scala session (instead of an external Java process): this
wenzelm
parents: 72396
diff changeset
   336
improves reactivity and saves resources. This experimental feature is
73248
dacf2598bb27 proper NEWS according to current situation;
wenzelm
parents: 73247
diff changeset
   337
guarded by system option "kodkod_scala" (default: true in PIDE
dacf2598bb27 proper NEWS according to current situation;
wenzelm
parents: 73247
diff changeset
   338
interaction, false in batch builds).
72439
wenzelm
parents: 72396
diff changeset
   339
72300
wenzelm
parents: 72290
diff changeset
   340
* Simproc "defined_all" and rewrite rule "subst_all" perform more
wenzelm
parents: 72290
diff changeset
   341
aggressive substitution with variables from assumptions.
wenzelm
parents: 72290
diff changeset
   342
INCOMPATIBILITY, consider repairing proofs locally like this:
wenzelm
parents: 72290
diff changeset
   343
wenzelm
parents: 72290
diff changeset
   344
  supply subst_all [simp del] [[simproc del: defined_all]]
wenzelm
parents: 72290
diff changeset
   345
72128
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   346
* Simproc "datatype_no_proper_subterm" rewrites equalities "lhs = rhs"
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   347
on datatypes to "False" if either side is a proper subexpression of the
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   348
other (for any datatype with a reasonable size function).
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   349
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   350
* Syntax for state monad combinators fcomp and scomp is organized in
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   351
bundle state_combinator_syntax.  Minor INCOMPATIBILITY.
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   352
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   353
* Syntax for reflected term syntax is organized in bundle term_syntax,
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   354
discontinuing previous locale term_syntax.  Minor INCOMPATIBILITY.
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   355
72128
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   356
* New constant "power_int" for exponentiation with integer exponent,
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   357
written as "x powi n".
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   358
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   359
* Added the "at most 1" quantifier, Uniq.
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   360
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   361
* For the natural numbers, "Sup {} = 0".
72234
913162a47d9f Update Metis to 2.4
desharna
parents: 72231
diff changeset
   362
73352
981a383610df HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents: 73336
diff changeset
   363
* 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: 73336
diff changeset
   364
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: 73336
diff changeset
   365
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: 73336
diff changeset
   366
981a383610df HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents: 73336
diff changeset
   367
* 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: 73336
diff changeset
   368
of algebraic integers.
981a383610df HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents: 73336
diff changeset
   369
72184
a4bffc0de967 bit operations as distinctive library theory
haftmann
parents: 72177
diff changeset
   370
* Library theory "Bit_Operations" with generic bit operations.
a4bffc0de967 bit operations as distinctive library theory
haftmann
parents: 72177
diff changeset
   371
72512
beeadb35e357 more thorough treatment of division, particularly signed division on int and word
haftmann
parents: 72496
diff changeset
   372
* Library theory "Signed_Division" provides operations for signed
beeadb35e357 more thorough treatment of division, particularly signed division on int and word
haftmann
parents: 72496
diff changeset
   373
division, instantiated for type int.
beeadb35e357 more thorough treatment of division, particularly signed division on int and word
haftmann
parents: 72496
diff changeset
   374
73289
ab9e27da0e85 HOL-Library: Changed notation for sum_mset
Manuel Eberl <eberlm@in.tum.de>
parents: 73249
diff changeset
   375
* Theory "Multiset": removed misleading notation \<Union># for sum_mset;
73336
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   376
replaced with \<Sum>\<^sub>#. Analogous notation for prod_mset also exists now.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   377
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   378
* New theory "HOL-Library.Word" takes over material from former session
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   379
"HOL-Word". INCOMPATIBILITY: need to adjust imports.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   380
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   381
* Theory "HOL-Library.Word": Type word is restricted to bit strings
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   382
consisting of at least one bit. INCOMPATIBILITY.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   383
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   384
* Theory "HOL-Library.Word": Bit operations NOT, AND, OR, XOR are based
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   385
on generic algebraic bit operations from theory
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   386
"HOL-Library.Bit_Operations". INCOMPATIBILITY.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   387
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   388
* Theory "HOL-Library.Word": Most operations on type word are set up for
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   389
transfer and lifting. INCOMPATIBILITY.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   390
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   391
* Theory "HOL-Library.Word": Generic type conversions. INCOMPATIBILITY,
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   392
sometimes additional rewrite rules must be added to applications to get
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   393
a confluent system again.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   394
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   395
* Theory "HOL-Library.Word": Uniform polymorphic "mask" operation for
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   396
both types int and word. INCOMPATIBILITY.
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   397
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   398
* Theory "HOL-Library.Word": Syntax for signed compare operators has
86a18742e5b2 clarified NEWS;
wenzelm
parents: 73320
diff changeset
   399
been consolidated with syntax of regular compare operators. Minor
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   400
INCOMPATIBILITY.
72621
633d14bd1e59 consolidated for the sake of documentation
haftmann
parents: 72565
diff changeset
   401
72749
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72745
diff changeset
   402
* 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: 72745
diff changeset
   403
represented as reversed lists of bools are separated into theory
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   404
Reversed_Bit_Lists in session Word_Lib in the AFP. INCOMPATIBILITY.
72749
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72745
diff changeset
   405
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72745
diff changeset
   406
* Former session "HOL-Word": Theory "Word_Bitwise" has been moved to AFP
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   407
entry Word_Lib as theory "Bitwise". INCOMPATIBILITY.
72749
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72745
diff changeset
   408
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72745
diff changeset
   409
* 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: 72745
diff changeset
   410
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: 72745
diff changeset
   411
INCOMPATIBILITY.
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72745
diff changeset
   412
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72745
diff changeset
   413
* Former session "HOL-Word": Operations lsb, msb and set_bit are
72780
58b1826354c9 NEWS and CONTRIBUTORS
haftmann
parents: 72759
diff changeset
   414
separated into theories Least_significant_bit, Most_significant_bit and
58b1826354c9 NEWS and CONTRIBUTORS
haftmann
parents: 72759
diff changeset
   415
Generic_set_bit respectively in session Word_Lib in the AFP.
58b1826354c9 NEWS and CONTRIBUTORS
haftmann
parents: 72759
diff changeset
   416
INCOMPATIBILITY.
72749
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72745
diff changeset
   417
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72745
diff changeset
   418
* Former session "HOL-Word": Ancient int numeral representation has been
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   419
factored out in separate theory "Ancient_Numeral" in session Word_Lib in
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   420
the AFP. INCOMPATIBILITY.
72749
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72745
diff changeset
   421
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72745
diff changeset
   422
* 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: 72745
diff changeset
   423
"bin_nth", "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   424
"max_word" are now mere input abbreviations. Minor INCOMPATIBILITY.
72749
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72745
diff changeset
   425
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72745
diff changeset
   426
* Former session "HOL-Word": Misc ancient material has been factored out
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   427
into separate theories and moved to session Word_Lib in the AFP. See
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   428
theory "Guide" there for further information. INCOMPATIBILITY.
72217
ec17263ec38d removed superfluous dependency
haftmann
parents: 72216
diff changeset
   429
72300
wenzelm
parents: 72290
diff changeset
   430
* Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands
wenzelm
parents: 72290
diff changeset
   431
are in working order again, as opposed to outputting "GaveUp" on nearly
wenzelm
parents: 72290
diff changeset
   432
all problems.
72191
ee2c7f0dd1be prefer single name
haftmann
parents: 72185
diff changeset
   433
73228
b1be35908165 clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents: 73212
diff changeset
   434
* Session "HOL-Hoare": concrete syntax only for Hoare triples, not
b1be35908165 clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents: 73212
diff changeset
   435
abstract language constructors.
b1be35908165 clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents: 73212
diff changeset
   436
b1be35908165 clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents: 73212
diff changeset
   437
* Session "HOL-Hoare": now provides a total correctness logic as well.
b1be35908165 clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents: 73212
diff changeset
   438
72128
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   439
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   440
*** FOL ***
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   441
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   442
* Added the "at most 1" quantifier, Uniq, as in HOL.
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   443
72300
wenzelm
parents: 72290
diff changeset
   444
* Simproc "defined_all" and rewrite rule "subst_all" have been changed
wenzelm
parents: 72290
diff changeset
   445
as in HOL.
72150
haftmann
parents: 72136
diff changeset
   446
72128
0408f6814224 misc tuning;
wenzelm
parents: 72070
diff changeset
   447
72135
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 72129
diff changeset
   448
*** ML ***
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 72129
diff changeset
   449
72565
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72549
diff changeset
   450
* 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: 72549
diff changeset
   451
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: 72549
diff changeset
   452
invocation works via the PIDE protocol.
72135
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 72129
diff changeset
   453
72745
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72744
diff changeset
   454
* Path.append is available as overloaded "+" operator, similar to
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72744
diff changeset
   455
corresponding Isabelle/Scala operation.
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72744
diff changeset
   456
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   457
* ML statistics via an external Poly/ML process: this allows monitoring
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   458
the runtime system while the ML program sleeps.
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   459
72135
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 72129
diff changeset
   460
71931
wenzelm
parents: 71881
diff changeset
   461
*** System ***
wenzelm
parents: 71881
diff changeset
   462
73247
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   463
* Isabelle server allows user-defined commands via
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   464
isabelle_scala_service.
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   465
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   466
* Update/rebuild external provers on currently supported OS platforms,
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   467
notably CVC4 1.8, E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
11140980a6b5 updated for release;
wenzelm
parents: 73237
diff changeset
   468
73116
b3e9e9e4ff74 clarified session log file: avoid erratic messages;
wenzelm
parents: 73113
diff changeset
   469
* The command-line tool "isabelle log" prints prover messages from the
b3e9e9e4ff74 clarified session log file: avoid erratic messages;
wenzelm
parents: 73113
diff changeset
   470
build database of the given session, following the the order of theory
b3e9e9e4ff74 clarified session log file: avoid erratic messages;
wenzelm
parents: 73113
diff changeset
   471
sources, instead of erratic parallel evaluation. Consequently, the
b3e9e9e4ff74 clarified session log file: avoid erratic messages;
wenzelm
parents: 73113
diff changeset
   472
session log file is restricted to system messages of the overall build
b3e9e9e4ff74 clarified session log file: avoid erratic messages;
wenzelm
parents: 73113
diff changeset
   473
process, and thus becomes more informative.
73113
626fcaebd049 NEWS and documentation for "isabelle log";
wenzelm
parents: 73073
diff changeset
   474
72541
564012e31db1 discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents: 72535
diff changeset
   475
* Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
564012e31db1 discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents: 72535
diff changeset
   476
variable.
564012e31db1 discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents: 72535
diff changeset
   477
72549
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72546
diff changeset
   478
* The command-line tool "isabelle logo" only outputs PDF; obsolete EPS
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72546
diff changeset
   479
(for DVI documents) has been discontinued. Former option -n has been
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72546
diff changeset
   480
turned into -o with explicit file name. Minor INCOMPATIBILITY.
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72546
diff changeset
   481
73417
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 73407
diff changeset
   482
* The command-line tool "isabelle components" supports new options -u
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 73407
diff changeset
   483
and -x to manage $ISABELLE_HOME_USER/etc/components without manual
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 73407
diff changeset
   484
editing of Isabelle configuration files.
fc828f64da5b support isabelle components -u and -x;
wenzelm
parents: 73407
diff changeset
   485
72395
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72380
diff changeset
   486
* The shell function "isabelle_directory" (within etc/settings of
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72380
diff changeset
   487
components) augments the list of special directories for persistent
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72380
diff changeset
   488
symbolic path names. This improves portability of heap images and
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72380
diff changeset
   489
session databases. It used to be hard-wired for Isabelle + AFP, but
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72380
diff changeset
   490
other projects may now participate on equal terms.
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72380
diff changeset
   491
72917
035b8054013a tuned NEWS;
wenzelm
parents: 72915
diff changeset
   492
* The command-line tool "isabelle process" now prints output to
035b8054013a tuned NEWS;
wenzelm
parents: 72915
diff changeset
   493
stdout/stderr separately and incrementally, instead of just one bulk to
035b8054013a tuned NEWS;
wenzelm
parents: 72915
diff changeset
   494
stdout after termination. Potential INCOMPATIBILITY for external tools.
035b8054013a tuned NEWS;
wenzelm
parents: 72915
diff changeset
   495
035b8054013a tuned NEWS;
wenzelm
parents: 72915
diff changeset
   496
* The command-line tool "isabelle console" now supports interrupts
035b8054013a tuned NEWS;
wenzelm
parents: 72915
diff changeset
   497
properly (on Linux and macOS).
035b8054013a tuned NEWS;
wenzelm
parents: 72915
diff changeset
   498
72333
7b318273a4aa discontinued old batch-build functionality;
wenzelm
parents: 72325
diff changeset
   499
* Batch-builds via "isabelle build" use a PIDE session with special
7b318273a4aa discontinued old batch-build functionality;
wenzelm
parents: 72325
diff changeset
   500
protocol: this allows to invoke Isabelle/Scala operations from
7b318273a4aa discontinued old batch-build functionality;
wenzelm
parents: 72325
diff changeset
   501
Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for the
7b318273a4aa discontinued old batch-build functionality;
wenzelm
parents: 72325
diff changeset
   502
java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings:
72206
80d7f004089d clarified NEWS;
wenzelm
parents: 72204
diff changeset
   503
80d7f004089d clarified NEWS;
wenzelm
parents: 72204
diff changeset
   504
  ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx8g"
72204
2d658beb815b enable pide_session by default (again), with extra JVM heap for AFP tests (see also 86e429abd38d, 026de3424c39);
wenzelm
parents: 72192
diff changeset
   505
72966
caa182bdab7a clarified options: batch-build has pide_reports disabled by default (requires significant resources);
wenzelm
parents: 72920
diff changeset
   506
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: 72920
diff changeset
   507
enabled.
caa182bdab7a clarified options: batch-build has pide_reports disabled by default (requires significant resources);
wenzelm
parents: 72920
diff changeset
   508
72915
7ab733b2aecb more NEWS;
wenzelm
parents: 72914
diff changeset
   509
* The command-line tool "isabelle build" provides option -P DIR to
7ab733b2aecb more NEWS;
wenzelm
parents: 72914
diff changeset
   510
produce PDF/HTML presentation in the specified directory; -P: refers to
7ab733b2aecb more NEWS;
wenzelm
parents: 72914
diff changeset
   511
the standard directory according to ISABELLE_BROWSER_INFO /
7ab733b2aecb more NEWS;
wenzelm
parents: 72914
diff changeset
   512
ISABELLE_BROWSER_INFO_SYSTEM settings. Generated PDF documents are taken
7ab733b2aecb more NEWS;
wenzelm
parents: 72914
diff changeset
   513
from the build database -- from this or earlier builds with option
7ab733b2aecb more NEWS;
wenzelm
parents: 72914
diff changeset
   514
document=pdf.
7ab733b2aecb more NEWS;
wenzelm
parents: 72914
diff changeset
   515
72809
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72793
diff changeset
   516
* The command-line tool "isabelle document" generates theory documents
72915
7ab733b2aecb more NEWS;
wenzelm
parents: 72914
diff changeset
   517
on the spot, using the underlying session build database (exported
72917
035b8054013a tuned NEWS;
wenzelm
parents: 72915
diff changeset
   518
LaTeX sources or existing PDF files). INCOMPATIBILITY, the former
72915
7ab733b2aecb more NEWS;
wenzelm
parents: 72914
diff changeset
   519
"isabelle document" tool was rather different and has been discontinued.
72809
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72793
diff changeset
   520
72024
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 72004
diff changeset
   521
* The command-line tool "isabelle sessions" explores the structure of
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 72004
diff changeset
   522
Isabelle sessions and prints result names in topological order (on
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 72004
diff changeset
   523
stdout).
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 72004
diff changeset
   524
71949
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71944
diff changeset
   525
* The Isabelle/Scala "Progress" interface changed slightly and
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71944
diff changeset
   526
"No_Progress" has been discontinued. INCOMPATIBILITY, use "new Progress"
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71944
diff changeset
   527
instead.
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71944
diff changeset
   528
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71944
diff changeset
   529
* General support for Isabelle/Scala system services, configured via the
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71944
diff changeset
   530
shell function "isabelle_scala_service" in etc/settings (e.g. of an
71957
wenzelm
parents: 71952
diff changeset
   531
Isabelle component); see implementations of class
wenzelm
parents: 71952
diff changeset
   532
Isabelle_System.Service in Isabelle/Scala. This supersedes former
wenzelm
parents: 71952
diff changeset
   533
"isabelle_scala_tools" and "isabelle_file_format": minor
wenzelm
parents: 71952
diff changeset
   534
INCOMPATIBILITY.
71944
wenzelm
parents: 71931
diff changeset
   535
72986
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72966
diff changeset
   536
* The syntax of theory load commands (for auxiliary files) is now
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72966
diff changeset
   537
specified in Isabelle/Scala, as instance of class
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72966
diff changeset
   538
isabelle.Command_Span.Load_Command registered via isabelle_scala_service
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72966
diff changeset
   539
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: 72966
diff changeset
   540
file extensions. Minor INCOMPATIBILITY, e.g. see theory
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72966
diff changeset
   541
HOL-SPARK.SPARK_Setup to emulate the old behaviour.
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72966
diff changeset
   542
73360
b84887a67cc6 clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents: 73356
diff changeset
   543
* JVM system property "isabelle.laf" has been discontinued; the default
b84887a67cc6 clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents: 73356
diff changeset
   544
Swing look-and-feel is ""FlatLaf Light".
b84887a67cc6 clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents: 73356
diff changeset
   545
72759
354bfab78cbf Isabelle/Phabricator supports Ubuntu 20.04 LTS;
wenzelm
parents: 72754
diff changeset
   546
* Isabelle/Phabricator supports Ubuntu 20.04 LTS.
354bfab78cbf Isabelle/Phabricator supports Ubuntu 20.04 LTS;
wenzelm
parents: 72754
diff changeset
   547
72070
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 72064
diff changeset
   548
* Isabelle/Phabricator setup has been updated to follow ongoing
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 72064
diff changeset
   549
development: libphutil has been discontinued. Minor INCOMPATIBILITY:
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 72064
diff changeset
   550
existing server installations should remove libphutil from
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 72064
diff changeset
   551
/usr/local/bin/isabelle-phabricator-upgrade and each installation root
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 72064
diff changeset
   552
directory (e.g. /var/www/phabricator-vcs/libphutil).
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 72064
diff changeset
   553
72744
wenzelm
parents: 72711
diff changeset
   554
* Experimental support for arm64-linux platform. The reference platform
wenzelm
parents: 72711
diff changeset
   555
is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
wenzelm
parents: 72711
diff changeset
   556
73478
030b930d1ac8 updated for release;
wenzelm
parents: 73470
diff changeset
   557
* Support for Apple Silicon, using mostly x86_64-darwin runtime
030b930d1ac8 updated for release;
wenzelm
parents: 73470
diff changeset
   558
translation via Rosetta 2 (e.g. Poly/ML and external provers), but also
030b930d1ac8 updated for release;
wenzelm
parents: 73470
diff changeset
   559
some native arm64-darwin executables (e.g. Java).
73399
56107393f2ef more NEWS;
wenzelm
parents: 73388
diff changeset
   560
71772
61ba52af28e3 back to post-release mode;
wenzelm
parents: 71765
diff changeset
   561
72064
0bbe0866b7e6 The Uniq quantifier for FOL too
paulson <lp15@cam.ac.uk>
parents: 72062
diff changeset
   562
71698
29e297fd5473 updated for release;
wenzelm
parents: 71697
diff changeset
   563
New in Isabelle2020 (April 2020)
29e297fd5473 updated for release;
wenzelm
parents: 71697
diff changeset
   564
--------------------------------
70449
a8238fd25541 back to post-release mode;
wenzelm
parents: 70444
diff changeset
   565
70748
wenzelm
parents: 70711
diff changeset
   566
*** General ***
wenzelm
parents: 70711
diff changeset
   567
70867
56d70f7ce4a4 more documentation;
wenzelm
parents: 70794
diff changeset
   568
* Session ROOT files need to specify explicit 'directories' for import
70871
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70867
diff changeset
   569
of theory files. Directories cannot be shared by different sessions.
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70867
diff changeset
   570
(Recall that import of theories from other sessions works via
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70867
diff changeset
   571
session-qualified theory names, together with suitable 'sessions'
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70867
diff changeset
   572
declarations in the ROOT.)
70867
56d70f7ce4a4 more documentation;
wenzelm
parents: 70794
diff changeset
   573
70748
wenzelm
parents: 70711
diff changeset
   574
* Internal derivations record dependencies on oracles and other theorems
wenzelm
parents: 70711
diff changeset
   575
accurately, including the implicit type-class reasoning wrt. proven
wenzelm
parents: 70711
diff changeset
   576
class relations and type arities. In particular, the formal tagging with
wenzelm
parents: 70711
diff changeset
   577
"Pure.skip_proofs" of results stemming from "instance ... sorry" is now
wenzelm
parents: 70711
diff changeset
   578
propagated properly to theorems depending on such type instances.
wenzelm
parents: 70711
diff changeset
   579
wenzelm
parents: 70711
diff changeset
   580
* Command 'sorry' (oracle "Pure.skip_proofs") is more precise about the
wenzelm
parents: 70711
diff changeset
   581
actual proposition that is assumed in the goal and proof context. This
wenzelm
parents: 70711
diff changeset
   582
requires at least Proofterm.proofs = 1 to show up in theorem
wenzelm
parents: 70711
diff changeset
   583
dependencies.
wenzelm
parents: 70711
diff changeset
   584
wenzelm
parents: 70711
diff changeset
   585
* Command 'thm_oracles' prints all oracles used in given theorems,
wenzelm
parents: 70711
diff changeset
   586
covering the full graph of transitive dependencies.
wenzelm
parents: 70711
diff changeset
   587
70791
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70785
diff changeset
   588
* Command 'thm_deps' prints immediate theorem dependencies of the given
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70785
diff changeset
   589
facts. The former graph visualization has been discontinued, because it
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70785
diff changeset
   590
was hardly usable.
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70785
diff changeset
   591
71658
wenzelm
parents: 71650
diff changeset
   592
* Refined treatment of proof terms, including type-class proofs for
wenzelm
parents: 71650
diff changeset
   593
minor object-logics (FOL, FOLP, Sequents).
wenzelm
parents: 71650
diff changeset
   594
71661
wenzelm
parents: 71658
diff changeset
   595
* The inference kernel is now confined to one main module: structure
wenzelm
parents: 71658
diff changeset
   596
Thm, without the former circular dependency on structure Axclass.
wenzelm
parents: 71658
diff changeset
   597
71759
b0b16088ccf2 allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
wenzelm
parents: 71757
diff changeset
   598
* 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: 71757
diff changeset
   599
separate delimiters (as documented in the isar-ref manual), without
71761
d350aabace23 proper escape for literal single quotes;
wenzelm
parents: 71759
diff changeset
   600
requiring an auxiliary empty block. A literal single quote needs to be
71765
wenzelm
parents: 71761
diff changeset
   601
escaped properly. Minor INCOMPATIBILITY.
71759
b0b16088ccf2 allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
wenzelm
parents: 71757
diff changeset
   602
70748
wenzelm
parents: 70711
diff changeset
   603
70708
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
   604
*** Isar ***
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
   605
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
   606
* The proof method combinator (subproofs m) applies the method
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
   607
expression m consecutively to each subgoal, constructing individual
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
   608
subproofs internally. This impacts the internal construction of proof
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
   609
terms: it makes a cascade of let-expressions within the derivation tree
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
   610
and may thus improve scalability.
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
   611
71639
wenzelm
parents: 71587
diff changeset
   612
* Attribute "trace_locales" activates tracing of locale instances during
wenzelm
parents: 71587
diff changeset
   613
roundup. It replaces the diagnostic command 'print_dependencies', which
wenzelm
parents: 71587
diff changeset
   614
has been discontinued.
70794
d997c7ba3305 Tracing of locale activation.
ballarin
parents: 70791
diff changeset
   615
70708
f2d58cafbc13 more documentation;
wenzelm
parents: 70620
diff changeset
   616
70873
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70871
diff changeset
   617
*** Isabelle/jEdit Prover IDE ***
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70871
diff changeset
   618
71757
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   619
* Prover IDE startup is now much faster, because theory dependencies are
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   620
no longer explored in advance. The overall session structure with its
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   621
declarations of 'directories' is sufficient to locate theory files. Thus
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   622
the "session focus" of option "isabelle jedit -S" has become obsolete
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   623
(likewise for "isabelle vscode_server -S"). Existing option "-R" is both
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   624
sufficient and more convenient to start editing a particular session.
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   625
71711
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71707
diff changeset
   626
* Actions isabelle.tooltip (CS+b) and isabelle.message (CS+m) display
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71707
diff changeset
   627
tooltip message popups, corresponding to mouse hovering with/without the
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71707
diff changeset
   628
CONTROL/COMMAND key pressed.
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71707
diff changeset
   629
71713
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   630
* The following actions allow to navigate errors within the current
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   631
document snapshot:
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   632
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   633
  isabelle.first-error (CS+a)
71719
ae3399b05e9b more documentation;
wenzelm
parents: 71713
diff changeset
   634
  isabelle.last-error (CS+z)
ae3399b05e9b more documentation;
wenzelm
parents: 71713
diff changeset
   635
  isabelle.next-error (CS+n)
ae3399b05e9b more documentation;
wenzelm
parents: 71713
diff changeset
   636
  isabelle.prev-error (CS+p)
71713
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   637
71642
wenzelm
parents: 71641
diff changeset
   638
* Support more brackets: \<llangle> \<rrangle> (intended for implicit argument syntax).
wenzelm
parents: 71641
diff changeset
   639
71734
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71719
diff changeset
   640
* Action isabelle.jconsole (menu item Plugins / Isabelle / Java/VM
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71719
diff changeset
   641
Monitor) applies the jconsole tool on the running Isabelle/jEdit
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71719
diff changeset
   642
process. This allows to monitor resource usage etc.
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71719
diff changeset
   643
71757
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   644
* More adequate default font sizes for Linux on HD / UHD displays:
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   645
automatic font scaling is usually absent on Linux, in contrast to
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   646
Windows and macOS.
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   647
71792
aff37005fd79 more NEWS;
wenzelm
parents: 71765
diff changeset
   648
* The default value for the jEdit property "view.antiAlias" (menu item
aff37005fd79 more NEWS;
wenzelm
parents: 71765
diff changeset
   649
Utilities / Global Options / Text Area / Anti Aliased smooth text) is
aff37005fd79 more NEWS;
wenzelm
parents: 71765
diff changeset
   650
now "subpixel HRGB", instead of former "standard". Especially on Linux
aff37005fd79 more NEWS;
wenzelm
parents: 71765
diff changeset
   651
this often leads to faster text rendering, but can also cause problems
aff37005fd79 more NEWS;
wenzelm
parents: 71765
diff changeset
   652
with odd color shades. An alternative is to switch back to "standard"
aff37005fd79 more NEWS;
wenzelm
parents: 71765
diff changeset
   653
here, and set the following Java system property:
aff37005fd79 more NEWS;
wenzelm
parents: 71765
diff changeset
   654
aff37005fd79 more NEWS;
wenzelm
parents: 71765
diff changeset
   655
    isabelle jedit -Dsun.java2d.opengl=true
aff37005fd79 more NEWS;
wenzelm
parents: 71765
diff changeset
   656
aff37005fd79 more NEWS;
wenzelm
parents: 71765
diff changeset
   657
This can be made persistent via JEDIT_JAVA_OPTIONS in
aff37005fd79 more NEWS;
wenzelm
parents: 71765
diff changeset
   658
$ISABELLE_HOME_USER/etc/settings. For the "Isabelle2020" desktop
aff37005fd79 more NEWS;
wenzelm
parents: 71765
diff changeset
   659
application there is a corresponding options file in the same directory.
aff37005fd79 more NEWS;
wenzelm
parents: 71765
diff changeset
   660
70873
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70871
diff changeset
   661
71686
be84312a2d53 update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents: 71661
diff changeset
   662
*** Isabelle/VSCode Prover IDE ***
be84312a2d53 update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents: 71661
diff changeset
   663
71697
bb82dd4d19f6 updated for release;
wenzelm
parents: 71686
diff changeset
   664
* Update of State and Preview panels to use new WebviewPanel API of
bb82dd4d19f6 updated for release;
wenzelm
parents: 71686
diff changeset
   665
VSCode.
71686
be84312a2d53 update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents: 71661
diff changeset
   666
be84312a2d53 update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents: 71661
diff changeset
   667
70522
48609a6af1a0 removed relics of ASCII syntax for indexed big operators
haftmann
parents: 70485
diff changeset
   668
*** HOL ***
48609a6af1a0 removed relics of ASCII syntax for indexed big operators
haftmann
parents: 70485
diff changeset
   669
71639
wenzelm
parents: 71587
diff changeset
   670
* Improvements of the 'lift_bnf' command:
71473
0c454a5d125d NEWS, CONTRIBUTORS, and documentation
traytel
parents: 71468
diff changeset
   671
  - Add support for quotient types.
71639
wenzelm
parents: 71587
diff changeset
   672
  - Generate transfer rules for the lifted map/set/rel/pred constants
wenzelm
parents: 71587
diff changeset
   673
    (theorems "<type>.<constant>_transfer_raw").
71473
0c454a5d125d NEWS, CONTRIBUTORS, and documentation
traytel
parents: 71468
diff changeset
   674
70974
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
   675
* Term_XML.Encode/Decode.term uses compact representation of Const
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
   676
"typargs" from the given declaration environment. This also makes more
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
   677
sense for translations to lambda-calculi with explicit polymorphism.
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
   678
INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
   679
applications.
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
   680
70710
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
   681
* ASCII membership syntax concerning big operators for infimum and
71639
wenzelm
parents: 71587
diff changeset
   682
supremum has been discontinued. INCOMPATIBILITY.
70710
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
   683
71757
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   684
* Removed multiplicativity assumption from class
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   685
"normalization_semidom". Introduced various new intermediate classes
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   686
with the multiplicativity assumption; many theorem statements
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   687
(especially involving GCD/LCM) had to be adapted. This allows for a more
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   688
natural instantiation of the algebraic typeclasses for e.g. Gaussian
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   689
integers. INCOMPATIBILITY.
317e9ebbc3e1 updated for release;
wenzelm
parents: 71750
diff changeset
   690
70710
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
   691
* Clear distinction between types for bits (False / True) and Z2 (0 /
71639
wenzelm
parents: 71587
diff changeset
   692
1): theory HOL-Library.Bit has been renamed accordingly.
wenzelm
parents: 71587
diff changeset
   693
INCOMPATIBILITY.
wenzelm
parents: 71587
diff changeset
   694
wenzelm
parents: 71587
diff changeset
   695
* Dynamic facts "algebra_split_simps" and "field_split_simps" correspond
71007
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70974
diff changeset
   696
to algebra_simps and field_simps but contain more aggressive rules
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70974
diff changeset
   697
potentially splitting goals; algebra_split_simps roughly replaces
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70974
diff changeset
   698
sign_simps and field_split_simps can be used instead of divide_simps.
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70974
diff changeset
   699
INCOMPATIBILITY.
70710
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
   700
71640
wenzelm
parents: 71639
diff changeset
   701
* Theory HOL.Complete_Lattices:
wenzelm
parents: 71639
diff changeset
   702
renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf
wenzelm
parents: 71639
diff changeset
   703
71646
6c52b1d71f8b proper symbols;
wenzelm
parents: 71645
diff changeset
   704
* Theory HOL-Library.Monad_Syntax: infix operation "bind" (\<bind>)
70710
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
   705
associates to the left now as is customary.
7783bece74b4 tuned whitespace;
wenzelm
parents: 70708
diff changeset
   706
71468
09aee7f5b447 Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents: 71364
diff changeset
   707
* Theory HOL-Library.Ramsey: full finite Ramsey's theorem with
09aee7f5b447 Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents: 71364
diff changeset
   708
multiple colours and arbitrary exponents.
09aee7f5b447 Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents: 71364
diff changeset
   709
71697
bb82dd4d19f6 updated for release;
wenzelm
parents: 71686
diff changeset
   710
* Session HOL-Proofs: build faster thanks to better treatment of proof
bb82dd4d19f6 updated for release;
wenzelm
parents: 71686
diff changeset
   711
terms in Isabelle/Pure.
71345
wenzelm
parents: 71332
diff changeset
   712
71650
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   713
* Session HOL-Word: bitwise NOT-operator has proper prefix syntax. Minor
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   714
INCOMPATIBILITY.
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   715
71697
bb82dd4d19f6 updated for release;
wenzelm
parents: 71686
diff changeset
   716
* Session HOL-Analysis: proof method "metric" implements a decision
bb82dd4d19f6 updated for release;
wenzelm
parents: 71686
diff changeset
   717
procedure for simple linear statements in metric spaces.
bb82dd4d19f6 updated for release;
wenzelm
parents: 71686
diff changeset
   718
bb82dd4d19f6 updated for release;
wenzelm
parents: 71686
diff changeset
   719
* Session HOL-Complex_Analysis has been split off from HOL-Analysis.
71347
a7d1fb0c9e16 proper prefix syntax
haftmann
parents: 71345
diff changeset
   720
71348
9e7d40d67258 tuned whitespace
haftmann
parents: 71347
diff changeset
   721
70711
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   722
*** ML ***
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   723
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   724
* Theory construction may be forked internally, the operation
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   725
Theory.join_theory recovers a single result theory. See also the example
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   726
in theory "HOL-ex.Join_Theory".
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   727
70751
d0b75c59beca added ML antiquotation @{oracle_name};
wenzelm
parents: 70748
diff changeset
   728
* Antiquotation @{oracle_name} inlines a formally checked oracle name.
d0b75c59beca added ML antiquotation @{oracle_name};
wenzelm
parents: 70748
diff changeset
   729
71648
2e1b0ee920f5 updated for release;
wenzelm
parents: 71646
diff changeset
   730
* Minimal support for a soft-type system within the Isabelle logical
2e1b0ee920f5 updated for release;
wenzelm
parents: 71646
diff changeset
   731
framework (module Soft_Type_System).
2e1b0ee920f5 updated for release;
wenzelm
parents: 71646
diff changeset
   732
71965
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71877
diff changeset
   733
* Former Variable.auto_fixes has been replaced by slightly more general
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71877
diff changeset
   734
Proof_Context.augment: it is subject to an optional soft-type system of
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71877
diff changeset
   735
the underlying object-logic. Minor INCOMPATIBILITY.
71648
2e1b0ee920f5 updated for release;
wenzelm
parents: 71646
diff changeset
   736
71650
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   737
* More scalable Export.export using XML.tree to avoid premature string
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   738
allocations, with convenient shortcut XML.blob. Minor INCOMPATIBILITY.
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   739
71707
wenzelm
parents: 71698
diff changeset
   740
* Prover IDE support for the underlying Poly/ML compiler (not the basis
wenzelm
parents: 71698
diff changeset
   741
library). Open $ML_SOURCES/ROOT.ML in Isabelle/jEdit to browse the
wenzelm
parents: 71698
diff changeset
   742
implementation with full markup.
wenzelm
parents: 71698
diff changeset
   743
70711
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70710
diff changeset
   744
70785
wenzelm
parents: 70751
diff changeset
   745
*** System ***
wenzelm
parents: 70751
diff changeset
   746
71645
wenzelm
parents: 71644
diff changeset
   747
* Standard rendering for more Isabelle symbols: \<llangle> \<rrangle> \<bbar> \<sqdot>
wenzelm
parents: 71644
diff changeset
   748
71587
820cf124dced added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents: 71552
diff changeset
   749
* The command-line tool "isabelle scala_project" creates a Gradle
820cf124dced added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents: 71552
diff changeset
   750
project configuration for Isabelle/Scala/jEdit, to support Scala IDEs
820cf124dced added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents: 71552
diff changeset
   751
such as IntelliJ IDEA.
820cf124dced added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents: 71552
diff changeset
   752
71502
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   753
* The command-line tool "isabelle phabricator_setup" facilitates
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   754
self-hosting of the Phabricator software-development platform, with
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   755
support for Git, Mercurial, Subversion repositories. This helps to avoid
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   756
monoculture and to escape the gravity of centralized version control by
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   757
Github and/or Bitbucket. For further documentation, see chapter
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   758
"Phabricator server administration" in the "system" manual. A notable
8f3940150493 tuned NEWS;
wenzelm
parents: 71500
diff changeset
   759
example installation is https://isabelle-dev.sketis.net/.
71332
wenzelm
parents: 71153
diff changeset
   760
71534
wenzelm
parents: 71502
diff changeset
   761
* The command-line tool "isabelle hg_setup" simplifies the setup of
wenzelm
parents: 71502
diff changeset
   762
Mercurial repositories, with hosting via Phabricator or SSH file server
wenzelm
parents: 71502
diff changeset
   763
access.
wenzelm
parents: 71502
diff changeset
   764
70876
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70873
diff changeset
   765
* The command-line tool "isabelle imports" has been discontinued: strict
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70873
diff changeset
   766
checking of session directories enforces session-qualified theory names
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70873
diff changeset
   767
in applications -- users are responsible to specify session ROOT entries
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70873
diff changeset
   768
properly.
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70873
diff changeset
   769
71641
wenzelm
parents: 71640
diff changeset
   770
* The command-line tool "isabelle dump" and its underlying
wenzelm
parents: 71640
diff changeset
   771
Isabelle/Scala module isabelle.Dump has become more scalable, by
wenzelm
parents: 71640
diff changeset
   772
splitting sessions and supporting a base logic image. Minor
wenzelm
parents: 71640
diff changeset
   773
INCOMPATIBILITY in options and parameters.
wenzelm
parents: 71640
diff changeset
   774
71965
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71877
diff changeset
   775
* The command-line tool "isabelle build_docker" has been slightly
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71877
diff changeset
   776
improved: it is now properly documented in the "system" manual.
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71877
diff changeset
   777
71650
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   778
* Isabelle/Scala support for the Linux platform (Ubuntu): packages,
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   779
users, system services.
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   780
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   781
* Isabelle/Scala support for proof terms (with full type/term
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   782
information) in module isabelle.Term.
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   783
71877
263298eb68b2 more NEWS;
wenzelm
parents: 71798
diff changeset
   784
* Isabelle/Scala: more scalable output of YXML files, e.g. relevant for
263298eb68b2 more NEWS;
wenzelm
parents: 71798
diff changeset
   785
"isabelle dump".
263298eb68b2 more NEWS;
wenzelm
parents: 71798
diff changeset
   786
70785
wenzelm
parents: 70751
diff changeset
   787
* Theory export via Isabelle/Scala has been reworked. The former "fact"
wenzelm
parents: 70751
diff changeset
   788
name space is now split into individual "thm" items: names are
wenzelm
parents: 70751
diff changeset
   789
potentially indexed, such as "foo" for singleton facts, or "bar(1)",
wenzelm
parents: 70751
diff changeset
   790
"bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now
wenzelm
parents: 70751
diff changeset
   791
exported as well: this spans an overall dependency graph of internal
wenzelm
parents: 70751
diff changeset
   792
inferences; it might help to reconstruct the formal structure of theory
71966
abf3e80bd815 tuned NEWS;
wenzelm
parents: 71965
diff changeset
   793
libraries. See also the module isabelle.Export_Theory in Isabelle/Scala.
70785
wenzelm
parents: 70751
diff changeset
   794
71697
bb82dd4d19f6 updated for release;
wenzelm
parents: 71686
diff changeset
   795
* Theory export of structured specifications, based on internal
bb82dd4d19f6 updated for release;
wenzelm
parents: 71686
diff changeset
   796
declarations of Spec_Rules by packages like 'definition', 'inductive',
bb82dd4d19f6 updated for release;
wenzelm
parents: 71686
diff changeset
   797
'primrec', 'function'.
bb82dd4d19f6 updated for release;
wenzelm
parents: 71686
diff changeset
   798
71640
wenzelm
parents: 71639
diff changeset
   799
* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
wenzelm
parents: 71639
diff changeset
   800
have been discontinued -- deprecated since Isabelle2018.
wenzelm
parents: 71639
diff changeset
   801
71650
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   802
* More complete x86_64 platform support on macOS, notably Catalina where
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   803
old x86 has been discontinued.
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   804
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   805
* Update to GHC stack 2.1.3 with stackage lts-13.19/ghc-8.6.4.
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   806
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   807
* Update to OCaml Opam 2.0.6 (using ocaml 4.05.0 as before).
22158ebde77f updated for release;
wenzelm
parents: 71648
diff changeset
   808
70449
a8238fd25541 back to post-release mode;
wenzelm
parents: 70444
diff changeset
   809
70974
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70876
diff changeset
   810
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   811
New in Isabelle2019 (June 2019)
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   812
-------------------------------
68683
d69127c6e80f back to post-release mode -- after fork point;
wenzelm
parents: 68681
diff changeset
   813
69042
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   814
*** General ***
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   815
70214
0674c24afc5e updated for release;
wenzelm
parents: 70213
diff changeset
   816
* The font collection "Isabelle DejaVu" is systematically derived from
0674c24afc5e updated for release;
wenzelm
parents: 70213
diff changeset
   817
the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif"
69353
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   818
and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   819
The DejaVu base fonts are retricted to well-defined Unicode ranges and
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   820
augmented by special Isabelle symbols, taken from the former
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   821
"IsabelleText" font (which is no longer provided separately). The line
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   822
metrics and overall rendering quality is closer to original DejaVu.
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   823
INCOMPATIBILITY with display configuration expecting the old
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   824
"IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead.
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   825
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   826
* The Isabelle fonts render "\<inverse>" properly as superscript "-1".
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69324
diff changeset
   827
69042
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   828
* Old-style inner comments (* ... *) within the term language are no
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   829
longer supported (legacy feature in Isabelle2018).
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   830
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   831
* Old-style {* verbatim *} tokens are explicitly marked as legacy
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   832
feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   833
via "isabelle update_cartouches -t" (available since Isabelle2015).
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   834
70482
wenzelm
parents: 70466
diff changeset
   835
* Infix operators that begin or end with a "*" are now parenthesized
wenzelm
parents: 70466
diff changeset
   836
without additional spaces, e.g. "(*)" instead of "( * )". Minor
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   837
INCOMPATIBILITY.
69066
nipkow
parents: 69045
diff changeset
   838
69592
6f755e3cd95d mixfix annotations may use cartouches;
wenzelm
parents: 69579
diff changeset
   839
* Mixfix annotations may use cartouches instead of old-style double
69598
9171d1ce5a35 support for "isabelle update -u mixfix_cartouches";
wenzelm
parents: 69597
diff changeset
   840
quotes, e.g. (infixl \<open>+\<close> 60). The command-line tool "isabelle update -u
9171d1ce5a35 support for "isabelle update -u mixfix_cartouches";
wenzelm
parents: 69597
diff changeset
   841
mixfix_cartouches" allows to update existing theory sources
9171d1ce5a35 support for "isabelle update -u mixfix_cartouches";
wenzelm
parents: 69597
diff changeset
   842
automatically.
69592
6f755e3cd95d mixfix annotations may use cartouches;
wenzelm
parents: 69579
diff changeset
   843
69221
1a52baa70aed clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents: 69218
diff changeset
   844
* ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation')
1a52baa70aed clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents: 69218
diff changeset
   845
need to provide a closed expression -- without trailing semicolon. Minor
1a52baa70aed clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents: 69218
diff changeset
   846
INCOMPATIBILITY.
1a52baa70aed clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents: 69218
diff changeset
   847
70239
0403b5127da1 documentation for generated files;
wenzelm
parents: 70214
diff changeset
   848
* Commands 'generate_file', 'export_generated_files', and
0403b5127da1 documentation for generated files;
wenzelm
parents: 70214
diff changeset
   849
'compile_generated_files' support a stateless (PIDE-conformant) model
0403b5127da1 documentation for generated files;
wenzelm
parents: 70214
diff changeset
   850
for generated sources and compiled binaries of other languages. The
70242
wenzelm
parents: 70239
diff changeset
   851
compilation process is managed in Isabelle/ML, and results exported to
70239
0403b5127da1 documentation for generated files;
wenzelm
parents: 70214
diff changeset
   852
the session database for further use (e.g. with "isabelle export" or
0403b5127da1 documentation for generated files;
wenzelm
parents: 70214
diff changeset
   853
"isabelle build -e").
0403b5127da1 documentation for generated files;
wenzelm
parents: 70214
diff changeset
   854
69042
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   855
69190
wenzelm
parents: 69184
diff changeset
   856
*** Isabelle/jEdit Prover IDE ***
wenzelm
parents: 69184
diff changeset
   857
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   858
* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   859
DejaVu" collection by default, which provides uniform rendering quality
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   860
with the usual Isabelle symbols. Line spacing no longer needs to be
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   861
adjusted: properties for the old IsabelleText font had "Global Options /
70251
381035c03220 proper default;
wenzelm
parents: 70250
diff changeset
   862
Text Area / Extra vertical line spacing (in pixels): -2", it now
381035c03220 proper default;
wenzelm
parents: 70250
diff changeset
   863
defaults to 1, but 0 works as well.
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   864
69796
wenzelm
parents: 69794
diff changeset
   865
* The jEdit File Browser is more prominent in the default GUI layout of
wenzelm
parents: 69794
diff changeset
   866
Isabelle/jEdit: various virtual file-systems provide access to Isabelle
wenzelm
parents: 69794
diff changeset
   867
resources, notably via "favorites:" (or "Edit Favorites").
wenzelm
parents: 69794
diff changeset
   868
70243
5b75480f371a more NEWS;
wenzelm
parents: 70242
diff changeset
   869
* Further markup and rendering for "plain text" (e.g. informal prose)
5b75480f371a more NEWS;
wenzelm
parents: 70242
diff changeset
   870
and "raw text" (e.g. verbatim sources). This improves the visual
5b75480f371a more NEWS;
wenzelm
parents: 70242
diff changeset
   871
appearance of formal comments inside the term language, or in general
5b75480f371a more NEWS;
wenzelm
parents: 70242
diff changeset
   872
for repeated alternation of formal and informal text.
5b75480f371a more NEWS;
wenzelm
parents: 70242
diff changeset
   873
69656
83f15deb2d36 added action "isabelle-export-browser";
wenzelm
parents: 69637
diff changeset
   874
* Action "isabelle-export-browser" points the File Browser to the theory
69780
wenzelm
parents: 69771
diff changeset
   875
exports of the current buffer, based on the "isabelle-export:" virtual
wenzelm
parents: 69771
diff changeset
   876
file-system. The directory view needs to be reloaded manually to follow
wenzelm
parents: 69771
diff changeset
   877
ongoing document processing.
wenzelm
parents: 69771
diff changeset
   878
wenzelm
parents: 69771
diff changeset
   879
* Action "isabelle-session-browser" points the File Browser to session
wenzelm
parents: 69771
diff changeset
   880
information, based on the "isabelle-session:" virtual file-system. Its
wenzelm
parents: 69771
diff changeset
   881
entries are structured according to chapter / session names, the open
wenzelm
parents: 69771
diff changeset
   882
operation is redirected to the session ROOT file.
69656
83f15deb2d36 added action "isabelle-export-browser";
wenzelm
parents: 69637
diff changeset
   883
69278
wenzelm
parents: 69274
diff changeset
   884
* Support for user-defined file-formats via class isabelle.File_Format
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
   885
in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
   886
the shell function "isabelle_file_format" in etc/settings (e.g. of an
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
   887
Isabelle component).
69278
wenzelm
parents: 69274
diff changeset
   888
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   889
* System option "jedit_text_overview" allows to disable the text
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   890
overview column.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   891
70035
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   892
* Command-line options "-s" and "-u" of "isabelle jedit" override the
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   893
default for system option "system_heaps" that determines the heap
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   894
storage directory for "isabelle build". Option "-n" is now clearly
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   895
separated from option "-s".
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
   896
70291
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   897
* The Isabelle/jEdit desktop application uses the same options as
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   898
"isabelle jedit" for its internal "isabelle build" process: the implicit
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   899
option "-o system_heaps" (or "-s") has been discontinued. This reduces
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   900
the potential for surprise wrt. command-line tools.
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   901
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   902
* The official download of the Isabelle/jEdit application already
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   903
contains heap images for Isabelle/HOL within its main directory: thus
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   904
the first encounter becomes faster and more robust (e.g. when run from a
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   905
read-only directory).
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70268
diff changeset
   906
70254
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   907
* Isabelle DejaVu fonts are available with hinting by default, which is
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   908
relevant for low-resolution displays. This may be disabled via system
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   909
option "isabelle_fonts_hinted = false" in
70258
ee0b8e06b01c proper etc/preferences;
wenzelm
parents: 70254
diff changeset
   910
$ISABELLE_HOME_USER/etc/preferences -- it occasionally yields better
70254
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   911
results.
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   912
70213
wenzelm
parents: 70208
diff changeset
   913
* OpenJDK 11 has quite different font rendering, with better glyph
wenzelm
parents: 70208
diff changeset
   914
shapes and improved sub-pixel anti-aliasing. In some situations results
70254
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   915
might be *worse* than Oracle Java 8, though -- a proper HiDPI / UHD
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70251
diff changeset
   916
display is recommended.
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   917
70442
b4534d72dd22 more NEWS;
wenzelm
parents: 70421
diff changeset
   918
* OpenJDK 11 supports GTK version 2.2 and 3 (according to system
b4534d72dd22 more NEWS;
wenzelm
parents: 70421
diff changeset
   919
property jdk.gtk.version). The factory default is version 3, but
b4534d72dd22 more NEWS;
wenzelm
parents: 70421
diff changeset
   920
ISABELLE_JAVA_SYSTEM_OPTIONS includes "-Djdk.gtk.version=2.2" to make
b4534d72dd22 more NEWS;
wenzelm
parents: 70421
diff changeset
   921
this more conservative (as in Java 8). Depending on the GTK theme
b4534d72dd22 more NEWS;
wenzelm
parents: 70421
diff changeset
   922
configuration, "-Djdk.gtk.version=3" might work better or worse.
b4534d72dd22 more NEWS;
wenzelm
parents: 70421
diff changeset
   923
69190
wenzelm
parents: 69184
diff changeset
   924
70144
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   925
*** Document preparation ***
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   926
73726
8eeea9901897 more NEWS;
wenzelm
parents: 73722
diff changeset
   927
* More predefined symbols: \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (package
8eeea9901897 more NEWS;
wenzelm
parents: 73722
diff changeset
   928
"pifont").
8eeea9901897 more NEWS;
wenzelm
parents: 73722
diff changeset
   929
8eeea9901897 more NEWS;
wenzelm
parents: 73722
diff changeset
   930
* High-quality blackboard-bold symbols from font "txmia" (package
8eeea9901897 more NEWS;
wenzelm
parents: 73722
diff changeset
   931
"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>.
73714
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73699
diff changeset
   932
70144
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   933
* Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   934
are stripped from document output: the effect is to modify the semantic
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   935
presentation context or to emit markup to the PIDE document. Some
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   936
predefined markers are taken from the Dublin Core Metadata Initiative,
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   937
e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that
70466
wenzelm
parents: 70444
diff changeset
   938
can be retrieved from the document database.
70144
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   939
70325
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   940
* Old-style command tags %name are re-interpreted as markers with
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   941
proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   942
before. Potential INCOMPATIBILITY: multiple markers are composed in
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   943
canonical order, resulting in a reversed list of tags in the
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   944
presentation context.
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   945
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   946
* Marker \<^marker>\<open>tag name\<close> does not apply to the proof of a top-level goal
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   947
statement by default (e.g. 'theorem', 'lemma'). This is a subtle change
d13865c21e36 updated documentation;
wenzelm
parents: 70311
diff changeset
   948
of semantics wrt. old-style %name.
70144
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   949
70328
0cc7fe616924 more abbrevs;
wenzelm
parents: 70325
diff changeset
   950
* In Isabelle/jEdit, the string "\tag" may be completed to a "\<^marker>\<open>tag \<close>"
0cc7fe616924 more abbrevs;
wenzelm
parents: 70325
diff changeset
   951
template.
0cc7fe616924 more abbrevs;
wenzelm
parents: 70325
diff changeset
   952
70307
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70292
diff changeset
   953
* Document antiquotation option "cartouche" indicates if the output
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70292
diff changeset
   954
should be delimited as cartouche; this takes precedence over the
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70292
diff changeset
   955
analogous option "quotes".
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70292
diff changeset
   956
70308
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   957
* Many document antiquotations are internally categorized as "embedded"
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   958
and expect one cartouche argument, which is typically used with the
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   959
\<^control>\<open>cartouche\<close> notation (e.g. \<^term>\<open>\<lambda>x y. x\<close>). The cartouche
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   960
delimiters are stripped in output of the source (antiquotation option
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   961
"source"), but it is possible to enforce delimiters via option
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   962
"source_cartouche", e.g. @{term [source_cartouche] \<open>\<lambda>x y. x\<close>}.
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   963
70144
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 70142
diff changeset
   964
68879
wenzelm
parents: 68848
diff changeset
   965
*** Isar ***
wenzelm
parents: 68848
diff changeset
   966
69045
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
   967
* Implicit cases goal1, goal2, goal3, etc. have been discontinued
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
   968
(legacy feature since Isabelle2016).
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
   969
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   970
* More robust treatment of structural errors: begin/end blocks take
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   971
precedence over goal/proof. This is particularly relevant for the
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   972
headless PIDE session and server.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   973
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   974
* Command keywords of kind thy_decl / thy_goal may be more specifically
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   975
fit into the traditional document model of "definition-statement-proof"
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   976
via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
   977
69045
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
   978
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   979
*** HOL ***
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   980
70191
435fb018e8ee "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents: 70144
diff changeset
   981
* Command 'export_code' produces output as logical files within the
70193
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   982
theory context, as well as formal session exports that can be
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   983
materialized via command-line tools "isabelle export" or "isabelle build
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   984
-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   985
provides a virtual file-system "isabelle-export:" that can be explored
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   986
in the regular file-browser. A 'file_prefix' argument allows to specify
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   987
an explicit name prefix for the target file (SML, OCaml, Scala) or
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   988
directory (Haskell); the default is "export" with a consecutive number
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   989
within each theory.
70191
435fb018e8ee "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents: 70144
diff changeset
   990
435fb018e8ee "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents: 70144
diff changeset
   991
* Command 'export_code': the 'file' argument is now legacy and will be
435fb018e8ee "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents: 70144
diff changeset
   992
removed soon: writing to the physical file-system is not well-defined in
70193
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   993
a reactive/parallel application like Isabelle. The empty 'file' argument
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   994
has been discontinued already: it is superseded by the file-browser in
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70191
diff changeset
   995
Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.
69637
e02bdf853a4c optional code export as theory export
haftmann
parents: 69622
diff changeset
   996
70204
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70193
diff changeset
   997
* Command 'code_reflect' no longer supports the 'file' argument: it has
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70193
diff changeset
   998
been superseded by 'file_prefix' for stateless file management as in
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70193
diff changeset
   999
'export_code'. Minor INCOMPATIBILITY.
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70193
diff changeset
  1000
69759
6a9a8ef5e4c6 prefer proper strings in OCaml
haftmann
parents: 69749
diff changeset
  1001
* Code generation for OCaml: proper strings are used for literals.
6a9a8ef5e4c6 prefer proper strings in OCaml
haftmann
parents: 69749
diff changeset
  1002
Minor INCOMPATIBILITY.
6a9a8ef5e4c6 prefer proper strings in OCaml
haftmann
parents: 69749
diff changeset
  1003
70108
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
  1004
* Code generation for OCaml: Zarith supersedes Nums as library for
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
  1005
proper integer arithmetic. The library is located via standard
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
  1006
invocations of "ocamlfind" (via ISABELLE_OCAMLFIND settings variable).
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
  1007
The environment provided by "isabelle ocaml_setup" already contains this
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
  1008
tool and the required packages. Minor INCOMPATIBILITY.
70087
55534affe445 migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents: 70084
diff changeset
  1009
69705
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69686
diff changeset
  1010
* Code generation for Haskell: code includes for Haskell must contain
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69686
diff changeset
  1011
proper module frame, nothing is added magically any longer.
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69686
diff changeset
  1012
INCOMPATIBILITY.
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69686
diff changeset
  1013
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1014
* Code generation: slightly more conventional syntax for 'code_stmts'
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1015
antiquotation. Minor INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1016
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1017
* Theory List: the precedence of the list_update operator has changed:
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1018
"f a [n := x]" now needs to be written "(f a)[n := x]".
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1019
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1020
* The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter> (not the corresponding binding operators)
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1021
now have the same precedence as any other prefix function symbol. Minor
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1022
INCOMPATIBILITY.
70042
62e47f06d22c avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents: 70035
diff changeset
  1023
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
  1024
* 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
  1025
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
  1026
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
  1027
SUPREMUM, UNION, INTER should now rarely occur in output and are just
70421
7e9269c188d6 more NEWS
haftmann
parents: 70400
diff changeset
  1028
retained as migration auxiliary. Abbreviations MINIMUM and MAXIMUM
7e9269c188d6 more NEWS
haftmann
parents: 70400
diff changeset
  1029
are gone INCOMPATIBILITY.
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
  1030
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1031
* The simplifier uses image_cong_simp as a congruence rule. The historic
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1032
and not really well-formed congruence rules INF_cong*, SUP_cong*, are
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1033
not used by default any longer. INCOMPATIBILITY; consider using declare
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1034
image_cong_simp [cong del] in extreme situations.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1035
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1036
* INF_image and SUP_image are no default simp rules any longer.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1037
INCOMPATIBILITY, prefer image_comp as simp rule if needed.
68938
a0b19a163f5e left-over rename from 3f9bb52082c4
haftmann
parents: 68883
diff changeset
  1038
69164
74f1b0f10b2b uniform naming of strong congruence rules
nipkow
parents: 69155
diff changeset
  1039
* Strong congruence rules (with =simp=> in the premises) for constant f
69558
27dae626822b prefer naming convention from datatype package for strong congruence rules
haftmann
parents: 69518
diff changeset
  1040
are now uniformly called f_cong_simp, in accordance with congruence
27dae626822b prefer naming convention from datatype package for strong congruence rules
haftmann
parents: 69518
diff changeset
  1041
rules produced for mappers by the datatype package. INCOMPATIBILITY.
69164
74f1b0f10b2b uniform naming of strong congruence rules
nipkow
parents: 69155
diff changeset
  1042
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1043
* Retired lemma card_Union_image; use the simpler card_UN_disjoint
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1044
instead. INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1045
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1046
* Facts sum_mset.commute and prod_mset.commute have been renamed to
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1047
sum_mset.swap and prod_mset.swap, similarly to sum.swap and prod.swap.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1048
INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1049
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1050
* ML structure Inductive: slightly more conventional naming schema.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1051
Minor INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1052
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1053
* ML: Various _global variants of specification tools have been removed.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1054
Minor INCOMPATIBILITY, prefer combinators
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1055
Named_Target.theory_map[_result] to lift specifications to the global
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1056
theory level.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1057
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1058
* Theory HOL-Library.Simps_Case_Conv: 'case_of_simps' now supports
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1059
overlapping and non-exhaustive patterns and handles arbitrarily nested
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1060
patterns. It uses on the same algorithm as HOL-Library.Code_Lazy, which
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1061
assumes sequential left-to-right pattern matching. The generated
69569
de09a7261120 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents: 69518
diff changeset
  1062
equation no longer tuples the arguments on the right-hand side.
de09a7261120 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents: 69518
diff changeset
  1063
INCOMPATIBILITY.
de09a7261120 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents: 69518
diff changeset
  1064
70482
wenzelm
parents: 70466
diff changeset
  1065
* Theory HOL-Library.Multiset: the \<Union># operator now has the same
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1066
precedence as any other prefix function symbol.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1067
70263
traytel
parents: 70258
diff changeset
  1068
* Theory HOL-Library.Cardinal_Notations has been discontinued in favor
70352
e79bbf86a984 tuned for release;
wenzelm
parents: 70348
diff changeset
  1069
of the bundle cardinal_syntax (available in theory Main). Minor
e79bbf86a984 tuned for release;
wenzelm
parents: 70348
diff changeset
  1070
INCOMPATIBILITY.
70263
traytel
parents: 70258
diff changeset
  1071
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1072
* Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring,
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1073
used for computing powers in class "monoid_mult" and modular
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1074
exponentiation.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1075
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1076
* Session HOL-Computational_Algebra: Formal Laurent series and overhaul
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1077
of Formal power series.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1078
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1079
* Session HOL-Number_Theory: More material on residue rings in
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1080
Carmichael's function, primitive roots, more properties for "ord".
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1081
70300
b601c2c87076 type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents: 70292
diff changeset
  1082
* Session HOL-Analysis: Better organization and much more material
b601c2c87076 type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents: 70292
diff changeset
  1083
at the level of abstract topological spaces.
b601c2c87076 type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents: 70292
diff changeset
  1084
70348
1f163f772da3 Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)
paulson <lp15@cam.ac.uk>
parents: 70328
diff changeset
  1085
* Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
70400
8371a25ca177 Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents: 70359
diff changeset
  1086
 algebraic closure of a field by de Vilhena and Baillon.
70214
0674c24afc5e updated for release;
wenzelm
parents: 70213
diff changeset
  1087
70352
e79bbf86a984 tuned for release;
wenzelm
parents: 70348
diff changeset
  1088
* Session HOL-Homology has been added. It is a port of HOL Light's
e79bbf86a984 tuned for release;
wenzelm
parents: 70348
diff changeset
  1089
homology library, with new proofs of "invariance of domain" and related
e79bbf86a984 tuned for release;
wenzelm
parents: 70348
diff changeset
  1090
results.
e79bbf86a984 tuned for release;
wenzelm
parents: 70348
diff changeset
  1091
69099
d44cb8a3e5e0 HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents: 69095
diff changeset
  1092
* Session HOL-SPARK: .prv files are no longer written to the
d44cb8a3e5e0 HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents: 69095
diff changeset
  1093
file-system, but exported to the session database. Results may be
70208
6ae9505d693a more convenient export;
wenzelm
parents: 70205
diff changeset
  1094
retrieved via "isabelle build -e HOL-SPARK-Examples" on the
6ae9505d693a more convenient export;
wenzelm
parents: 70205
diff changeset
  1095
command-line.
69099
d44cb8a3e5e0 HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents: 69095
diff changeset
  1096
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1097
* Sledgehammer:
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1098
  - The URL for SystemOnTPTP, which is used by remote provers, has been
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1099
    updated.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1100
  - The machine-learning-based filter MaSh has been optimized to take
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1101
    less time (in most cases).
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1102
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1103
* SMT: reconstruction is now possible using the SMT solver veriT.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1104
70358
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70352
diff changeset
  1105
* Session HOL-Word:
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70352
diff changeset
  1106
  * New theory More_Word as comprehensive entrance point.
70359
85fb1a585f52 eliminated type class
haftmann
parents: 70358
diff changeset
  1107
  * Merged type class bitss into type class bits.
70358
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70352
diff changeset
  1108
  INCOMPATIBILITY.
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70352
diff changeset
  1109
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
  1110
68804
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
  1111
*** ML ***
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
  1112
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1113
* Command 'generate_file' allows to produce sources for other languages,
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1114
with antiquotations in the Isabelle context (only the control-cartouche
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1115
form). The default "cartouche" antiquotation evaluates an ML expression
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1116
of type string and inlines the result as a string literal of the target
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1117
language. For example, this works for Haskell as follows:
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1118
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1119
  generate_file "Pure.hs" = \<open>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1120
  module Isabelle.Pure where
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1121
    allConst, impConst, eqConst :: String
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1122
    allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1123
    impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1124
    eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1125
  \<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1126
70268
4f936de6d9b8 tuned -- prefer Isar command 'compile_generated_files';
wenzelm
parents: 70263
diff changeset
  1127
See also commands 'export_generated_files' and 'compile_generated_files'
4f936de6d9b8 tuned -- prefer Isar command 'compile_generated_files';
wenzelm
parents: 70263
diff changeset
  1128
to use the results.
68804
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
  1129
70444
22cfcfcadd8b more documentation;
wenzelm
parents: 70442
diff changeset
  1130
* ML evaluation (notably via command 'ML' or 'ML_file') is subject to
68824
7414ce0256e1 some NEWS (instead of proper documentation);
wenzelm
parents: 68804
diff changeset
  1131
option ML_environment to select a named environment, such as "Isabelle"
70444
22cfcfcadd8b more documentation;
wenzelm
parents: 70442
diff changeset
  1132
for Isabelle/ML, or "SML" for official Standard ML.
68804
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
  1133
69391
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69387
diff changeset
  1134
* ML antiquotation @{master_dir} refers to the master directory of the
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69387
diff changeset
  1135
underlying theory, i.e. the directory of the theory file.
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69387
diff changeset
  1136
69481
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69391
diff changeset
  1137
* ML antiquotation @{verbatim} inlines its argument as string literal,
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69391
diff changeset
  1138
preserving newlines literally. The short form \<^verbatim>\<open>abc\<close> is particularly
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69391
diff changeset
  1139
useful.
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69391
diff changeset
  1140
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1141
* Local_Theory.reset is no longer available in user space. Regular
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1142
definitional packages should use balanced blocks of
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1143
Local_Theory.open_target versus Local_Theory.close_target instead, or
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1144
the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1145
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1146
* Original PolyML.pointerEq is retained as a convenience for tools that
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1147
don't use Isabelle/ML (where this is called "pointer_eq").
69391
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69387
diff changeset
  1148
69287
94fa3376ba33 added ML antiquotation @{master_dir};
wenzelm
parents: 69282
diff changeset
  1149
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
  1150
*** System ***
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
  1151
70213
wenzelm
parents: 70208
diff changeset
  1152
* Update to OpenJDK 11: the current long-term support version of Java.
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1153
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1154
* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1155
the full overhead of 64-bit values everywhere. This special x86_64_32
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1156
mode provides up to 16GB ML heap, while program code and stacks are
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1157
allocated elsewhere. Thus approx. 5 times more memory is available for
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1158
applications compared to old x86 mode (which is no longer used by
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1159
Isabelle). The switch to the x86_64 CPU architecture also avoids
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1160
compatibility problems with Linux and macOS, where 32-bit applications
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1161
are gradually phased out.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1162
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1163
* System option "checkpoint" has been discontinued: obsolete thanks to
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1164
improved memory management in Poly/ML.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1165
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1166
* System option "system_heaps" determines where to store the session
70035
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
  1167
image of "isabelle build" (and other tools using that internally).
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
  1168
Former option "-s" is superseded by option "-o system_heaps".
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
  1169
INCOMPATIBILITY in command-line syntax.
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 70010
diff changeset
  1170
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1171
* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1172
source modules for Isabelle tools implemented in Haskell, notably for
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1173
Isabelle/PIDE.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1174
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1175
* The command-line tool "isabelle build -e" retrieves theory exports
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1176
from the session build database, using 'export_files' in session ROOT
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1177
entries.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1178
69597
wenzelm
parents: 69592
diff changeset
  1179
* The command-line tool "isabelle update" uses Isabelle/PIDE in
wenzelm
parents: 69592
diff changeset
  1180
batch-mode to update theory sources based on semantic markup produced in
69622
wenzelm
parents: 69604
diff changeset
  1181
Isabelle/ML. Actual updates depend on system options that may be enabled
69600
wenzelm
parents: 69598
diff changeset
  1182
via "-u OPT" (for "update_OPT"), see also $ISABELLE_HOME/etc/options
wenzelm
parents: 69598
diff changeset
  1183
section "Theory update". Theory sessions are specified as in "isabelle
69597
wenzelm
parents: 69592
diff changeset
  1184
dump".
wenzelm
parents: 69592
diff changeset
  1185
69604
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69600
diff changeset
  1186
* The command-line tool "isabelle update -u control_cartouches" changes
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69600
diff changeset
  1187
antiquotations into control-symbol format (where possible): @{NAME}
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69600
diff changeset
  1188
becomes \<^NAME> and @{NAME ARG} becomes \<^NAME>\<open>ARG\<close>.
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69600
diff changeset
  1189
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
  1190
* Support for Isabelle command-line tools defined in Isabelle/Scala.
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
  1191
Instances of class Isabelle_Scala_Tools may be configured via the shell
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
  1192
function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
  1193
component).
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69278
diff changeset
  1194
70205
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70204
diff changeset
  1195
* Isabelle Server command "use_theories" supports "nodes_status_delay"
69044
wenzelm
parents: 69042
diff changeset
  1196
for continuous output of node status information. The time interval is
wenzelm
parents: 69042
diff changeset
  1197
specified in seconds; a negative value means it is disabled (default).
wenzelm
parents: 69042
diff changeset
  1198
wenzelm
parents: 69042
diff changeset
  1199
* Isabelle Server command "use_theories" terminates more robustly in the
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
  1200
presence of structurally broken sources: full consolidation of theories
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
  1201
is no longer required.
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
  1202
70108
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
  1203
* OCaml tools and libraries are now accesed via ISABELLE_OCAMLFIND,
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
  1204
which needs to point to a suitable version of "ocamlfind" (e.g. via
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
  1205
OPAM, see below). INCOMPATIBILITY: settings variables ISABELLE_OCAML and
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
  1206
ISABELLE_OCAMLC are no longer supported.
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
  1207
69273
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1208
* Support for managed installations of Glasgow Haskell Compiler and
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1209
OCaml via the following command-line tools:
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1210
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1211
  isabelle ghc_setup
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1212
  isabelle ghc_stack
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1213
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1214
  isabelle ocaml_setup
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1215
  isabelle ocaml_opam
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1216
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1217
The global installation state is determined by the following settings
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1218
(and corresponding directory contents):
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1219
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1220
  ISABELLE_STACK_ROOT
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1221
  ISABELLE_STACK_RESOLVER
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1222
  ISABELLE_GHC_VERSION
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1223
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1224
  ISABELLE_OPAM_ROOT
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1225
  ISABELLE_OCAML_VERSION
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1226
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1227
After setup, the following Isabelle settings are automatically
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1228
redirected (overriding existing user settings):
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1229
69274
1bee990d443c tuned whitespace;
wenzelm
parents: 69273
diff changeset
  1230
  ISABELLE_GHC
1bee990d443c tuned whitespace;
wenzelm
parents: 69273
diff changeset
  1231
70108
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
  1232
  ISABELLE_OCAMLFIND
69273
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1233
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1234
The old meaning of these settings as locally installed executables may
c1a27fce2076 clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents: 69235
diff changeset
  1235
be recovered by purging the directories ISABELLE_STACK_ROOT /
70108
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
  1236
ISABELLE_OPAM_ROOT, or by resetting these variables in
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 70096
diff changeset
  1237
$ISABELLE_HOME_USER/etc/settings.
69190
wenzelm
parents: 69184
diff changeset
  1238
70002
8c587dd44f51 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents: 69990
diff changeset
  1239
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
  1240
68392
9b4f60bdad54 updated for release;
wenzelm
parents: 68373
diff changeset
  1241
New in Isabelle2018 (August 2018)
9b4f60bdad54 updated for release;
wenzelm
parents: 68373
diff changeset
  1242
---------------------------------
66653
435cb8d69e27 back to post-release mode -- after fork point;
wenzelm
parents: 66652
diff changeset
  1243
66712
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 66690
diff changeset
  1244
*** General ***
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 66690
diff changeset
  1245
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1246
* Session-qualified theory names are mandatory: it is no longer possible
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1247
to refer to unqualified theories from the parent session.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1248
INCOMPATIBILITY for old developments that have not been updated to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1249
Isabelle2017 yet (using the "isabelle imports" tool).
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1250
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1251
* Only the most fundamental theory names are global, usually the entry
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1252
points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1253
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1254
formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1255
68559
7aae213d9e69 discontinued pending_shyps: too much complication due to lazy facts;
wenzelm
parents: 68548
diff changeset
  1256
* Global facts need to be closed: no free variables and no hypotheses.
7aae213d9e69 discontinued pending_shyps: too much complication due to lazy facts;
wenzelm
parents: 68548
diff changeset
  1257
Rare INCOMPATIBILITY.
68540
000a0e062529 disallow pending hyps;
wenzelm
parents: 68523
diff changeset
  1258
68665
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
  1259
* Facts stemming from locale interpretation are subject to lazy
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
  1260
evaluation for improved performance. Rare INCOMPATIBILITY: errors
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
  1261
stemming from interpretation morphisms might be deferred and thus
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
  1262
difficult to locate; enable system option "strict_facts" temporarily to
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
  1263
avoid this.
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
  1264
67446
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
  1265
* Marginal comments need to be written exclusively in the new-style form
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
  1266
"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
  1267
supported. INCOMPATIBILITY, use the command-line tool "isabelle
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
  1268
update_comments" to update existing theory files.
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
  1269
67507
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
  1270
* Old-style inner comments (* ... *) within the term language are legacy
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
  1271
and will be discontinued soon: use formal comments "\<comment> \<open>...\<close>" or "\<^cancel>\<open>...\<close>"
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
  1272
instead.
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
  1273
67402
nipkow
parents: 67400
diff changeset
  1274
* The "op <infix-op>" syntax for infix operators has been replaced by
67400
nipkow
parents: 67398
diff changeset
  1275
"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
nipkow
parents: 67398
diff changeset
  1276
be a space between the "*" and the corresponding parenthesis.
68543
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1277
INCOMPATIBILITY, use the command-line tool "isabelle update_op" to
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1278
convert theory and ML files to the new syntax. Because it is based on
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1279
regular expression matching, the result may need a bit of manual
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1280
postprocessing. Invoking "isabelle update_op" converts all files in the
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1281
current directory (recursively). In case you want to exclude conversion
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1282
of ML files (because the tool frequently also converts ML's "op"
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1283
syntax), use option "-m".
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67395
diff changeset
  1284
67013
335a7dce7cb3 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents: 66994
diff changeset
  1285
* Theory header 'abbrevs' specifications need to be separated by 'and'.
335a7dce7cb3 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents: 66994
diff changeset
  1286
INCOMPATIBILITY.
335a7dce7cb3 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents: 66994
diff changeset
  1287
66757
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
  1288
* Command 'external_file' declares the formal dependency on the given
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
  1289
file name, such that the Isabelle build process knows about it, but
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
  1290
without specific Prover IDE management.
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
  1291
66759
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
  1292
* Session ROOT entries no longer allow specification of 'files'. Rare
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
  1293
INCOMPATIBILITY, use command 'external_file' within a proper theory
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
  1294
context.
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
  1295
66764
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1296
* Session root directories may be specified multiple times: each
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1297
accessible ROOT file is processed only once. This facilitates
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1298
specification of $ISABELLE_HOME_USER/ROOTS or command-line options like
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1299
-d or -D for "isabelle build" and "isabelle jedit". Example:
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1300
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1301
  isabelle build -D '~~/src/ZF'
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1302
67264
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67263
diff changeset
  1303
* The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67263
diff changeset
  1304
use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67263
diff changeset
  1305
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1306
* In HTML output, the Isabelle symbol "\<hyphen>" is rendered as explicit
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1307
Unicode hyphen U+2010, to avoid unclear meaning of the old "soft hyphen"
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1308
U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1309
output.
67305
ecb74607063f more robust hyphen (see also "Soft hyphen (SHY) – a hard problem?" http://jkorpela.fi/shy.html);
wenzelm
parents: 67304
diff changeset
  1310
66712
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 66690
diff changeset
  1311
67262
wenzelm
parents: 67248
diff changeset
  1312
*** Isabelle/jEdit Prover IDE ***
66768
f27488f47a47 completion supports theory header imports;
wenzelm
parents: 66764
diff changeset
  1313
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1314
* The command-line tool "isabelle jedit" provides more flexible options
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1315
for session management:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1316
68472
581a1bfec8ad clarified documentation;
wenzelm
parents: 68470
diff changeset
  1317
  - option -R builds an auxiliary logic image with all theories from
581a1bfec8ad clarified documentation;
wenzelm
parents: 68470
diff changeset
  1318
    other sessions that are not already present in its parent
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1319
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1320
  - option -S is like -R, with a focus on the selected session and its
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1321
    descendants (this reduces startup time for big projects like AFP)
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1322
68472
581a1bfec8ad clarified documentation;
wenzelm
parents: 68470
diff changeset
  1323
  - option -A specifies an alternative ancestor session for options -R
581a1bfec8ad clarified documentation;
wenzelm
parents: 68470
diff changeset
  1324
    and -S
581a1bfec8ad clarified documentation;
wenzelm
parents: 68470
diff changeset
  1325
68541
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68540
diff changeset
  1326
  - option -i includes additional sessions into the name-space of
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68540
diff changeset
  1327
    theories
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68540
diff changeset
  1328
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1329
  Examples:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1330
    isabelle jedit -R HOL-Number_Theory
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1331
    isabelle jedit -R HOL-Number_Theory -A HOL
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1332
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1333
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
68541
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68540
diff changeset
  1334
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL
68394
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1335
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1336
* PIDE markup for session ROOT files: allows to complete session names,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1337
follow links to theories and document files etc.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1338
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1339
* Completion supports theory header imports, using theory base name.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1340
E.g. "Prob" may be completed to "HOL-Probability.Probability".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1341
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1342
* Named control symbols (without special Unicode rendering) are shown as
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1343
bold-italic keyword. This is particularly useful for the short form of
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1344
antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1345
"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1346
arguments into this format.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1347
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1348
* Completion provides templates for named symbols with arguments,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1349
e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68392
diff changeset
  1350
68369
wenzelm
parents: 68365
diff changeset
  1351
* Slightly more parallel checking, notably for high priority print
wenzelm
parents: 68365
diff changeset
  1352
functions (e.g. State output).
wenzelm
parents: 68365
diff changeset
  1353
68080
17f79ae49401 set view title dynamically;
wenzelm
parents: 68072
diff changeset
  1354
* The view title is set dynamically, according to the Isabelle
17f79ae49401 set view title dynamically;
wenzelm
parents: 68072
diff changeset
  1355
distribution and the logic session name. The user can override this via
17f79ae49401 set view title dynamically;
wenzelm
parents: 68072
diff changeset
  1356
set-view-title (stored persistently in $JEDIT_SETTINGS/perspective.xml).
17f79ae49401 set view title dynamically;
wenzelm
parents: 68072
diff changeset
  1357
67395
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67381
diff changeset
  1358
* System options "spell_checker_include" and "spell_checker_exclude"
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67381
diff changeset
  1359
supersede former "spell_checker_elements" to determine regions of text
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67381
diff changeset
  1360
that are subject to spell-checking. Minor INCOMPATIBILITY.
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67381
diff changeset
  1361
67248
68177abb2988 isabelle.preview presents bibtex database files as well;
wenzelm
parents: 67246
diff changeset
  1362
* Action "isabelle.preview" is able to present more file formats,
67267
wenzelm
parents: 67264
diff changeset
  1363
notably bibtex database files and ML files.
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67224
diff changeset
  1364
67263
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67262
diff changeset
  1365
* Action "isabelle.draft" is similar to "isabelle.preview", but shows a
68068
b91c4acc1aaf clarified menu actions;
wenzelm
parents: 68034
diff changeset
  1366
plain-text document draft. Both are available via the menu "Plugins /
b91c4acc1aaf clarified menu actions;
wenzelm
parents: 68034
diff changeset
  1367
Isabelle".
67263
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67262
diff changeset
  1368
67304
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
  1369
* When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
  1370
is only used if there is no conflict with existing Unicode sequences in
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
  1371
the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
  1372
symbols remain in literal \<symbol> form. This avoids accidental loss of
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
  1373
Unicode content when saving the file.
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
  1374
68545
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68543
diff changeset
  1375
* Bibtex database files (.bib) are semantically checked.
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68543
diff changeset
  1376
67994
wenzelm
parents: 67929
diff changeset
  1377
* Update to jedit-5.5.0, the latest release.
wenzelm
parents: 67929
diff changeset
  1378
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67224
diff changeset
  1379
67262
wenzelm
parents: 67248
diff changeset
  1380
*** Isabelle/VSCode Prover IDE ***
wenzelm
parents: 67248
diff changeset
  1381
wenzelm
parents: 67248
diff changeset
  1382
* HTML preview of theories and other file-formats similar to
wenzelm
parents: 67248
diff changeset
  1383
Isabelle/jEdit.
wenzelm
parents: 67248
diff changeset
  1384
68690
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
  1385
* Command-line tool "isabelle vscode_server" accepts the same options
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
  1386
-A, -R, -S, -i for session selection as "isabelle jedit". This is
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
  1387
relevant for isabelle.args configuration settings in VSCode. The former
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: