NEWS
author paulson <lp15@cam.ac.uk>
Mon, 30 Nov 2020 22:00:23 +0000
changeset 72797 402afc68f2f9
parent 72763 3cc73d00553c
child 72810 b00ee476151b
permissions -rw-r--r--
A bunch of suggestions from Pedro Sánchez Terraf
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
57491
9eedaafc05c8 tuned grammar and spelling (cf. 0cf15843b82f);
wenzelm
parents: 57476
diff changeset
     1
Isabelle NEWS -- history of user-relevant changes
9eedaafc05c8 tuned grammar and spelling (cf. 0cf15843b82f);
wenzelm
parents: 57476
diff changeset
     2
=================================================
2553
ed941505cab7 Isabelle NEWS -- history of user-visible changes;
wenzelm
parents:
diff changeset
     3
62114
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents: 62111
diff changeset
     4
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
60006
wenzelm
parents: 59998
diff changeset
     5
64603
a7f5e59378f7 tuned whitespace;
wenzelm
parents: 64602
diff changeset
     6
71557
61ba52af28e3 back to post-release mode;
wenzelm
parents: 71551
diff changeset
     7
New in this Isabelle version
61ba52af28e3 back to post-release mode;
wenzelm
parents: 71551
diff changeset
     8
----------------------------
61ba52af28e3 back to post-release mode;
wenzelm
parents: 71551
diff changeset
     9
72232
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
    10
*** General ***
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
    11
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
    12
* Proof method "subst" is confined to the original subgoal range: its
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
    13
included distinct_subgoals_tac no longer affects unrelated subgoals.
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
    14
Rare INCOMPATIBILITY.
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
    15
e5fcbf6dc687 proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents: 72208
diff changeset
    16
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 71927
diff changeset
    17
*** Isabelle/jEdit Prover IDE ***
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 71927
diff changeset
    18
72299
0c7a74a1c6d9 clarified defaults for nitpick;
wenzelm
parents: 72292
diff changeset
    19
* Auto nitpick is enabled by default: it is now reasonably fast due to
0c7a74a1c6d9 clarified defaults for nitpick;
wenzelm
parents: 72292
diff changeset
    20
Kodkod invocation within Isabelle/Scala.
0c7a74a1c6d9 clarified defaults for nitpick;
wenzelm
parents: 72292
diff changeset
    21
72249
4bf8a8a2d2ad more uniform JVM vs. ML status widget;
wenzelm
parents: 72247
diff changeset
    22
* The jEdit status line includes widgets both for JVM and ML heap usage.
4bf8a8a2d2ad more uniform JVM vs. ML status widget;
wenzelm
parents: 72247
diff changeset
    23
Ongoing ML ongoing garbage collection is shown as "ML cleanup".
72150
510ebf846696 more documentation;
wenzelm
parents: 72120
diff changeset
    24
510ebf846696 more documentation;
wenzelm
parents: 72120
diff changeset
    25
* The Monitor dockable provides buttons to request a full garbage
510ebf846696 more documentation;
wenzelm
parents: 72120
diff changeset
    26
collection and sharing of live data on the ML heap. It also includes
510ebf846696 more documentation;
wenzelm
parents: 72120
diff changeset
    27
information about the Java Runtime system.
510ebf846696 more documentation;
wenzelm
parents: 72120
diff changeset
    28
72247
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 72232
diff changeset
    29
* Update to jedit-5.6.0, the latest release. This version works properly
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 72232
diff changeset
    30
on macOS by default, without the special MacOSX plugin.
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 71927
diff changeset
    31
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 71927
diff changeset
    32
71902
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 71901
diff changeset
    33
*** Document preparation ***
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 71901
diff changeset
    34
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72581
diff changeset
    35
* Keyword 'document_theories' within ROOT specifies theories from other
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72581
diff changeset
    36
sessions that should be included in the generated document source
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72581
diff changeset
    37
directory. This does not affect the generated session.tex: \input{...}
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72581
diff changeset
    38
needs to be used separately.
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72581
diff changeset
    39
72314
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
    40
* The standard LaTeX engine is now lualatex, according to settings
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
    41
variable ISABELLE_PDFLATEX. This is mostly upwards compatible with old
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
    42
pdflatex, but text encoding needs to conform strictly to utf8. Rare
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
    43
INCOMPATIBILITY.
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
    44
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
    45
* Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
    46
document output is always PDF.
684f14b1e7fc ISABELLE_PDFLATEX is now lualatex;
wenzelm
parents: 72309
diff changeset
    47
72763
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72749
diff changeset
    48
* Antiquotation @{tool} refers to Isabelle command-line tools, with
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72749
diff changeset
    49
completion and formal reference to the source (external script or
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72749
diff changeset
    50
internal Scala function).
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72749
diff changeset
    51
71908
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
    52
* Antiquotation @{bash_function} refers to GNU bash functions that are
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
    53
checked within the Isabelle settings environment.
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
    54
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
    55
* Antiquotations @{scala}, @{scala_object}, @{scala_type},
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
    56
@{scala_method} refer to checked Isabelle/Scala entities.
71902
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 71901
diff changeset
    57
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 71901
diff changeset
    58
71901
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
    59
*** Pure ***
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
    60
71924
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents: 71923
diff changeset
    61
* Session Pure-Examples contains notable examples for Isabelle/Pure
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents: 71923
diff changeset
    62
(former entries of HOL-Isar_Examples).
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents: 71923
diff changeset
    63
72739
e7c2848b78e8 refined syntax for bundle mixins for locale and class specifications
haftmann
parents: 72728
diff changeset
    64
* Named contexts (locale and class specifications, locale and class
e7c2848b78e8 refined syntax for bundle mixins for locale and class specifications
haftmann
parents: 72728
diff changeset
    65
context blocks) allow bundle mixins for the surface context.  This
e7c2848b78e8 refined syntax for bundle mixins for locale and class specifications
haftmann
parents: 72728
diff changeset
    66
allows syntax notations to be organized within bundles conveniently.
e7c2848b78e8 refined syntax for bundle mixins for locale and class specifications
haftmann
parents: 72728
diff changeset
    67
See src/HOL/ex/Specifications_with_bundle_mixins.thy for examples
e7c2848b78e8 refined syntax for bundle mixins for locale and class specifications
haftmann
parents: 72728
diff changeset
    68
and the Isar reference manual for syntx descriptions.
e7c2848b78e8 refined syntax for bundle mixins for locale and class specifications
haftmann
parents: 72728
diff changeset
    69
71901
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
    70
* Definitions in locales produce rule which can be added as congruence
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
    71
rule to protect foundational terms during simplification.
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
    72
72450
24bd1316eaae consolidated names and operations
haftmann
parents: 72388
diff changeset
    73
* Consolidated terminology and function signatures for nested targets:
24bd1316eaae consolidated names and operations
haftmann
parents: 72388
diff changeset
    74
24bd1316eaae consolidated names and operations
haftmann
parents: 72388
diff changeset
    75
  * Local_Theory.begin_nested replaces Local_Theory.open_target.
24bd1316eaae consolidated names and operations
haftmann
parents: 72388
diff changeset
    76
24bd1316eaae consolidated names and operations
haftmann
parents: 72388
diff changeset
    77
  * Local_Theory.end_nested replaces Local_Theory.close_target.
24bd1316eaae consolidated names and operations
haftmann
parents: 72388
diff changeset
    78
72451
e51f1733618d replaced combinators by more conventional nesting pattern
haftmann
parents: 72450
diff changeset
    79
  * Combination of Local_Theory.begin_nested and
e51f1733618d replaced combinators by more conventional nesting pattern
haftmann
parents: 72450
diff changeset
    80
    Local_Theory.end_nested(_result) replaces
e51f1733618d replaced combinators by more conventional nesting pattern
haftmann
parents: 72450
diff changeset
    81
    Local_Theory.subtarget(_result).
e51f1733618d replaced combinators by more conventional nesting pattern
haftmann
parents: 72450
diff changeset
    82
72450
24bd1316eaae consolidated names and operations
haftmann
parents: 72388
diff changeset
    83
INCOMPATIBILITY.
24bd1316eaae consolidated names and operations
haftmann
parents: 72388
diff changeset
    84
72516
17dc99589a91 unified Local_Theory.init with Generic_Target.init
haftmann
parents: 72515
diff changeset
    85
* Local_Theory.init replaces Generic_Target.init.  Minor INCOMPATIBILITY.
17dc99589a91 unified Local_Theory.init with Generic_Target.init
haftmann
parents: 72515
diff changeset
    86
71901
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
    87
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
    88
*** HOL ***
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
    89
72478
b452242dce36 proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents: 72470
diff changeset
    90
* An updated version of the veriT solver is now included as Isabelle
b452242dce36 proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents: 72470
diff changeset
    91
component. It can be used in the "smt" proof method via "smt (verit)" or
b452242dce36 proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents: 72470
diff changeset
    92
via "declare [[smt_solver = verit]]" in the context; see also session
b452242dce36 proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents: 72470
diff changeset
    93
HOL-Word-SMT_Examples.
b452242dce36 proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents: 72470
diff changeset
    94
72208
wenzelm
parents: 72163
diff changeset
    95
* Nitpick/Kodkod may be invoked directly within the running
wenzelm
parents: 72163
diff changeset
    96
Isabelle/Scala session (instead of an external Java process): this
wenzelm
parents: 72163
diff changeset
    97
improves reactivity and saves resources. This experimental feature is
72299
0c7a74a1c6d9 clarified defaults for nitpick;
wenzelm
parents: 72292
diff changeset
    98
guarded by system option "kodkod_scala" (default: true).
72208
wenzelm
parents: 72163
diff changeset
    99
71927
wenzelm
parents: 71924
diff changeset
   100
* Session HOL-Examples contains notable examples for Isabelle/HOL
wenzelm
parents: 71924
diff changeset
   101
(former entries of HOL-Isar_Examples, HOL-ex etc.).
wenzelm
parents: 71924
diff changeset
   102
72070
wenzelm
parents: 72060
diff changeset
   103
* Simproc "defined_all" and rewrite rule "subst_all" perform more
wenzelm
parents: 72060
diff changeset
   104
aggressive substitution with variables from assumptions.
wenzelm
parents: 72060
diff changeset
   105
INCOMPATIBILITY, consider repairing proofs locally like this:
wenzelm
parents: 72060
diff changeset
   106
wenzelm
parents: 72060
diff changeset
   107
  supply subst_all [simp del] [[simproc del: defined_all]]
wenzelm
parents: 72060
diff changeset
   108
71901
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   109
* Simproc "datatype_no_proper_subterm" rewrites equalities "lhs = rhs"
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   110
on datatypes to "False" if either side is a proper subexpression of the
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   111
other (for any datatype with a reasonable size function).
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   112
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   113
* New constant "power_int" for exponentiation with integer exponent,
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   114
written as "x powi n".
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   115
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   116
* Added the "at most 1" quantifier, Uniq.
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   117
71941
49af3d9a818c replaced mere alias by input abbreviation
haftmann
parents: 71940
diff changeset
   118
* For the natural numbers, Sup {} = 0.
49af3d9a818c replaced mere alias by input abbreviation
haftmann
parents: 71940
diff changeset
   119
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 72001
diff changeset
   120
* Updated the Metis prover underlying the "metis" proof method to
913162a47d9f Update Metis to 2.4
desharna
parents: 72001
diff changeset
   121
  version 2.4 (release 20180810). The new version fixes one soundness
913162a47d9f Update Metis to 2.4
desharna
parents: 72001
diff changeset
   122
  defect and two incompleteness defects. Very slight INCOMPATIBILITY.
913162a47d9f Update Metis to 2.4
desharna
parents: 72001
diff changeset
   123
71956
a4bffc0de967 bit operations as distinctive library theory
haftmann
parents: 71949
diff changeset
   124
* Library theory "Bit_Operations" with generic bit operations.
a4bffc0de967 bit operations as distinctive library theory
haftmann
parents: 71949
diff changeset
   125
72281
beeadb35e357 more thorough treatment of division, particularly signed division on int and word
haftmann
parents: 72264
diff changeset
   126
* Library theory "Signed_Division" provides operations for signed
beeadb35e357 more thorough treatment of division, particularly signed division on int and word
haftmann
parents: 72264
diff changeset
   127
division, instantiated for type int.
beeadb35e357 more thorough treatment of division, particularly signed division on int and word
haftmann
parents: 72264
diff changeset
   128
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   129
* Self-contained library theory "Word" taken over from former session
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   130
"HOL-Word".
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   131
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   132
* Theory "Word": Type word is restricted to bit strings consisting
71957
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71956
diff changeset
   133
of at least one bit.  INCOMPATIBILITY.
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71956
diff changeset
   134
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   135
* Theory "Word": Bit operations NOT, AND, OR, XOR are based on
71957
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71956
diff changeset
   136
generic algebraic bit operations from HOL-Library.Bit_Operations.
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71956
diff changeset
   137
INCOMPATIBILITY.
71956
a4bffc0de967 bit operations as distinctive library theory
haftmann
parents: 71949
diff changeset
   138
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   139
* Theory "Word": Most operations on type word are set up
72079
8c355e2dd7db more consequent transferability
haftmann
parents: 72070
diff changeset
   140
for transfer and lifting.  INCOMPATIBILITY.
8c355e2dd7db more consequent transferability
haftmann
parents: 72070
diff changeset
   141
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   142
* Theory "Word": Generic type conversions.  INCOMPATIBILITY,
72263
c0a552515c29 NEWS and CONTRIBUTORS
haftmann
parents: 72249
diff changeset
   143
sometimes additional rewrite rules must be added to applications to
c0a552515c29 NEWS and CONTRIBUTORS
haftmann
parents: 72249
diff changeset
   144
get a confluent system again.
c0a552515c29 NEWS and CONTRIBUTORS
haftmann
parents: 72249
diff changeset
   145
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   146
* Theory "Word": Uniform polymorphic "mask" operation for both
72264
haftmann
parents: 72263
diff changeset
   147
types int and word.  INCOMPATIBILITY.
72082
41393ecb57ac uniform mask operation
haftmann
parents: 72079
diff changeset
   148
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   149
* Theory "Word": Syntax for signed compare operators has been
72388
633d14bd1e59 consolidated for the sake of documentation
haftmann
parents: 72332
diff changeset
   150
consolidated with syntax of regular compare operators.
633d14bd1e59 consolidated for the sake of documentation
haftmann
parents: 72332
diff changeset
   151
Minor INCOMPATIBILITY.
633d14bd1e59 consolidated for the sake of documentation
haftmann
parents: 72332
diff changeset
   152
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   153
* Former session "HOL-Word": Various operations dealing with bit values
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   154
represented as reversed lists of bools are separated into theory
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   155
Reversed_Bit_Lists in session Word_Lib in the AFP.  INCOMPATIBILITY.
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   156
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   157
* Former session "HOL-Word": Theory "Word_Bitwise" has been moved to AFP
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   158
entry Word_Lib as theory "Bitwise".  INCOMPATIBILITY.
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   159
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   160
* Former session "HOL-Word": Compound operation "bin_split" simplifies
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   161
by default into its components "drop_bit" and "take_bit".
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   162
INCOMPATIBILITY.
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   163
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   164
* Former session "HOL-Word": Operations lsb, msb and set_bit are
72546
58b1826354c9 NEWS and CONTRIBUTORS
haftmann
parents: 72521
diff changeset
   165
separated into theories Least_significant_bit, Most_significant_bit and
58b1826354c9 NEWS and CONTRIBUTORS
haftmann
parents: 72521
diff changeset
   166
Generic_set_bit respectively in session Word_Lib in the AFP.
58b1826354c9 NEWS and CONTRIBUTORS
haftmann
parents: 72521
diff changeset
   167
INCOMPATIBILITY.
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   168
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   169
* Former session "HOL-Word": Ancient int numeral representation has been
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   170
factored out in separate theory "Ancient_Numeral" in session Word_Lib
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   171
in the AFP.  INCOMPATIBILITY.
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   172
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   173
* Former session "HOL-Word": Operations "bin_last", "bin_rest",
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   174
"bin_nth", "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   175
"max_word" are now mere input abbreviations.  Minor INCOMPATIBILITY.
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   176
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   177
* Former session "HOL-Word": Misc ancient material has been factored out
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   178
into separate theories and moved to session Word_Lib in the AFP.  See
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72511
diff changeset
   179
theory "Guide" there for further information.  INCOMPATIBILITY.
71987
ec17263ec38d removed superfluous dependency
haftmann
parents: 71986
diff changeset
   180
72070
wenzelm
parents: 72060
diff changeset
   181
* Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands
wenzelm
parents: 72060
diff changeset
   182
are in working order again, as opposed to outputting "GaveUp" on nearly
wenzelm
parents: 72060
diff changeset
   183
all problems.
71959
ee2c7f0dd1be prefer single name
haftmann
parents: 71957
diff changeset
   184
72518
4be6ae020fc4 Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents: 72516
diff changeset
   185
* Sledgehammer:
4be6ae020fc4 Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents: 72516
diff changeset
   186
  - Use veriT in proof preplay.
4be6ae020fc4 Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents: 72516
diff changeset
   187
  - Take adventage of more cores in proof preplay.
4be6ae020fc4 Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents: 72516
diff changeset
   188
72581
de581f98a3a1 bundled syntax for state monad combinators
haftmann
parents: 72574
diff changeset
   189
* Syntax for state monad combinators fcomp and scomp is organized in
de581f98a3a1 bundled syntax for state monad combinators
haftmann
parents: 72574
diff changeset
   190
bundle state_combinator_syntax.  Minor INCOMPATIBILITY.
de581f98a3a1 bundled syntax for state monad combinators
haftmann
parents: 72574
diff changeset
   191
72607
feebdaa346e5 bundles for reflected term syntax
haftmann
parents: 72600
diff changeset
   192
* Syntax for reflected term syntax is organized in bundle term_syntax,
feebdaa346e5 bundles for reflected term syntax
haftmann
parents: 72600
diff changeset
   193
discontinuing previous locale term_syntax.  Minor INCOMPATIBILITY.
feebdaa346e5 bundles for reflected term syntax
haftmann
parents: 72600
diff changeset
   194
71901
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   195
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   196
*** FOL ***
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   197
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   198
* Added the "at most 1" quantifier, Uniq, as in HOL.
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   199
72070
wenzelm
parents: 72060
diff changeset
   200
* Simproc "defined_all" and rewrite rule "subst_all" have been changed
wenzelm
parents: 72060
diff changeset
   201
as in HOL.
71923
haftmann
parents: 71909
diff changeset
   202
71901
0408f6814224 misc tuning;
wenzelm
parents: 71845
diff changeset
   203
71908
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
   204
*** ML ***
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
   205
72060
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 72042
diff changeset
   206
* Theory_Data extend operation is obsolete and needs to be the identity
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 72042
diff changeset
   207
function; merge should be conservative and not reset to the empty value.
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 72042
diff changeset
   208
Subtle INCOMPATIBILITY and change of semantics (due to
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 72042
diff changeset
   209
Theory.join_theory from Isabelle2020). Special extend/merge behaviour at
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 72042
diff changeset
   210
the begin of a new theory can be achieved via Theory.at_begin.
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 72042
diff changeset
   211
72332
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72316
diff changeset
   212
* Antiquotations @{scala_function}, @{scala}, @{scala_thread} refer to
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72316
diff changeset
   213
registered Isabelle/Scala functions (of type String => String):
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72316
diff changeset
   214
invocation works via the PIDE protocol.
71908
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
   215
72511
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72510
diff changeset
   216
* Path.append is available as overloaded "+" operator, similar to
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72510
diff changeset
   217
corresponding Isabelle/Scala operation.
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72510
diff changeset
   218
71908
0dc67ae4a4c7 more NEWS;
wenzelm
parents: 71902
diff changeset
   219
71715
wenzelm
parents: 71666
diff changeset
   220
*** System ***
wenzelm
parents: 71666
diff changeset
   221
72457
wenzelm
parents: 72451
diff changeset
   222
* Update/rebuild external provers on currently supported OS platforms,
72684
dcc0022f0179 updated to cvc4-1.8;
wenzelm
parents: 72681
diff changeset
   223
notably CVC4 1.8, E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
72457
wenzelm
parents: 72451
diff changeset
   224
72309
564012e31db1 discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents: 72299
diff changeset
   225
* Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
564012e31db1 discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents: 72299
diff changeset
   226
variable.
564012e31db1 discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents: 72299
diff changeset
   227
72316
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72314
diff changeset
   228
* The command-line tool "isabelle logo" only outputs PDF; obsolete EPS
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72314
diff changeset
   229
(for DVI documents) has been discontinued. Former option -n has been
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72314
diff changeset
   230
turned into -o with explicit file name. Minor INCOMPATIBILITY.
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72314
diff changeset
   231
72162
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72150
diff changeset
   232
* The shell function "isabelle_directory" (within etc/settings of
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72150
diff changeset
   233
components) augments the list of special directories for persistent
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72150
diff changeset
   234
symbolic path names. This improves portability of heap images and
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72150
diff changeset
   235
session databases. It used to be hard-wired for Isabelle + AFP, but
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72150
diff changeset
   236
other projects may now participate on equal terms.
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 72150
diff changeset
   237
72120
wenzelm
parents: 72103
diff changeset
   238
* ML statistics via an external Poly/ML process: this allows monitoring
wenzelm
parents: 72103
diff changeset
   239
the runtime system while the ML program sleeps.
wenzelm
parents: 72103
diff changeset
   240
72681
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   241
* The command-line tool "isabelle process" now prints output to
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   242
stdout/stderr separately and incrementally, instead of just one bulk to
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   243
stdout after termination. Potential INCOMPATIBILITY for external tools.
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   244
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   245
* The command-line tool "isabelle console" now supports interrupts
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   246
properly (on Linux and macOS).
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   247
72103
7b318273a4aa discontinued old batch-build functionality;
wenzelm
parents: 72088
diff changeset
   248
* Batch-builds via "isabelle build" use a PIDE session with special
7b318273a4aa discontinued old batch-build functionality;
wenzelm
parents: 72088
diff changeset
   249
protocol: this allows to invoke Isabelle/Scala operations from
7b318273a4aa discontinued old batch-build functionality;
wenzelm
parents: 72088
diff changeset
   250
Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for the
7b318273a4aa discontinued old batch-build functionality;
wenzelm
parents: 72088
diff changeset
   251
java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings:
71976
80d7f004089d clarified NEWS;
wenzelm
parents: 71975
diff changeset
   252
80d7f004089d clarified NEWS;
wenzelm
parents: 71975
diff changeset
   253
  ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx8g"
71975
2d658beb815b enable pide_session by default (again), with extra JVM heap for AFP tests (see also 86e429abd38d, 026de3424c39);
wenzelm
parents: 71964
diff changeset
   254
72728
caa182bdab7a clarified options: batch-build has pide_reports disabled by default (requires significant resources);
wenzelm
parents: 72684
diff changeset
   255
This includes full PIDE markup, if option "build_pide_reports" is
caa182bdab7a clarified options: batch-build has pide_reports disabled by default (requires significant resources);
wenzelm
parents: 72684
diff changeset
   256
enabled.
caa182bdab7a clarified options: batch-build has pide_reports disabled by default (requires significant resources);
wenzelm
parents: 72684
diff changeset
   257
72679
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   258
* The command-line tool "isabelle build" provides option -P DIR to
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   259
produce PDF/HTML presentation in the specified directory; -P: refers to
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   260
the standard directory according to ISABELLE_BROWSER_INFO /
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   261
ISABELLE_BROWSER_INFO_SYSTEM settings. Generated PDF documents are taken
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   262
from the build database -- from this or earlier builds with option
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   263
document=pdf.
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   264
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72557
diff changeset
   265
* The command-line tool "isabelle document" generates theory documents
72679
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   266
on the spot, using the underlying session build database (exported
72681
035b8054013a tuned NEWS;
wenzelm
parents: 72679
diff changeset
   267
LaTeX sources or existing PDF files). INCOMPATIBILITY, the former
72679
7ab733b2aecb more NEWS;
wenzelm
parents: 72678
diff changeset
   268
"isabelle document" tool was rather different and has been discontinued.
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72557
diff changeset
   269
71808
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71788
diff changeset
   270
* The command-line tool "isabelle sessions" explores the structure of
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71788
diff changeset
   271
Isabelle sessions and prints result names in topological order (on
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71788
diff changeset
   272
stdout).
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71788
diff changeset
   273
71733
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71728
diff changeset
   274
* The Isabelle/Scala "Progress" interface changed slightly and
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71728
diff changeset
   275
"No_Progress" has been discontinued. INCOMPATIBILITY, use "new Progress"
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71728
diff changeset
   276
instead.
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71728
diff changeset
   277
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71728
diff changeset
   278
* General support for Isabelle/Scala system services, configured via the
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71728
diff changeset
   279
shell function "isabelle_scala_service" in etc/settings (e.g. of an
71741
wenzelm
parents: 71736
diff changeset
   280
Isabelle component); see implementations of class
wenzelm
parents: 71736
diff changeset
   281
Isabelle_System.Service in Isabelle/Scala. This supersedes former
wenzelm
parents: 71736
diff changeset
   282
"isabelle_scala_tools" and "isabelle_file_format": minor
wenzelm
parents: 71736
diff changeset
   283
INCOMPATIBILITY.
71728
wenzelm
parents: 71715
diff changeset
   284
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   285
* The syntax of theory load commands (for auxiliary files) is now
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   286
specified in Isabelle/Scala, as instance of class
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   287
isabelle.Command_Span.Load_Command registered via isabelle_scala_service
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   288
in etc/settings. This allows more flexible schemes than just a list of
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   289
file extensions. Minor INCOMPATIBILITY, e.g. see theory
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   290
HOL-SPARK.SPARK_Setup to emulate the old behaviour.
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72728
diff changeset
   291
72163
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 72162
diff changeset
   292
* Isabelle server allows user-defined commands via
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 72162
diff changeset
   293
isabelle_scala_service.
f5722290a4d0 allow user-defined server commands via isabelle_scala_service;
wenzelm
parents: 72162
diff changeset
   294
72521
354bfab78cbf Isabelle/Phabricator supports Ubuntu 20.04 LTS;
wenzelm
parents: 72518
diff changeset
   295
* Isabelle/Phabricator supports Ubuntu 20.04 LTS.
354bfab78cbf Isabelle/Phabricator supports Ubuntu 20.04 LTS;
wenzelm
parents: 72518
diff changeset
   296
71845
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 71839
diff changeset
   297
* Isabelle/Phabricator setup has been updated to follow ongoing
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 71839
diff changeset
   298
development: libphutil has been discontinued. Minor INCOMPATIBILITY:
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 71839
diff changeset
   299
existing server installations should remove libphutil from
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 71839
diff changeset
   300
/usr/local/bin/isabelle-phabricator-upgrade and each installation root
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 71839
diff changeset
   301
directory (e.g. /var/www/phabricator-vcs/libphutil).
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 71839
diff changeset
   302
72510
wenzelm
parents: 72478
diff changeset
   303
* Experimental support for arm64-linux platform. The reference platform
wenzelm
parents: 72478
diff changeset
   304
is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
wenzelm
parents: 72478
diff changeset
   305
71557
61ba52af28e3 back to post-release mode;
wenzelm
parents: 71551
diff changeset
   306
71839
0bbe0866b7e6 The Uniq quantifier for FOL too
paulson <lp15@cam.ac.uk>
parents: 71837
diff changeset
   307
71485
29e297fd5473 updated for release;
wenzelm
parents: 71484
diff changeset
   308
New in Isabelle2020 (April 2020)
29e297fd5473 updated for release;
wenzelm
parents: 71484
diff changeset
   309
--------------------------------
70265
a8238fd25541 back to post-release mode;
wenzelm
parents: 70260
diff changeset
   310
70562
wenzelm
parents: 70525
diff changeset
   311
*** General ***
wenzelm
parents: 70525
diff changeset
   312
70677
56d70f7ce4a4 more documentation;
wenzelm
parents: 70608
diff changeset
   313
* Session ROOT files need to specify explicit 'directories' for import
70681
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70677
diff changeset
   314
of theory files. Directories cannot be shared by different sessions.
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70677
diff changeset
   315
(Recall that import of theories from other sessions works via
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70677
diff changeset
   316
session-qualified theory names, together with suitable 'sessions'
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70677
diff changeset
   317
declarations in the ROOT.)
70677
56d70f7ce4a4 more documentation;
wenzelm
parents: 70608
diff changeset
   318
70562
wenzelm
parents: 70525
diff changeset
   319
* Internal derivations record dependencies on oracles and other theorems
wenzelm
parents: 70525
diff changeset
   320
accurately, including the implicit type-class reasoning wrt. proven
wenzelm
parents: 70525
diff changeset
   321
class relations and type arities. In particular, the formal tagging with
wenzelm
parents: 70525
diff changeset
   322
"Pure.skip_proofs" of results stemming from "instance ... sorry" is now
wenzelm
parents: 70525
diff changeset
   323
propagated properly to theorems depending on such type instances.
wenzelm
parents: 70525
diff changeset
   324
wenzelm
parents: 70525
diff changeset
   325
* Command 'sorry' (oracle "Pure.skip_proofs") is more precise about the
wenzelm
parents: 70525
diff changeset
   326
actual proposition that is assumed in the goal and proof context. This
wenzelm
parents: 70525
diff changeset
   327
requires at least Proofterm.proofs = 1 to show up in theorem
wenzelm
parents: 70525
diff changeset
   328
dependencies.
wenzelm
parents: 70525
diff changeset
   329
wenzelm
parents: 70525
diff changeset
   330
* Command 'thm_oracles' prints all oracles used in given theorems,
wenzelm
parents: 70525
diff changeset
   331
covering the full graph of transitive dependencies.
wenzelm
parents: 70525
diff changeset
   332
70605
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70599
diff changeset
   333
* Command 'thm_deps' prints immediate theorem dependencies of the given
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70599
diff changeset
   334
facts. The former graph visualization has been discontinued, because it
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70599
diff changeset
   335
was hardly usable.
048cf2096186 clarified 'thm_deps' command;
wenzelm
parents: 70599
diff changeset
   336
71446
wenzelm
parents: 71438
diff changeset
   337
* Refined treatment of proof terms, including type-class proofs for
wenzelm
parents: 71438
diff changeset
   338
minor object-logics (FOL, FOLP, Sequents).
wenzelm
parents: 71438
diff changeset
   339
71448
wenzelm
parents: 71446
diff changeset
   340
* The inference kernel is now confined to one main module: structure
wenzelm
parents: 71446
diff changeset
   341
Thm, without the former circular dependency on structure Axclass.
wenzelm
parents: 71446
diff changeset
   342
71545
b0b16088ccf2 allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
wenzelm
parents: 71543
diff changeset
   343
* Mixfix annotations may use "' " (single quote followed by space) to
b0b16088ccf2 allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
wenzelm
parents: 71543
diff changeset
   344
separate delimiters (as documented in the isar-ref manual), without
71547
d350aabace23 proper escape for literal single quotes;
wenzelm
parents: 71545
diff changeset
   345
requiring an auxiliary empty block. A literal single quote needs to be
71551
wenzelm
parents: 71547
diff changeset
   346
escaped properly. Minor INCOMPATIBILITY.
71545
b0b16088ccf2 allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
wenzelm
parents: 71543
diff changeset
   347
70562
wenzelm
parents: 70525
diff changeset
   348
70522
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   349
*** Isar ***
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   350
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   351
* The proof method combinator (subproofs m) applies the method
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   352
expression m consecutively to each subgoal, constructing individual
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   353
subproofs internally. This impacts the internal construction of proof
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   354
terms: it makes a cascade of let-expressions within the derivation tree
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   355
and may thus improve scalability.
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   356
71427
wenzelm
parents: 71378
diff changeset
   357
* Attribute "trace_locales" activates tracing of locale instances during
wenzelm
parents: 71378
diff changeset
   358
roundup. It replaces the diagnostic command 'print_dependencies', which
wenzelm
parents: 71378
diff changeset
   359
has been discontinued.
70608
d997c7ba3305 Tracing of locale activation.
ballarin
parents: 70605
diff changeset
   360
70522
f2d58cafbc13 more documentation;
wenzelm
parents: 70434
diff changeset
   361
70683
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   362
*** Isabelle/jEdit Prover IDE ***
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   363
71543
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   364
* Prover IDE startup is now much faster, because theory dependencies are
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   365
no longer explored in advance. The overall session structure with its
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   366
declarations of 'directories' is sufficient to locate theory files. Thus
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   367
the "session focus" of option "isabelle jedit -S" has become obsolete
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   368
(likewise for "isabelle vscode_server -S"). Existing option "-R" is both
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   369
sufficient and more convenient to start editing a particular session.
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   370
71497
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71493
diff changeset
   371
* Actions isabelle.tooltip (CS+b) and isabelle.message (CS+m) display
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71493
diff changeset
   372
tooltip message popups, corresponding to mouse hovering with/without the
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71493
diff changeset
   373
CONTROL/COMMAND key pressed.
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71493
diff changeset
   374
71499
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71497
diff changeset
   375
* The following actions allow to navigate errors within the current
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71497
diff changeset
   376
document snapshot:
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71497
diff changeset
   377
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71497
diff changeset
   378
  isabelle.first-error (CS+a)
71505
ae3399b05e9b more documentation;
wenzelm
parents: 71499
diff changeset
   379
  isabelle.last-error (CS+z)
ae3399b05e9b more documentation;
wenzelm
parents: 71499
diff changeset
   380
  isabelle.next-error (CS+n)
ae3399b05e9b more documentation;
wenzelm
parents: 71499
diff changeset
   381
  isabelle.prev-error (CS+p)
71499
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71497
diff changeset
   382
71430
wenzelm
parents: 71429
diff changeset
   383
* Support more brackets: \<llangle> \<rrangle> (intended for implicit argument syntax).
wenzelm
parents: 71429
diff changeset
   384
71520
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71505
diff changeset
   385
* Action isabelle.jconsole (menu item Plugins / Isabelle / Java/VM
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71505
diff changeset
   386
Monitor) applies the jconsole tool on the running Isabelle/jEdit
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71505
diff changeset
   387
process. This allows to monitor resource usage etc.
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71505
diff changeset
   388
71543
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   389
* More adequate default font sizes for Linux on HD / UHD displays:
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   390
automatic font scaling is usually absent on Linux, in contrast to
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   391
Windows and macOS.
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   392
71575
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   393
* The default value for the jEdit property "view.antiAlias" (menu item
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   394
Utilities / Global Options / Text Area / Anti Aliased smooth text) is
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   395
now "subpixel HRGB", instead of former "standard". Especially on Linux
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   396
this often leads to faster text rendering, but can also cause problems
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   397
with odd color shades. An alternative is to switch back to "standard"
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   398
here, and set the following Java system property:
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   399
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   400
    isabelle jedit -Dsun.java2d.opengl=true
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   401
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   402
This can be made persistent via JEDIT_JAVA_OPTIONS in
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   403
$ISABELLE_HOME_USER/etc/settings. For the "Isabelle2020" desktop
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   404
application there is a corresponding options file in the same directory.
aff37005fd79 more NEWS;
wenzelm
parents: 71551
diff changeset
   405
70683
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   406
71473
be84312a2d53 update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents: 71448
diff changeset
   407
*** Isabelle/VSCode Prover IDE ***
be84312a2d53 update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents: 71448
diff changeset
   408
71484
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   409
* Update of State and Preview panels to use new WebviewPanel API of
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   410
VSCode.
71473
be84312a2d53 update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents: 71448
diff changeset
   411
be84312a2d53 update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents: 71448
diff changeset
   412
70337
48609a6af1a0 removed relics of ASCII syntax for indexed big operators
haftmann
parents: 70300
diff changeset
   413
*** HOL ***
48609a6af1a0 removed relics of ASCII syntax for indexed big operators
haftmann
parents: 70300
diff changeset
   414
71427
wenzelm
parents: 71378
diff changeset
   415
* Improvements of the 'lift_bnf' command:
71264
0c454a5d125d NEWS, CONTRIBUTORS, and documentation
traytel
parents: 71259
diff changeset
   416
  - Add support for quotient types.
71427
wenzelm
parents: 71378
diff changeset
   417
  - Generate transfer rules for the lifted map/set/rel/pred constants
wenzelm
parents: 71378
diff changeset
   418
    (theorems "<type>.<constant>_transfer_raw").
71264
0c454a5d125d NEWS, CONTRIBUTORS, and documentation
traytel
parents: 71259
diff changeset
   419
70784
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
   420
* Term_XML.Encode/Decode.term uses compact representation of Const
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
   421
"typargs" from the given declaration environment. This also makes more
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
   422
sense for translations to lambda-calculi with explicit polymorphism.
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
   423
INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
   424
applications.
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
   425
70524
7783bece74b4 tuned whitespace;
wenzelm
parents: 70522
diff changeset
   426
* ASCII membership syntax concerning big operators for infimum and
71427
wenzelm
parents: 71378
diff changeset
   427
supremum has been discontinued. INCOMPATIBILITY.
70524
7783bece74b4 tuned whitespace;
wenzelm
parents: 70522
diff changeset
   428
71543
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   429
* Removed multiplicativity assumption from class
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   430
"normalization_semidom". Introduced various new intermediate classes
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   431
with the multiplicativity assumption; many theorem statements
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   432
(especially involving GCD/LCM) had to be adapted. This allows for a more
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   433
natural instantiation of the algebraic typeclasses for e.g. Gaussian
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   434
integers. INCOMPATIBILITY.
317e9ebbc3e1 updated for release;
wenzelm
parents: 71536
diff changeset
   435
70524
7783bece74b4 tuned whitespace;
wenzelm
parents: 70522
diff changeset
   436
* Clear distinction between types for bits (False / True) and Z2 (0 /
71427
wenzelm
parents: 71378
diff changeset
   437
1): theory HOL-Library.Bit has been renamed accordingly.
wenzelm
parents: 71378
diff changeset
   438
INCOMPATIBILITY.
wenzelm
parents: 71378
diff changeset
   439
wenzelm
parents: 71378
diff changeset
   440
* Dynamic facts "algebra_split_simps" and "field_split_simps" correspond
70817
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70784
diff changeset
   441
to algebra_simps and field_simps but contain more aggressive rules
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70784
diff changeset
   442
potentially splitting goals; algebra_split_simps roughly replaces
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70784
diff changeset
   443
sign_simps and field_split_simps can be used instead of divide_simps.
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70784
diff changeset
   444
INCOMPATIBILITY.
70524
7783bece74b4 tuned whitespace;
wenzelm
parents: 70522
diff changeset
   445
71428
wenzelm
parents: 71427
diff changeset
   446
* Theory HOL.Complete_Lattices:
wenzelm
parents: 71427
diff changeset
   447
renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf
wenzelm
parents: 71427
diff changeset
   448
71434
6c52b1d71f8b proper symbols;
wenzelm
parents: 71433
diff changeset
   449
* Theory HOL-Library.Monad_Syntax: infix operation "bind" (\<bind>)
70524
7783bece74b4 tuned whitespace;
wenzelm
parents: 70522
diff changeset
   450
associates to the left now as is customary.
7783bece74b4 tuned whitespace;
wenzelm
parents: 70522
diff changeset
   451
71259
09aee7f5b447 Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents: 71166
diff changeset
   452
* Theory HOL-Library.Ramsey: full finite Ramsey's theorem with
09aee7f5b447 Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents: 71166
diff changeset
   453
multiple colours and arbitrary exponents.
09aee7f5b447 Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents: 71166
diff changeset
   454
71484
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   455
* Session HOL-Proofs: build faster thanks to better treatment of proof
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   456
terms in Isabelle/Pure.
71147
wenzelm
parents: 71134
diff changeset
   457
71438
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   458
* Session HOL-Word: bitwise NOT-operator has proper prefix syntax. Minor
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   459
INCOMPATIBILITY.
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   460
71484
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   461
* Session HOL-Analysis: proof method "metric" implements a decision
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   462
procedure for simple linear statements in metric spaces.
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   463
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   464
* Session HOL-Complex_Analysis has been split off from HOL-Analysis.
71149
a7d1fb0c9e16 proper prefix syntax
haftmann
parents: 71147
diff changeset
   465
71150
9e7d40d67258 tuned whitespace
haftmann
parents: 71149
diff changeset
   466
70525
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   467
*** ML ***
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   468
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   469
* Theory construction may be forked internally, the operation
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   470
Theory.join_theory recovers a single result theory. See also the example
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   471
in theory "HOL-ex.Join_Theory".
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   472
70565
d0b75c59beca added ML antiquotation @{oracle_name};
wenzelm
parents: 70562
diff changeset
   473
* Antiquotation @{oracle_name} inlines a formally checked oracle name.
d0b75c59beca added ML antiquotation @{oracle_name};
wenzelm
parents: 70562
diff changeset
   474
71436
2e1b0ee920f5 updated for release;
wenzelm
parents: 71434
diff changeset
   475
* Minimal support for a soft-type system within the Isabelle logical
2e1b0ee920f5 updated for release;
wenzelm
parents: 71434
diff changeset
   476
framework (module Soft_Type_System).
2e1b0ee920f5 updated for release;
wenzelm
parents: 71434
diff changeset
   477
71750
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71662
diff changeset
   478
* Former Variable.auto_fixes has been replaced by slightly more general
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71662
diff changeset
   479
Proof_Context.augment: it is subject to an optional soft-type system of
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71662
diff changeset
   480
the underlying object-logic. Minor INCOMPATIBILITY.
71436
2e1b0ee920f5 updated for release;
wenzelm
parents: 71434
diff changeset
   481
71438
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   482
* More scalable Export.export using XML.tree to avoid premature string
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   483
allocations, with convenient shortcut XML.blob. Minor INCOMPATIBILITY.
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   484
71493
wenzelm
parents: 71485
diff changeset
   485
* Prover IDE support for the underlying Poly/ML compiler (not the basis
wenzelm
parents: 71485
diff changeset
   486
library). Open $ML_SOURCES/ROOT.ML in Isabelle/jEdit to browse the
wenzelm
parents: 71485
diff changeset
   487
implementation with full markup.
wenzelm
parents: 71485
diff changeset
   488
70525
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70524
diff changeset
   489
70599
wenzelm
parents: 70565
diff changeset
   490
*** System ***
wenzelm
parents: 70565
diff changeset
   491
71433
wenzelm
parents: 71432
diff changeset
   492
* Standard rendering for more Isabelle symbols: \<llangle> \<rrangle> \<bbar> \<sqdot>
wenzelm
parents: 71432
diff changeset
   493
71378
820cf124dced added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents: 71343
diff changeset
   494
* The command-line tool "isabelle scala_project" creates a Gradle
820cf124dced added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents: 71343
diff changeset
   495
project configuration for Isabelle/Scala/jEdit, to support Scala IDEs
820cf124dced added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents: 71343
diff changeset
   496
such as IntelliJ IDEA.
820cf124dced added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents: 71343
diff changeset
   497
71293
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
   498
* The command-line tool "isabelle phabricator_setup" facilitates
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
   499
self-hosting of the Phabricator software-development platform, with
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
   500
support for Git, Mercurial, Subversion repositories. This helps to avoid
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
   501
monoculture and to escape the gravity of centralized version control by
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
   502
Github and/or Bitbucket. For further documentation, see chapter
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
   503
"Phabricator server administration" in the "system" manual. A notable
8f3940150493 tuned NEWS;
wenzelm
parents: 71291
diff changeset
   504
example installation is https://isabelle-dev.sketis.net/.
71134
wenzelm
parents: 70957
diff changeset
   505
71325
wenzelm
parents: 71293
diff changeset
   506
* The command-line tool "isabelle hg_setup" simplifies the setup of
wenzelm
parents: 71293
diff changeset
   507
Mercurial repositories, with hosting via Phabricator or SSH file server
wenzelm
parents: 71293
diff changeset
   508
access.
wenzelm
parents: 71293
diff changeset
   509
70686
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70683
diff changeset
   510
* The command-line tool "isabelle imports" has been discontinued: strict
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70683
diff changeset
   511
checking of session directories enforces session-qualified theory names
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70683
diff changeset
   512
in applications -- users are responsible to specify session ROOT entries
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70683
diff changeset
   513
properly.
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70683
diff changeset
   514
71429
wenzelm
parents: 71428
diff changeset
   515
* The command-line tool "isabelle dump" and its underlying
wenzelm
parents: 71428
diff changeset
   516
Isabelle/Scala module isabelle.Dump has become more scalable, by
wenzelm
parents: 71428
diff changeset
   517
splitting sessions and supporting a base logic image. Minor
wenzelm
parents: 71428
diff changeset
   518
INCOMPATIBILITY in options and parameters.
wenzelm
parents: 71428
diff changeset
   519
71750
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71662
diff changeset
   520
* The command-line tool "isabelle build_docker" has been slightly
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71662
diff changeset
   521
improved: it is now properly documented in the "system" manual.
f39b1afe8845 tuned NEWS;
wenzelm
parents: 71662
diff changeset
   522
71438
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   523
* Isabelle/Scala support for the Linux platform (Ubuntu): packages,
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   524
users, system services.
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   525
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   526
* Isabelle/Scala support for proof terms (with full type/term
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   527
information) in module isabelle.Term.
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   528
71662
263298eb68b2 more NEWS;
wenzelm
parents: 71581
diff changeset
   529
* Isabelle/Scala: more scalable output of YXML files, e.g. relevant for
263298eb68b2 more NEWS;
wenzelm
parents: 71581
diff changeset
   530
"isabelle dump".
263298eb68b2 more NEWS;
wenzelm
parents: 71581
diff changeset
   531
70599
wenzelm
parents: 70565
diff changeset
   532
* Theory export via Isabelle/Scala has been reworked. The former "fact"
wenzelm
parents: 70565
diff changeset
   533
name space is now split into individual "thm" items: names are
wenzelm
parents: 70565
diff changeset
   534
potentially indexed, such as "foo" for singleton facts, or "bar(1)",
wenzelm
parents: 70565
diff changeset
   535
"bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now
wenzelm
parents: 70565
diff changeset
   536
exported as well: this spans an overall dependency graph of internal
wenzelm
parents: 70565
diff changeset
   537
inferences; it might help to reconstruct the formal structure of theory
71751
abf3e80bd815 tuned NEWS;
wenzelm
parents: 71750
diff changeset
   538
libraries. See also the module isabelle.Export_Theory in Isabelle/Scala.
70599
wenzelm
parents: 70565
diff changeset
   539
71484
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   540
* Theory export of structured specifications, based on internal
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   541
declarations of Spec_Rules by packages like 'definition', 'inductive',
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   542
'primrec', 'function'.
bb82dd4d19f6 updated for release;
wenzelm
parents: 71473
diff changeset
   543
71428
wenzelm
parents: 71427
diff changeset
   544
* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
wenzelm
parents: 71427
diff changeset
   545
have been discontinued -- deprecated since Isabelle2018.
wenzelm
parents: 71427
diff changeset
   546
71438
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   547
* More complete x86_64 platform support on macOS, notably Catalina where
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   548
old x86 has been discontinued.
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   549
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   550
* Update to GHC stack 2.1.3 with stackage lts-13.19/ghc-8.6.4.
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   551
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   552
* Update to OCaml Opam 2.0.6 (using ocaml 4.05.0 as before).
22158ebde77f updated for release;
wenzelm
parents: 71436
diff changeset
   553
70265
a8238fd25541 back to post-release mode;
wenzelm
parents: 70260
diff changeset
   554
70784
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70686
diff changeset
   555
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   556
New in Isabelle2019 (June 2019)
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   557
-------------------------------
68683
d69127c6e80f back to post-release mode -- after fork point;
wenzelm
parents: 68681
diff changeset
   558
69042
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   559
*** General ***
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   560
70032
0674c24afc5e updated for release;
wenzelm
parents: 70031
diff changeset
   561
* The font collection "Isabelle DejaVu" is systematically derived from
0674c24afc5e updated for release;
wenzelm
parents: 70031
diff changeset
   562
the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif"
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
   563
and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
   564
The DejaVu base fonts are retricted to well-defined Unicode ranges and
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
   565
augmented by special Isabelle symbols, taken from the former
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
   566
"IsabelleText" font (which is no longer provided separately). The line
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
   567
metrics and overall rendering quality is closer to original DejaVu.
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
   568
INCOMPATIBILITY with display configuration expecting the old
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
   569
"IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead.
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
   570
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
   571
* The Isabelle fonts render "\<inverse>" properly as superscript "-1".
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69316
diff changeset
   572
69042
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   573
* Old-style inner comments (* ... *) within the term language are no
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   574
longer supported (legacy feature in Isabelle2018).
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   575
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   576
* Old-style {* verbatim *} tokens are explicitly marked as legacy
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   577
feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   578
via "isabelle update_cartouches -t" (available since Isabelle2015).
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   579
70297
wenzelm
parents: 70281
diff changeset
   580
* Infix operators that begin or end with a "*" are now parenthesized
wenzelm
parents: 70281
diff changeset
   581
without additional spaces, e.g. "(*)" instead of "( * )". Minor
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   582
INCOMPATIBILITY.
69066
nipkow
parents: 69045
diff changeset
   583
69580
6f755e3cd95d mixfix annotations may use cartouches;
wenzelm
parents: 69569
diff changeset
   584
* Mixfix annotations may use cartouches instead of old-style double
69586
9171d1ce5a35 support for "isabelle update -u mixfix_cartouches";
wenzelm
parents: 69585
diff changeset
   585
quotes, e.g. (infixl \<open>+\<close> 60). The command-line tool "isabelle update -u
9171d1ce5a35 support for "isabelle update -u mixfix_cartouches";
wenzelm
parents: 69585
diff changeset
   586
mixfix_cartouches" allows to update existing theory sources
9171d1ce5a35 support for "isabelle update -u mixfix_cartouches";
wenzelm
parents: 69585
diff changeset
   587
automatically.
69580
6f755e3cd95d mixfix annotations may use cartouches;
wenzelm
parents: 69569
diff changeset
   588
69216
1a52baa70aed clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents: 69213
diff changeset
   589
* ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation')
1a52baa70aed clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents: 69213
diff changeset
   590
need to provide a closed expression -- without trailing semicolon. Minor
1a52baa70aed clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents: 69213
diff changeset
   591
INCOMPATIBILITY.
1a52baa70aed clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents: 69213
diff changeset
   592
70057
0403b5127da1 documentation for generated files;
wenzelm
parents: 70032
diff changeset
   593
* Commands 'generate_file', 'export_generated_files', and
0403b5127da1 documentation for generated files;
wenzelm
parents: 70032
diff changeset
   594
'compile_generated_files' support a stateless (PIDE-conformant) model
0403b5127da1 documentation for generated files;
wenzelm
parents: 70032
diff changeset
   595
for generated sources and compiled binaries of other languages. The
70060
wenzelm
parents: 70057
diff changeset
   596
compilation process is managed in Isabelle/ML, and results exported to
70057
0403b5127da1 documentation for generated files;
wenzelm
parents: 70032
diff changeset
   597
the session database for further use (e.g. with "isabelle export" or
0403b5127da1 documentation for generated files;
wenzelm
parents: 70032
diff changeset
   598
"isabelle build -e").
0403b5127da1 documentation for generated files;
wenzelm
parents: 70032
diff changeset
   599
69042
6e9df530b441 discontinued old-style inner comments;
wenzelm
parents: 69037
diff changeset
   600
69189
wenzelm
parents: 69183
diff changeset
   601
*** Isabelle/jEdit Prover IDE ***
wenzelm
parents: 69183
diff changeset
   602
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   603
* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   604
DejaVu" collection by default, which provides uniform rendering quality
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   605
with the usual Isabelle symbols. Line spacing no longer needs to be
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   606
adjusted: properties for the old IsabelleText font had "Global Options /
70069
381035c03220 proper default;
wenzelm
parents: 70068
diff changeset
   607
Text Area / Extra vertical line spacing (in pixels): -2", it now
381035c03220 proper default;
wenzelm
parents: 70068
diff changeset
   608
defaults to 1, but 0 works as well.
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   609
69780
wenzelm
parents: 69778
diff changeset
   610
* The jEdit File Browser is more prominent in the default GUI layout of
wenzelm
parents: 69778
diff changeset
   611
Isabelle/jEdit: various virtual file-systems provide access to Isabelle
wenzelm
parents: 69778
diff changeset
   612
resources, notably via "favorites:" (or "Edit Favorites").
wenzelm
parents: 69778
diff changeset
   613
70061
5b75480f371a more NEWS;
wenzelm
parents: 70060
diff changeset
   614
* Further markup and rendering for "plain text" (e.g. informal prose)
5b75480f371a more NEWS;
wenzelm
parents: 70060
diff changeset
   615
and "raw text" (e.g. verbatim sources). This improves the visual
5b75480f371a more NEWS;
wenzelm
parents: 70060
diff changeset
   616
appearance of formal comments inside the term language, or in general
5b75480f371a more NEWS;
wenzelm
parents: 70060
diff changeset
   617
for repeated alternation of formal and informal text.
5b75480f371a more NEWS;
wenzelm
parents: 70060
diff changeset
   618
69643
83f15deb2d36 added action "isabelle-export-browser";
wenzelm
parents: 69624
diff changeset
   619
* Action "isabelle-export-browser" points the File Browser to the theory
69764
wenzelm
parents: 69755
diff changeset
   620
exports of the current buffer, based on the "isabelle-export:" virtual
wenzelm
parents: 69755
diff changeset
   621
file-system. The directory view needs to be reloaded manually to follow
wenzelm
parents: 69755
diff changeset
   622
ongoing document processing.
wenzelm
parents: 69755
diff changeset
   623
wenzelm
parents: 69755
diff changeset
   624
* Action "isabelle-session-browser" points the File Browser to session
wenzelm
parents: 69755
diff changeset
   625
information, based on the "isabelle-session:" virtual file-system. Its
wenzelm
parents: 69755
diff changeset
   626
entries are structured according to chapter / session names, the open
wenzelm
parents: 69755
diff changeset
   627
operation is redirected to the session ROOT file.
69643
83f15deb2d36 added action "isabelle-export-browser";
wenzelm
parents: 69624
diff changeset
   628
69273
wenzelm
parents: 69269
diff changeset
   629
* Support for user-defined file-formats via class isabelle.File_Format
69277
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69273
diff changeset
   630
in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69273
diff changeset
   631
the shell function "isabelle_file_format" in etc/settings (e.g. of an
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69273
diff changeset
   632
Isabelle component).
69273
wenzelm
parents: 69269
diff changeset
   633
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   634
* System option "jedit_text_overview" allows to disable the text
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   635
overview column.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   636
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69829
diff changeset
   637
* Command-line options "-s" and "-u" of "isabelle jedit" override the
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69829
diff changeset
   638
default for system option "system_heaps" that determines the heap
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69829
diff changeset
   639
storage directory for "isabelle build". Option "-n" is now clearly
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69829
diff changeset
   640
separated from option "-s".
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69829
diff changeset
   641
70105
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
   642
* The Isabelle/jEdit desktop application uses the same options as
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
   643
"isabelle jedit" for its internal "isabelle build" process: the implicit
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
   644
option "-o system_heaps" (or "-s") has been discontinued. This reduces
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
   645
the potential for surprise wrt. command-line tools.
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
   646
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
   647
* The official download of the Isabelle/jEdit application already
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
   648
contains heap images for Isabelle/HOL within its main directory: thus
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
   649
the first encounter becomes faster and more robust (e.g. when run from a
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
   650
read-only directory).
eadd87383e30 clarified build of standard heaps;
wenzelm
parents: 70082
diff changeset
   651
70072
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
   652
* Isabelle DejaVu fonts are available with hinting by default, which is
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
   653
relevant for low-resolution displays. This may be disabled via system
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
   654
option "isabelle_fonts_hinted = false" in
70075
ee0b8e06b01c proper etc/preferences;
wenzelm
parents: 70072
diff changeset
   655
$ISABELLE_HOME_USER/etc/preferences -- it occasionally yields better
70072
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
   656
results.
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
   657
70031
wenzelm
parents: 70026
diff changeset
   658
* OpenJDK 11 has quite different font rendering, with better glyph
wenzelm
parents: 70026
diff changeset
   659
shapes and improved sub-pixel anti-aliasing. In some situations results
70072
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
   660
might be *worse* than Oracle Java 8, though -- a proper HiDPI / UHD
54dc58086351 support both hinted and unhinted fonts;
wenzelm
parents: 70069
diff changeset
   661
display is recommended.
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   662
70258
b4534d72dd22 more NEWS;
wenzelm
parents: 70237
diff changeset
   663
* OpenJDK 11 supports GTK version 2.2 and 3 (according to system
b4534d72dd22 more NEWS;
wenzelm
parents: 70237
diff changeset
   664
property jdk.gtk.version). The factory default is version 3, but
b4534d72dd22 more NEWS;
wenzelm
parents: 70237
diff changeset
   665
ISABELLE_JAVA_SYSTEM_OPTIONS includes "-Djdk.gtk.version=2.2" to make
b4534d72dd22 more NEWS;
wenzelm
parents: 70237
diff changeset
   666
this more conservative (as in Java 8). Depending on the GTK theme
b4534d72dd22 more NEWS;
wenzelm
parents: 70237
diff changeset
   667
configuration, "-Djdk.gtk.version=3" might work better or worse.
b4534d72dd22 more NEWS;
wenzelm
parents: 70237
diff changeset
   668
69189
wenzelm
parents: 69183
diff changeset
   669
69962
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
   670
*** Document preparation ***
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
   671
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
   672
* Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
   673
are stripped from document output: the effect is to modify the semantic
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
   674
presentation context or to emit markup to the PIDE document. Some
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
   675
predefined markers are taken from the Dublin Core Metadata Initiative,
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
   676
e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that
70281
wenzelm
parents: 70260
diff changeset
   677
can be retrieved from the document database.
69962
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
   678
70140
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
   679
* Old-style command tags %name are re-interpreted as markers with
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
   680
proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
   681
before. Potential INCOMPATIBILITY: multiple markers are composed in
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
   682
canonical order, resulting in a reversed list of tags in the
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
   683
presentation context.
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
   684
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
   685
* Marker \<^marker>\<open>tag name\<close> does not apply to the proof of a top-level goal
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
   686
statement by default (e.g. 'theorem', 'lemma'). This is a subtle change
d13865c21e36 updated documentation;
wenzelm
parents: 70127
diff changeset
   687
of semantics wrt. old-style %name.
69962
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
   688
70143
0cc7fe616924 more abbrevs;
wenzelm
parents: 70140
diff changeset
   689
* In Isabelle/jEdit, the string "\tag" may be completed to a "\<^marker>\<open>tag \<close>"
0cc7fe616924 more abbrevs;
wenzelm
parents: 70140
diff changeset
   690
template.
0cc7fe616924 more abbrevs;
wenzelm
parents: 70140
diff changeset
   691
70121
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70106
diff changeset
   692
* Document antiquotation option "cartouche" indicates if the output
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70106
diff changeset
   693
should be delimited as cartouche; this takes precedence over the
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70106
diff changeset
   694
analogous option "quotes".
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 70106
diff changeset
   695
70122
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70121
diff changeset
   696
* Many document antiquotations are internally categorized as "embedded"
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70121
diff changeset
   697
and expect one cartouche argument, which is typically used with the
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70121
diff changeset
   698
\<^control>\<open>cartouche\<close> notation (e.g. \<^term>\<open>\<lambda>x y. x\<close>). The cartouche
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70121
diff changeset
   699
delimiters are stripped in output of the source (antiquotation option
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70121
diff changeset
   700
"source"), but it is possible to enforce delimiters via option
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70121
diff changeset
   701
"source_cartouche", e.g. @{term [source_cartouche] \<open>\<lambda>x y. x\<close>}.
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70121
diff changeset
   702
69962
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69960
diff changeset
   703
68879
wenzelm
parents: 68848
diff changeset
   704
*** Isar ***
wenzelm
parents: 68848
diff changeset
   705
69045
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
   706
* Implicit cases goal1, goal2, goal3, etc. have been discontinued
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
   707
(legacy feature since Isabelle2016).
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
   708
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   709
* More robust treatment of structural errors: begin/end blocks take
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   710
precedence over goal/proof. This is particularly relevant for the
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   711
headless PIDE session and server.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   712
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   713
* Command keywords of kind thy_decl / thy_goal may be more specifically
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   714
fit into the traditional document model of "definition-statement-proof"
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   715
via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   716
69045
8c240fdeffcb discontinued old-style goal cases;
wenzelm
parents: 69044
diff changeset
   717
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   718
*** HOL ***
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   719
70009
435fb018e8ee "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents: 69962
diff changeset
   720
* Command 'export_code' produces output as logical files within the
70011
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
   721
theory context, as well as formal session exports that can be
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
   722
materialized via command-line tools "isabelle export" or "isabelle build
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
   723
-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
   724
provides a virtual file-system "isabelle-export:" that can be explored
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
   725
in the regular file-browser. A 'file_prefix' argument allows to specify
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
   726
an explicit name prefix for the target file (SML, OCaml, Scala) or
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
   727
directory (Haskell); the default is "export" with a consecutive number
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
   728
within each theory.
70009
435fb018e8ee "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents: 69962
diff changeset
   729
435fb018e8ee "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents: 69962
diff changeset
   730
* Command 'export_code': the 'file' argument is now legacy and will be
435fb018e8ee "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents: 69962
diff changeset
   731
removed soon: writing to the physical file-system is not well-defined in
70011
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
   732
a reactive/parallel application like Isabelle. The empty 'file' argument
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
   733
has been discontinued already: it is superseded by the file-browser in
9dde788b0128 clarified 'file_prefix';
wenzelm
parents: 70009
diff changeset
   734
Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.
69624
e02bdf853a4c optional code export as theory export
haftmann
parents: 69609
diff changeset
   735
70022
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70011
diff changeset
   736
* Command 'code_reflect' no longer supports the 'file' argument: it has
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70011
diff changeset
   737
been superseded by 'file_prefix' for stateless file management as in
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70011
diff changeset
   738
'export_code'. Minor INCOMPATIBILITY.
49e178cbf923 'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents: 70011
diff changeset
   739
69743
6a9a8ef5e4c6 prefer proper strings in OCaml
haftmann
parents: 69733
diff changeset
   740
* Code generation for OCaml: proper strings are used for literals.
6a9a8ef5e4c6 prefer proper strings in OCaml
haftmann
parents: 69733
diff changeset
   741
Minor INCOMPATIBILITY.
6a9a8ef5e4c6 prefer proper strings in OCaml
haftmann
parents: 69733
diff changeset
   742
69926
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
   743
* Code generation for OCaml: Zarith supersedes Nums as library for
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
   744
proper integer arithmetic. The library is located via standard
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
   745
invocations of "ocamlfind" (via ISABELLE_OCAMLFIND settings variable).
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
   746
The environment provided by "isabelle ocaml_setup" already contains this
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
   747
tool and the required packages. Minor INCOMPATIBILITY.
69906
55534affe445 migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents: 69903
diff changeset
   748
69690
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69672
diff changeset
   749
* Code generation for Haskell: code includes for Haskell must contain
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69672
diff changeset
   750
proper module frame, nothing is added magically any longer.
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69672
diff changeset
   751
INCOMPATIBILITY.
1fb204399d8d self-contained code modules for Haskell
haftmann
parents: 69672
diff changeset
   752
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   753
* Code generation: slightly more conventional syntax for 'code_stmts'
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   754
antiquotation. Minor INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   755
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   756
* Theory List: the precedence of the list_update operator has changed:
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   757
"f a [n := x]" now needs to be written "(f a)[n := x]".
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   758
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   759
* The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter> (not the corresponding binding operators)
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   760
now have the same precedence as any other prefix function symbol. Minor
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   761
INCOMPATIBILITY.
69861
62e47f06d22c avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents: 69854
diff changeset
   762
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   763
* 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
   764
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
   765
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
   766
SUPREMUM, UNION, INTER should now rarely occur in output and are just
70237
7e9269c188d6 more NEWS
haftmann
parents: 70215
diff changeset
   767
retained as migration auxiliary. Abbreviations MINIMUM and MAXIMUM
7e9269c188d6 more NEWS
haftmann
parents: 70215
diff changeset
   768
are gone INCOMPATIBILITY.
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   769
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   770
* The simplifier uses image_cong_simp as a congruence rule. The historic
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   771
and not really well-formed congruence rules INF_cong*, SUP_cong*, are
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   772
not used by default any longer. INCOMPATIBILITY; consider using declare
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   773
image_cong_simp [cong del] in extreme situations.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   774
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   775
* INF_image and SUP_image are no default simp rules any longer.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   776
INCOMPATIBILITY, prefer image_comp as simp rule if needed.
68938
a0b19a163f5e left-over rename from 3f9bb52082c4
haftmann
parents: 68883
diff changeset
   777
69164
74f1b0f10b2b uniform naming of strong congruence rules
nipkow
parents: 69155
diff changeset
   778
* Strong congruence rules (with =simp=> in the premises) for constant f
69546
27dae626822b prefer naming convention from datatype package for strong congruence rules
haftmann
parents: 69506
diff changeset
   779
are now uniformly called f_cong_simp, in accordance with congruence
27dae626822b prefer naming convention from datatype package for strong congruence rules
haftmann
parents: 69506
diff changeset
   780
rules produced for mappers by the datatype package. INCOMPATIBILITY.
69164
74f1b0f10b2b uniform naming of strong congruence rules
nipkow
parents: 69155
diff changeset
   781
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   782
* Retired lemma card_Union_image; use the simpler card_UN_disjoint
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   783
instead. INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   784
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   785
* Facts sum_mset.commute and prod_mset.commute have been renamed to
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   786
sum_mset.swap and prod_mset.swap, similarly to sum.swap and prod.swap.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   787
INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   788
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   789
* ML structure Inductive: slightly more conventional naming schema.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   790
Minor INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   791
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   792
* ML: Various _global variants of specification tools have been removed.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   793
Minor INCOMPATIBILITY, prefer combinators
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   794
Named_Target.theory_map[_result] to lift specifications to the global
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   795
theory level.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   796
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   797
* Theory HOL-Library.Simps_Case_Conv: 'case_of_simps' now supports
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   798
overlapping and non-exhaustive patterns and handles arbitrarily nested
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   799
patterns. It uses on the same algorithm as HOL-Library.Code_Lazy, which
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   800
assumes sequential left-to-right pattern matching. The generated
69568
de09a7261120 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents: 69506
diff changeset
   801
equation no longer tuples the arguments on the right-hand side.
de09a7261120 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents: 69506
diff changeset
   802
INCOMPATIBILITY.
de09a7261120 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents: 69506
diff changeset
   803
70297
wenzelm
parents: 70281
diff changeset
   804
* Theory HOL-Library.Multiset: the \<Union># operator now has the same
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   805
precedence as any other prefix function symbol.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   806
70080
traytel
parents: 70075
diff changeset
   807
* Theory HOL-Library.Cardinal_Notations has been discontinued in favor
70168
e79bbf86a984 tuned for release;
wenzelm
parents: 70164
diff changeset
   808
of the bundle cardinal_syntax (available in theory Main). Minor
e79bbf86a984 tuned for release;
wenzelm
parents: 70164
diff changeset
   809
INCOMPATIBILITY.
70080
traytel
parents: 70075
diff changeset
   810
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   811
* Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring,
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   812
used for computing powers in class "monoid_mult" and modular
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   813
exponentiation.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   814
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   815
* Session HOL-Computational_Algebra: Formal Laurent series and overhaul
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   816
of Formal power series.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   817
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   818
* Session HOL-Number_Theory: More material on residue rings in
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   819
Carmichael's function, primitive roots, more properties for "ord".
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   820
70125
b601c2c87076 type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents: 70106
diff changeset
   821
* Session HOL-Analysis: Better organization and much more material
b601c2c87076 type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents: 70106
diff changeset
   822
at the level of abstract topological spaces.
b601c2c87076 type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents: 70106
diff changeset
   823
70164
1f163f772da3 Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)
paulson <lp15@cam.ac.uk>
parents: 70143
diff changeset
   824
* Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
70215
8371a25ca177 Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents: 70175
diff changeset
   825
 algebraic closure of a field by de Vilhena and Baillon.
70032
0674c24afc5e updated for release;
wenzelm
parents: 70031
diff changeset
   826
70168
e79bbf86a984 tuned for release;
wenzelm
parents: 70164
diff changeset
   827
* Session HOL-Homology has been added. It is a port of HOL Light's
e79bbf86a984 tuned for release;
wenzelm
parents: 70164
diff changeset
   828
homology library, with new proofs of "invariance of domain" and related
e79bbf86a984 tuned for release;
wenzelm
parents: 70164
diff changeset
   829
results.
e79bbf86a984 tuned for release;
wenzelm
parents: 70164
diff changeset
   830
69099
d44cb8a3e5e0 HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents: 69094
diff changeset
   831
* Session HOL-SPARK: .prv files are no longer written to the
d44cb8a3e5e0 HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents: 69094
diff changeset
   832
file-system, but exported to the session database. Results may be
70026
6ae9505d693a more convenient export;
wenzelm
parents: 70023
diff changeset
   833
retrieved via "isabelle build -e HOL-SPARK-Examples" on the
6ae9505d693a more convenient export;
wenzelm
parents: 70023
diff changeset
   834
command-line.
69099
d44cb8a3e5e0 HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents: 69094
diff changeset
   835
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   836
* Sledgehammer:
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   837
  - The URL for SystemOnTPTP, which is used by remote provers, has been
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   838
    updated.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   839
  - The machine-learning-based filter MaSh has been optimized to take
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   840
    less time (in most cases).
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   841
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   842
* SMT: reconstruction is now possible using the SMT solver veriT.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   843
70174
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70168
diff changeset
   844
* Session HOL-Word:
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70168
diff changeset
   845
  * New theory More_Word as comprehensive entrance point.
70175
85fb1a585f52 eliminated type class
haftmann
parents: 70174
diff changeset
   846
  * Merged type class bitss into type class bits.
70174
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70168
diff changeset
   847
  INCOMPATIBILITY.
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents: 70168
diff changeset
   848
68796
9ca183045102 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents: 68770
diff changeset
   849
68803
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
   850
*** ML ***
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
   851
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   852
* Command 'generate_file' allows to produce sources for other languages,
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   853
with antiquotations in the Isabelle context (only the control-cartouche
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   854
form). The default "cartouche" antiquotation evaluates an ML expression
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   855
of type string and inlines the result as a string literal of the target
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   856
language. For example, this works for Haskell as follows:
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   857
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   858
  generate_file "Pure.hs" = \<open>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   859
  module Isabelle.Pure where
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   860
    allConst, impConst, eqConst :: String
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   861
    allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   862
    impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   863
    eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   864
  \<close>
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   865
70082
4f936de6d9b8 tuned -- prefer Isar command 'compile_generated_files';
wenzelm
parents: 70080
diff changeset
   866
See also commands 'export_generated_files' and 'compile_generated_files'
4f936de6d9b8 tuned -- prefer Isar command 'compile_generated_files';
wenzelm
parents: 70080
diff changeset
   867
to use the results.
68803
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
   868
70260
22cfcfcadd8b more documentation;
wenzelm
parents: 70258
diff changeset
   869
* ML evaluation (notably via command 'ML' or 'ML_file') is subject to
68824
7414ce0256e1 some NEWS (instead of proper documentation);
wenzelm
parents: 68803
diff changeset
   870
option ML_environment to select a named environment, such as "Isabelle"
70260
22cfcfcadd8b more documentation;
wenzelm
parents: 70258
diff changeset
   871
for Isabelle/ML, or "SML" for official Standard ML.
68803
169bf32b35dd retain original PolyML.pointerEq;
wenzelm
parents: 68796
diff changeset
   872
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69377
diff changeset
   873
* ML antiquotation @{master_dir} refers to the master directory of the
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69377
diff changeset
   874
underlying theory, i.e. the directory of the theory file.
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69377
diff changeset
   875
69470
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69381
diff changeset
   876
* ML antiquotation @{verbatim} inlines its argument as string literal,
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69381
diff changeset
   877
preserving newlines literally. The short form \<^verbatim>\<open>abc\<close> is particularly
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69381
diff changeset
   878
useful.
c8c3285f1294 more ML antiquotations;
wenzelm
parents: 69381
diff changeset
   879
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   880
* Local_Theory.reset is no longer available in user space. Regular
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   881
definitional packages should use balanced blocks of
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   882
Local_Theory.open_target versus Local_Theory.close_target instead, or
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   883
the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   884
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   885
* Original PolyML.pointerEq is retained as a convenience for tools that
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   886
don't use Isabelle/ML (where this is called "pointer_eq").
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents: 69377
diff changeset
   887
69282
94fa3376ba33 added ML antiquotation @{master_dir};
wenzelm
parents: 69277
diff changeset
   888
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
   889
*** System ***
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
   890
70031
wenzelm
parents: 70026
diff changeset
   891
* Update to OpenJDK 11: the current long-term support version of Java.
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   892
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   893
* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   894
the full overhead of 64-bit values everywhere. This special x86_64_32
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   895
mode provides up to 16GB ML heap, while program code and stacks are
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   896
allocated elsewhere. Thus approx. 5 times more memory is available for
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   897
applications compared to old x86 mode (which is no longer used by
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   898
Isabelle). The switch to the x86_64 CPU architecture also avoids
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   899
compatibility problems with Linux and macOS, where 32-bit applications
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   900
are gradually phased out.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   901
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   902
* System option "checkpoint" has been discontinued: obsolete thanks to
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   903
improved memory management in Poly/ML.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   904
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   905
* System option "system_heaps" determines where to store the session
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69829
diff changeset
   906
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: 69829
diff changeset
   907
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: 69829
diff changeset
   908
INCOMPATIBILITY in command-line syntax.
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69829
diff changeset
   909
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   910
* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   911
source modules for Isabelle tools implemented in Haskell, notably for
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   912
Isabelle/PIDE.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   913
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   914
* The command-line tool "isabelle build -e" retrieves theory exports
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   915
from the session build database, using 'export_files' in session ROOT
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   916
entries.
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   917
69585
wenzelm
parents: 69580
diff changeset
   918
* The command-line tool "isabelle update" uses Isabelle/PIDE in
wenzelm
parents: 69580
diff changeset
   919
batch-mode to update theory sources based on semantic markup produced in
69609
wenzelm
parents: 69592
diff changeset
   920
Isabelle/ML. Actual updates depend on system options that may be enabled
69588
wenzelm
parents: 69586
diff changeset
   921
via "-u OPT" (for "update_OPT"), see also $ISABELLE_HOME/etc/options
wenzelm
parents: 69586
diff changeset
   922
section "Theory update". Theory sessions are specified as in "isabelle
69585
wenzelm
parents: 69580
diff changeset
   923
dump".
wenzelm
parents: 69580
diff changeset
   924
69592
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69588
diff changeset
   925
* The command-line tool "isabelle update -u control_cartouches" changes
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69588
diff changeset
   926
antiquotations into control-symbol format (where possible): @{NAME}
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69588
diff changeset
   927
becomes \<^NAME> and @{NAME ARG} becomes \<^NAME>\<open>ARG\<close>.
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69588
diff changeset
   928
69277
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69273
diff changeset
   929
* Support for Isabelle command-line tools defined in Isabelle/Scala.
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69273
diff changeset
   930
Instances of class Isabelle_Scala_Tools may be configured via the shell
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69273
diff changeset
   931
function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69273
diff changeset
   932
component).
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69273
diff changeset
   933
70023
5aef4e9966c4 misc tuning for release;
wenzelm
parents: 70022
diff changeset
   934
* Isabelle Server command "use_theories" supports "nodes_status_delay"
69044
wenzelm
parents: 69042
diff changeset
   935
for continuous output of node status information. The time interval is
wenzelm
parents: 69042
diff changeset
   936
specified in seconds; a negative value means it is disabled (default).
wenzelm
parents: 69042
diff changeset
   937
wenzelm
parents: 69042
diff changeset
   938
* 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
   939
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
   940
is no longer required.
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
   941
69926
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
   942
* OCaml tools and libraries are now accesed via ISABELLE_OCAMLFIND,
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
   943
which needs to point to a suitable version of "ocamlfind" (e.g. via
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
   944
OPAM, see below). INCOMPATIBILITY: settings variables ISABELLE_OCAML and
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
   945
ISABELLE_OCAMLC are no longer supported.
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
   946
69268
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: 69230
diff changeset
   947
* 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: 69230
diff changeset
   948
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: 69230
diff changeset
   949
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: 69230
diff changeset
   950
  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: 69230
diff changeset
   951
  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: 69230
diff changeset
   952
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: 69230
diff changeset
   953
  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: 69230
diff changeset
   954
  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: 69230
diff changeset
   955
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: 69230
diff changeset
   956
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: 69230
diff changeset
   957
(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: 69230
diff changeset
   958
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: 69230
diff changeset
   959
  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: 69230
diff changeset
   960
  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: 69230
diff changeset
   961
  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: 69230
diff changeset
   962
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: 69230
diff changeset
   963
  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: 69230
diff changeset
   964
  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: 69230
diff changeset
   965
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: 69230
diff changeset
   966
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: 69230
diff changeset
   967
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: 69230
diff changeset
   968
69269
1bee990d443c tuned whitespace;
wenzelm
parents: 69268
diff changeset
   969
  ISABELLE_GHC
1bee990d443c tuned whitespace;
wenzelm
parents: 69268
diff changeset
   970
69926
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
   971
  ISABELLE_OCAMLFIND
69268
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: 69230
diff changeset
   972
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: 69230
diff changeset
   973
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: 69230
diff changeset
   974
be recovered by purging the directories ISABELLE_STACK_ROOT /
69926
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
   975
ISABELLE_OPAM_ROOT, or by resetting these variables in
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69914
diff changeset
   976
$ISABELLE_HOME_USER/etc/settings.
69189
wenzelm
parents: 69183
diff changeset
   977
69822
8c587dd44f51 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents: 69811
diff changeset
   978
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68879
diff changeset
   979
68391
9b4f60bdad54 updated for release;
wenzelm
parents: 68373
diff changeset
   980
New in Isabelle2018 (August 2018)
9b4f60bdad54 updated for release;
wenzelm
parents: 68373
diff changeset
   981
---------------------------------
66651
435cb8d69e27 back to post-release mode -- after fork point;
wenzelm
parents: 66650
diff changeset
   982
66712
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 66688
diff changeset
   983
*** General ***
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 66688
diff changeset
   984
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   985
* Session-qualified theory names are mandatory: it is no longer possible
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   986
to refer to unqualified theories from the parent session.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   987
INCOMPATIBILITY for old developments that have not been updated to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   988
Isabelle2017 yet (using the "isabelle imports" tool).
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   989
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   990
* Only the most fundamental theory names are global, usually the entry
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   991
points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   992
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   993
formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   994
68558
7aae213d9e69 discontinued pending_shyps: too much complication due to lazy facts;
wenzelm
parents: 68548
diff changeset
   995
* 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
   996
Rare INCOMPATIBILITY.
68540
000a0e062529 disallow pending hyps;
wenzelm
parents: 68523
diff changeset
   997
68661
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
   998
* Facts stemming from locale interpretation are subject to lazy
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
   999
evaluation for improved performance. Rare INCOMPATIBILITY: errors
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
  1000
stemming from interpretation morphisms might be deferred and thus
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
  1001
difficult to locate; enable system option "strict_facts" temporarily to
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
  1002
avoid this.
5820f0f379ae added system option "strict_facts";
wenzelm
parents: 68647
diff changeset
  1003
67446
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
  1004
* Marginal comments need to be written exclusively in the new-style form
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
  1005
"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
  1006
supported. INCOMPATIBILITY, use the command-line tool "isabelle
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
  1007
update_comments" to update existing theory files.
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
  1008
67507
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
  1009
* Old-style inner comments (* ... *) within the term language are legacy
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
  1010
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
  1011
instead.
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
  1012
67402
nipkow
parents: 67400
diff changeset
  1013
* The "op <infix-op>" syntax for infix operators has been replaced by
67400
nipkow
parents: 67398
diff changeset
  1014
"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
nipkow
parents: 67398
diff changeset
  1015
be a space between the "*" and the corresponding parenthesis.
68543
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1016
INCOMPATIBILITY, use the command-line tool "isabelle update_op" to
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1017
convert theory and ML files to the new syntax. Because it is based on
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1018
regular expression matching, the result may need a bit of manual
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1019
postprocessing. Invoking "isabelle update_op" converts all files in the
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1020
current directory (recursively). In case you want to exclude conversion
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1021
of ML files (because the tool frequently also converts ML's "op"
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1022
syntax), use option "-m".
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67395
diff changeset
  1023
67013
335a7dce7cb3 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents: 66994
diff changeset
  1024
* 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
  1025
INCOMPATIBILITY.
335a7dce7cb3 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents: 66994
diff changeset
  1026
66757
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
  1027
* Command 'external_file' declares the formal dependency on the given
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
  1028
file name, such that the Isabelle build process knows about it, but
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
  1029
without specific Prover IDE management.
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
  1030
66759
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
  1031
* Session ROOT entries no longer allow specification of 'files'. Rare
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
  1032
INCOMPATIBILITY, use command 'external_file' within a proper theory
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
  1033
context.
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
  1034
66764
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1035
* 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
  1036
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
  1037
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
  1038
-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
  1039
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1040
  isabelle build -D '~~/src/ZF'
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1041
67263
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67262
diff changeset
  1042
* The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67262
diff changeset
  1043
use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67262
diff changeset
  1044
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1045
* In HTML output, the Isabelle symbol "\<hyphen>" is rendered as explicit
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1046
Unicode hyphen U+2010, to avoid unclear meaning of the old "soft hyphen"
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1047
U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1048
output.
67305
ecb74607063f more robust hyphen (see also "Soft hyphen (SHY) – a hard problem?" http://jkorpela.fi/shy.html);
wenzelm
parents: 67304
diff changeset
  1049
66712
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 66688
diff changeset
  1050
67261
wenzelm
parents: 67248
diff changeset
  1051
*** Isabelle/jEdit Prover IDE ***
66768
f27488f47a47 completion supports theory header imports;
wenzelm
parents: 66764
diff changeset
  1052
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1053
* The command-line tool "isabelle jedit" provides more flexible options
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1054
for session management:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1055
68472
581a1bfec8ad clarified documentation;
wenzelm
parents: 68469
diff changeset
  1056
  - option -R builds an auxiliary logic image with all theories from
581a1bfec8ad clarified documentation;
wenzelm
parents: 68469
diff changeset
  1057
    other sessions that are not already present in its parent
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1058
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1059
  - option -S is like -R, with a focus on the selected session and its
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1060
    descendants (this reduces startup time for big projects like AFP)
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1061
68472
581a1bfec8ad clarified documentation;
wenzelm
parents: 68469
diff changeset
  1062
  - option -A specifies an alternative ancestor session for options -R
581a1bfec8ad clarified documentation;
wenzelm
parents: 68469
diff changeset
  1063
    and -S
581a1bfec8ad clarified documentation;
wenzelm
parents: 68469
diff changeset
  1064
68541
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68540
diff changeset
  1065
  - option -i includes additional sessions into the name-space of
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68540
diff changeset
  1066
    theories
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68540
diff changeset
  1067
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1068
  Examples:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1069
    isabelle jedit -R HOL-Number_Theory
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1070
    isabelle jedit -R HOL-Number_Theory -A HOL
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1071
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1072
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
68541
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68540
diff changeset
  1073
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1074
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1075
* PIDE markup for session ROOT files: allows to complete session names,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1076
follow links to theories and document files etc.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1077
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1078
* Completion supports theory header imports, using theory base name.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1079
E.g. "Prob" may be completed to "HOL-Probability.Probability".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1080
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1081
* Named control symbols (without special Unicode rendering) are shown as
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1082
bold-italic keyword. This is particularly useful for the short form of
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1083
antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1084
"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1085
arguments into this format.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1086
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1087
* Completion provides templates for named symbols with arguments,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1088
e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1089
68368
wenzelm
parents: 68364
diff changeset
  1090
* Slightly more parallel checking, notably for high priority print
wenzelm
parents: 68364
diff changeset
  1091
functions (e.g. State output).
wenzelm
parents: 68364
diff changeset
  1092
68080
17f79ae49401 set view title dynamically;
wenzelm
parents: 68073
diff changeset
  1093
* The view title is set dynamically, according to the Isabelle
17f79ae49401 set view title dynamically;
wenzelm
parents: 68073
diff changeset
  1094
distribution and the logic session name. The user can override this via
17f79ae49401 set view title dynamically;
wenzelm
parents: 68073
diff changeset
  1095
set-view-title (stored persistently in $JEDIT_SETTINGS/perspective.xml).
17f79ae49401 set view title dynamically;
wenzelm
parents: 68073
diff changeset
  1096
67395
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67381
diff changeset
  1097
* 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
  1098
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
  1099
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
  1100
67248
68177abb2988 isabelle.preview presents bibtex database files as well;
wenzelm
parents: 67246
diff changeset
  1101
* Action "isabelle.preview" is able to present more file formats,
67266
wenzelm
parents: 67263
diff changeset
  1102
notably bibtex database files and ML files.
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67224
diff changeset
  1103
67262
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67261
diff changeset
  1104
* Action "isabelle.draft" is similar to "isabelle.preview", but shows a
68067
b91c4acc1aaf clarified menu actions;
wenzelm
parents: 68033
diff changeset
  1105
plain-text document draft. Both are available via the menu "Plugins /
b91c4acc1aaf clarified menu actions;
wenzelm
parents: 68033
diff changeset
  1106
Isabelle".
67262
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67261
diff changeset
  1107
67304
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
  1108
* 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
  1109
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
  1110
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
  1111
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
  1112
Unicode content when saving the file.
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
  1113
68545
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68543
diff changeset
  1114
* Bibtex database files (.bib) are semantically checked.
7922992c99ea misc tuning and updates for release;
wenzelm
parents: 68543
diff changeset
  1115
67993
wenzelm
parents: 67928
diff changeset
  1116
* Update to jedit-5.5.0, the latest release.
wenzelm
parents: 67928
diff changeset
  1117
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67224
diff changeset
  1118
67261
wenzelm
parents: 67248
diff changeset
  1119
*** Isabelle/VSCode Prover IDE ***
wenzelm
parents: 67248
diff changeset
  1120
wenzelm
parents: 67248
diff changeset
  1121
* HTML preview of theories and other file-formats similar to
wenzelm
parents: 67248
diff changeset
  1122
Isabelle/jEdit.
wenzelm
parents: 67248
diff changeset
  1123
68690
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
  1124
* Command-line tool "isabelle vscode_server" accepts the same options
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
  1125
-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
  1126
relevant for isabelle.args configuration settings in VSCode. The former
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
  1127
option -A (explore all known session files) has been discontinued: it is
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
  1128
enabled by default, unless option -S is used to focus on a particular
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
  1129
spot in the session structure. INCOMPATIBILITY.
354c04092cd0 more flexible session selection as in "isabelle jedit";
wenzelm
parents: 68681
diff changeset
  1130
66768
f27488f47a47 completion supports theory header imports;
wenzelm
parents: 66764
diff changeset
  1131
67140
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
  1132
*** Document preparation ***
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
  1133
67448
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
  1134
* Formal comments work uniformly in outer syntax, inner syntax (term
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
  1135
language), Isabelle/ML and some other embedded languages of Isabelle.
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
  1136
See also "Document comments" in the isar-ref manual. The following forms
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
  1137
are supported:
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
  1138
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
  1139
  - marginal text comment: \<comment> \<open>\<dots>\<close>
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
  1140
  - canceled source: \<^cancel>\<open>\<dots>\<close>
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
  1141
  - raw LaTeX: \<^latex>\<open>\<dots>\<close>
67413
2555713586c8 added \<^cancel> operator for unused text;
wenzelm
parents: 67402
diff changeset
  1142
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 67368
diff changeset
  1143
* Outside of the inner theory body, the default presentation context is
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 67368
diff changeset
  1144
theory Pure. Thus elementary antiquotations may be used in markup
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 67368
diff changeset
  1145
commands (e.g. 'chapter', 'section', 'text') and formal comments.
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 67368
diff changeset
  1146
68513
88b0e63d58a5 updated documentation;
wenzelm
parents: 68484
diff changeset
  1147
* System option "document_tags" specifies alternative command tags. This
88b0e63d58a5 updated documentation;
wenzelm
parents: 68484
diff changeset
  1148
is occasionally useful to control the global visibility of commands via
88b0e63d58a5 updated documentation;
wenzelm
parents: 68484
diff changeset
  1149
session options (e.g. in ROOT).
67140
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
  1150
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
  1151
* Document markup commands ('section', 'text' etc.) are implicitly
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
  1152
tagged as "document" and visible by default. This avoids the application
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
  1153
of option "document_tags" to these commands.
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
  1154
67145
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
  1155
* Isabelle names are mangled into LaTeX macro names to allow the full
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
  1156
identifier syntax with underscore, prime, digits. This is relevant for
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
  1157
antiquotations in control symbol notation, e.g. \<^const_name> becomes
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
  1158
\isactrlconstUNDERSCOREname.
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
  1159
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1160
* Document preparation with skip_proofs option now preserves the content
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1161
more accurately: only terminal proof steps ('by' etc.) are skipped.
67297
86a099f896fc formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents: 67295
diff changeset
  1162
68484
59793df7f853 clarified document antiquotation @{theory};
wenzelm
parents: 68472
diff changeset
  1163
* Document antiquotation @{theory name} requires the long
59793df7f853 clarified document antiquotation @{theory};
wenzelm
parents: 68472
diff changeset
  1164
session-qualified theory name: this is what users reading the text
59793df7f853 clarified document antiquotation @{theory};
wenzelm
parents: 68472
diff changeset
  1165
normally need to import.
59793df7f853 clarified document antiquotation @{theory};
wenzelm
parents: 68472
diff changeset
  1166
67219
81e9804b2014 added document antiquotation @{session name};
wenzelm
parents: 67215
diff changeset
  1167
* Document antiquotation @{session name} checks and prints the given
81e9804b2014 added document antiquotation @{session name};
wenzelm
parents: 67215
diff changeset
  1168
session name verbatim.
81e9804b2014 added document antiquotation @{session name};
wenzelm
parents: 67215
diff changeset
  1169
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1170
* Document antiquotation @{cite} now checks the given Bibtex entries
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1171
against the Bibtex database files -- only in batch-mode session builds.
67157
d0657c8b7616 clarified document preparation vs. skip_proofs;
wenzelm
parents: 67145
diff changeset
  1172
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 67173
diff changeset
  1173
* Command-line tool "isabelle document" has been re-implemented in
67194
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67191
diff changeset
  1174
Isabelle/Scala, with simplified arguments and explicit errors from the
67203
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67199
diff changeset
  1175
latex and bibtex process. Minor INCOMPATIBILITY.
67173
e746db6db903 more explicit latex errors;
wenzelm
parents: 67157
diff changeset
  1176
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1177
* Session ROOT entry: empty 'document_files' means there is no document
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1178
for this session. There is no need to specify options [document = false]
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1179
anymore.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1180
67140
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
  1181
67702
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67616
diff changeset
  1182
*** Isar ***
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67616
diff changeset
  1183
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67616
diff changeset
  1184
* Command 'interpret' no longer exposes resulting theorems as literal
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67616
diff changeset
  1185
facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67616
diff changeset
  1186
improves modularity of proofs and scalability of locale interpretation.
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67616
diff changeset
  1187
Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67616
diff changeset
  1188
(e.g. use 'find_theorems' or 'try' to figure this out).
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67616
diff changeset
  1189
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1190
* The old 'def' command has been discontinued (legacy since
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1191
Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1192
object-logic equality or equivalence.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1193
68543
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1194
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1195
*** Pure ***
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1196
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1197
* The inner syntax category "sort" now includes notation "_" for the
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1198
dummy sort: it is effectively ignored in type-inference.
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1199
67740
b6ce18784872 Proper rewrite morphisms in locale instances.
ballarin
parents: 67718
diff changeset
  1200
* Rewrites clauses (keyword 'rewrites') were moved into the locale
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1201
expression syntax, where they are part of locale instances. In
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1202
interpretation commands rewrites clauses now need to occur before 'for'
68469
aad109fde9ec In interpretation commands, clarify what to do with definitions immediately subject to rewriting.
ballarin
parents: 68466
diff changeset
  1203
and 'defines'. Rare INCOMPATIBILITY; definitions immediately subject to
aad109fde9ec In interpretation commands, clarify what to do with definitions immediately subject to rewriting.
ballarin
parents: 68466
diff changeset
  1204
rewriting may need to be pulled up into the surrounding theory.
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1205
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1206
* For 'rewrites' clauses, if activating a locale instance fails, fall
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1207
back to reading the clause first. This helps avoid qualification of
67764
0f8cb5568b63 Drop rewrites after defines in interpretations.
ballarin
parents: 67741
diff changeset
  1208
locale instances where the qualifier's sole purpose is avoiding
0f8cb5568b63 Drop rewrites after defines in interpretations.
ballarin
parents: 67741
diff changeset
  1209
duplicate constant declarations.
67741
d5a7f2c54655 Fall back to reading rewrite morphism first if activation fails without it.
ballarin
parents: 67740
diff changeset
  1210
68543
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1211
* Proof method "simp" now supports a new modifier "flip:" followed by a
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1212
list of theorems. Each of these theorems is removed from the simpset
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1213
(without warning if it is not there) and the symmetric version of the
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1214
theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto"
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1215
and friends the modifier is "simp flip:".
67718
17874d43d3b3 notation for dummy sort;
wenzelm
parents: 67702
diff changeset
  1216
17874d43d3b3 notation for dummy sort;
wenzelm
parents: 67702
diff changeset
  1217
66661
fdab65297bd6 real oracle
blanchet
parents: 66651
diff changeset
  1218
*** HOL ***
fdab65297bd6 real oracle
blanchet
parents: 66651
diff changeset
  1219
68568
cf01d04e94d7 more NEWS;
wenzelm
parents: 68558
diff changeset
  1220
* Sledgehammer: bundled version of "vampire" (for non-commercial users)
cf01d04e94d7 more NEWS;
wenzelm
parents: 68558
diff changeset
  1221
helps to avoid fragility of "remote_vampire" service.
cf01d04e94d7 more NEWS;
wenzelm
parents: 68558
diff changeset
  1222
68028
1f9f973eed2a proper datatype for 8-bit characters
haftmann
parents: 68027
diff changeset
  1223
* Clarified relationship of characters, strings and code generation:
1f9f973eed2a proper datatype for 8-bit characters
haftmann
parents: 68027
diff changeset
  1224
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1225
  - Type "char" is now a proper datatype of 8-bit values.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1226
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1227
  - Conversions "nat_of_char" and "char_of_nat" are gone; use more
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1228
    general conversions "of_char" and "char_of" with suitable type
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1229
    constraints instead.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1230
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1231
  - The zero character is just written "CHR 0x00", not "0" any longer.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1232
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1233
  - Type "String.literal" (for code generation) is now isomorphic to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1234
    lists of 7-bit (ASCII) values; concrete values can be written as
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1235
    "STR ''...''" for sequences of printable characters and "STR 0x..."
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1236
    for one single ASCII code point given as hexadecimal numeral.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1237
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1238
  - Type "String.literal" supports concatenation "... + ..." for all
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1239
    standard target languages.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1240
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1241
  - Theory HOL-Library.Code_Char is gone; study the explanations
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1242
    concerning "String.literal" in the tutorial on code generation to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1243
    get an idea how target-language string literals can be converted to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1244
    HOL string values and vice versa.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1245
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1246
  - Session Imperative-HOL: operation "raise" directly takes a value of
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1247
    type "String.literal" as argument, not type "string".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1248
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1249
INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1250
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1251
* Code generation: Code generation takes an explicit option
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1252
"case_insensitive" to accomodate case-insensitive file systems.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1253
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1254
* Abstract bit operations as part of Main: push_bit, take_bit, drop_bit.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1255
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1256
* New, more general, axiomatization of complete_distrib_lattice. The
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1257
former axioms:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1258
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1259
  "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1260
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1261
are replaced by:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1262
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1263
  "Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1264
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1265
The instantiations of sets and functions as complete_distrib_lattice are
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1266
moved to Hilbert_Choice.thy because their proofs need the Hilbert choice
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1267
operator. The dual of this property is also proved in theory
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1268
HOL.Hilbert_Choice.
67831
07f5588f2735 Removed stray 'sledgehammer' invocation
Manuel Eberl <eberlm@in.tum.de>
parents: 67830
diff changeset
  1269
67999
1b05f74f2e5f tidying up including contributions from Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents: 67993
diff changeset
  1270
* New syntax for the minimum/maximum of a function over a finite set:
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1271
MIN x\<in>A. B and even MIN x. B (only useful for finite types), also MAX.
67999
1b05f74f2e5f tidying up including contributions from Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents: 67993
diff changeset
  1272
67525
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
  1273
* Clarifed theorem names:
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
  1274
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
  1275
  Min.antimono ~> Min.subset_imp
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
  1276
  Max.antimono ~> Max.subset_imp
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
  1277
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
  1278
Minor INCOMPATIBILITY.
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
  1279
66661
fdab65297bd6 real oracle
blanchet
parents: 66651
diff changeset
  1280
* SMT module:
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1281
66661
fdab65297bd6 real oracle
blanchet
parents: 66651
diff changeset
  1282
  - The 'smt_oracle' option is now necessary when using the 'smt' method
66662
4b10fa05423b document incompatibility
blanchet
parents: 66661
diff changeset
  1283
    with a solver other than Z3. INCOMPATIBILITY.
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1284
66844
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
  1285
  - The encoding to first-order logic is now more complete in the
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
  1286
    presence of higher-order quantifiers. An 'smt_explicit_application'
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
  1287
    option has been added to control this. INCOMPATIBILITY.
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
  1288
66804
3f9bb52082c4 avoid name clashes on interpretation of abstract locales
haftmann
parents: 66803
diff changeset
  1289
* Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
66844
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
  1290
sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
  1291
interpretation of abstract locales. INCOMPATIBILITY.
66804
3f9bb52082c4 avoid name clashes on interpretation of abstract locales
haftmann
parents: 66803
diff changeset
  1292
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1293
* Predicate coprime is now a real definition, not a mere abbreviation.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1294
INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1295
66803
dd8922885a68 avoid trivial definition
haftmann
parents: 66801
diff changeset
  1296
* Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
dd8922885a68 avoid trivial definition
haftmann
parents: 66801
diff changeset
  1297
INCOMPATIBILITY.
dd8922885a68 avoid trivial definition
haftmann
parents: 66801
diff changeset
  1298
68373
f254e383bfe9 NEWS: infinite products
paulson <lp15@cam.ac.uk>
parents: 68370
diff changeset
  1299
* The relator rel_filter on filters has been strengthened to its
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1300
canonical categorical definition with better properties.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1301
INCOMPATIBILITY.
67616
1d005f514417 strengthen filter relator to canonical categorical definition with better properties
Andreas Lochbihler
parents: 67591
diff changeset
  1302
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents: 67999
diff changeset
  1303
* Generalized linear algebra involving linear, span, dependent, dim
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents: 67999
diff changeset
  1304
from type class real_vector to locales module and vector_space.
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents: 67999
diff changeset
  1305
Renamed:
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1306
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1307
  span_inc ~> span_superset
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1308
  span_superset ~> span_base
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1309
  span_eq ~> span_eq_iff
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1310
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1311
INCOMPATIBILITY.
66844
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
  1312
66937
a1a4a5e2933a rule out pathologic instances
haftmann
parents: 66909
diff changeset
  1313
* Class linordered_semiring_1 covers zero_less_one also, ruling out
a1a4a5e2933a rule out pathologic instances
haftmann
parents: 66909
diff changeset
  1314
pathologic instances. Minor INCOMPATIBILITY.
a1a4a5e2933a rule out pathologic instances
haftmann
parents: 66909
diff changeset
  1315
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1316
* Theory HOL.List: functions "sorted_wrt" and "sorted" now compare every
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1317
element in a list to all following elements, not just the next one.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1318
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1319
* Theory HOL.List syntax:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1320
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1321
  - filter-syntax "[x <- xs. P]" is no longer output syntax, but only
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1322
    input syntax
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1323
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1324
  - list comprehension syntax now supports tuple patterns in "pat <- xs"
68249
949d93804740 First step to remove nonstandard "[x <- xs. P]" syntax: only input
nipkow
parents: 68246
diff changeset
  1325
68450
41de07c7a0f3 Map.empty now qualified to avoid name clashes
nipkow
parents: 68404
diff changeset
  1326
* Theory Map: "empty" must now be qualified as "Map.empty".
41de07c7a0f3 Map.empty now qualified to avoid name clashes
nipkow
parents: 68404
diff changeset
  1327
67051
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 67043
diff changeset
  1328
* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 67043
diff changeset
  1329
68100
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
  1330
* Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
  1331
clash with fact mod_mult_self4 (on more generic semirings).
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
  1332
INCOMPATIBILITY.
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
  1333
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
  1334
* Eliminated some theorem aliasses:
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
  1335
  even_times_iff ~> even_mult_iff
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
  1336
  mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
  1337
  even_of_nat ~> even_int_iff
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
  1338
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
  1339
INCOMPATIBILITY.
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
  1340
68157
057d5b4ce47e removed some non-essential rules
haftmann
parents: 68125
diff changeset
  1341
* Eliminated some theorem duplicate variations:
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1342
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1343
  - dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1344
  - mod_Suc_eq_Suc_mod can be replaced by mod_Suc
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1345
  - mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1346
  - mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1347
  - the witness of mod_eqD can be given directly as "_ div _"
68157
057d5b4ce47e removed some non-essential rules
haftmann
parents: 68125
diff changeset
  1348
057d5b4ce47e removed some non-essential rules
haftmann
parents: 68125
diff changeset
  1349
INCOMPATIBILITY.
057d5b4ce47e removed some non-essential rules
haftmann
parents: 68125
diff changeset
  1350
68260
61188c781cdd avoid overaggressive classical rule
haftmann
parents: 68249
diff changeset
  1351
* Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1352
longer aggresively destroyed to "\<exists>q. m = d * q". INCOMPATIBILITY, adding
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1353
"elim!: dvd" to classical proof methods in most situations restores
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1354
broken proofs.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1355
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1356
* Theory HOL-Library.Conditional_Parametricity provides command
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1357
'parametric_constant' for proving parametricity of non-recursive
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1358
definitions. For constants that are not fully parametric the command
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1359
will infer conditions on relations (e.g., bi_unique, bi_total, or type
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1360
class conditions such as "respects 0") sufficient for parametricity. See
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1361
theory HOL-ex.Conditional_Parametricity_Examples for some examples.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1362
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1363
* Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1364
generator to generate code for algebraic types with lazy evaluation
68639
357fca99a65a more examples for Code_Lazy
Andreas Lochbihler
parents: 68568
diff changeset
  1365
semantics even in call-by-value target languages. See the theories
68647
wenzelm
parents: 68640
diff changeset
  1366
HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for some
wenzelm
parents: 68640
diff changeset
  1367
examples.
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1368
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1369
* Theory HOL-Library.Landau_Symbols has been moved here from AFP.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1370
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1371
* Theory HOL-Library.Old_Datatype no longer provides the legacy command
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1372
'old_datatype'. INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1373
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1374
* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1375
instances of rat, real, complex as factorial rings etc. Import
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1376
HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1377
INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1378
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1379
* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1380
infix/prefix notation.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1381
68543
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1382
* Session HOL-Algebra: revamped with much new material. The set of
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1383
isomorphisms between two groups is now denoted iso rather than iso_set.
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1384
INCOMPATIBILITY.
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1385
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1386
* Session HOL-Analysis: the Arg function now respects the same interval
c87e1adb91af misc tuning for release;
wenzelm
parents: 68541
diff changeset
  1387
as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi.
68499
d4312962161a Rationalisation of complex transcendentals, esp the Arg function
paulson <lp15@cam.ac.uk>
parents: 68484
diff changeset
  1388
INCOMPATIBILITY.
d4312962161a Rationalisation of complex transcendentals, esp the Arg function
paulson <lp15@cam.ac.uk>
parents: 68484
diff changeset
  1389
68548
wenzelm
parents: 68547
diff changeset
  1390
* Session HOL-Analysis: the functions zorder, zer_poly, porder and
wenzelm
parents: 68547
diff changeset
  1391
pol_poly have been redefined. All related lemmas have been reworked.
68531
7c6f812afdc4 NEWS and CONTRIBUTORS
Wenda Li <wl302@cam.ac.uk>
parents: 68523
diff changeset
  1392
INCOMPATIBILITY.
7c6f812afdc4 NEWS and CONTRIBUTORS
Wenda Li <wl302@cam.ac.uk>
parents: 68523
diff changeset
  1393
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
  1394
* Session HOL