NEWS
author wenzelm
Wed, 27 Jun 2018 20:31:22 +0200
changeset 68523 ccacc84e0251
parent 68522 d9cbc1e8644d
child 68531 7c6f812afdc4
child 68540 000a0e062529
permissions -rw-r--r--
clarified settings -- avoid hard-wired directories; tuned documentation;
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
68391
9b4f60bdad54 updated for release;
wenzelm
parents: 68373
diff changeset
     7
New in Isabelle2018 (August 2018)
9b4f60bdad54 updated for release;
wenzelm
parents: 68373
diff changeset
     8
---------------------------------
66651
435cb8d69e27 back to post-release mode -- after fork point;
wenzelm
parents: 66650
diff changeset
     9
66712
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 66688
diff changeset
    10
*** General ***
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 66688
diff changeset
    11
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    12
* Session-qualified theory names are mandatory: it is no longer possible
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    13
to refer to unqualified theories from the parent session.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    14
INCOMPATIBILITY for old developments that have not been updated to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    15
Isabelle2017 yet (using the "isabelle imports" tool).
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    16
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    17
* Only the most fundamental theory names are global, usually the entry
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    18
points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    19
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    20
formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    21
67446
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
    22
* Marginal comments need to be written exclusively in the new-style form
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
    23
"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
    24
supported. INCOMPATIBILITY, use the command-line tool "isabelle
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
    25
update_comments" to update existing theory files.
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67433
diff changeset
    26
67507
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
    27
* Old-style inner comments (* ... *) within the term language are legacy
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
    28
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
    29
instead.
5db077cfe1b2 old-style inner comments are legacy;
wenzelm
parents: 67448
diff changeset
    30
67402
nipkow
parents: 67400
diff changeset
    31
* The "op <infix-op>" syntax for infix operators has been replaced by
67400
nipkow
parents: 67398
diff changeset
    32
"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
nipkow
parents: 67398
diff changeset
    33
be a space between the "*" and the corresponding parenthesis.
nipkow
parents: 67398
diff changeset
    34
INCOMPATIBILITY.
67398
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67395
diff changeset
    35
There is an Isabelle tool "update_op" that converts theory and ML files
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67395
diff changeset
    36
to the new syntax. Because it is based on regular expression matching,
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67395
diff changeset
    37
the result may need a bit of manual postprocessing. Invoking "isabelle
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67395
diff changeset
    38
update_op" converts all files in the current directory (recursively).
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67395
diff changeset
    39
In case you want to exclude conversion of ML files (because the tool
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67395
diff changeset
    40
frequently also converts ML's "op" syntax), use option "-m".
5eb932e604a2 Manual updates towards conversion of "op" syntax
nipkow
parents: 67395
diff changeset
    41
67013
335a7dce7cb3 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents: 66994
diff changeset
    42
* 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
    43
INCOMPATIBILITY.
335a7dce7cb3 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents: 66994
diff changeset
    44
66757
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
    45
* Command 'external_file' declares the formal dependency on the given
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
    46
file name, such that the Isabelle build process knows about it, but
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
    47
without specific Prover IDE management.
e32750d7acb4 added command 'external_file';
wenzelm
parents: 66745
diff changeset
    48
66759
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
    49
* Session ROOT entries no longer allow specification of 'files'. Rare
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
    50
INCOMPATIBILITY, use command 'external_file' within a proper theory
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
    51
context.
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66757
diff changeset
    52
66764
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
    53
* 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
    54
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
    55
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
    56
-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
    57
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
    58
  isabelle build -D '~~/src/ZF'
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
    59
67263
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67262
diff changeset
    60
* The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67262
diff changeset
    61
use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67262
diff changeset
    62
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    63
* In HTML output, the Isabelle symbol "\<hyphen>" is rendered as explicit
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    64
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
    65
U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    66
output.
67305
ecb74607063f more robust hyphen (see also "Soft hyphen (SHY) – a hard problem?" http://jkorpela.fi/shy.html);
wenzelm
parents: 67304
diff changeset
    67
66712
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 66688
diff changeset
    68
67261
wenzelm
parents: 67248
diff changeset
    69
*** Isabelle/jEdit Prover IDE ***
66768
f27488f47a47 completion supports theory header imports;
wenzelm
parents: 66764
diff changeset
    70
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    71
* The command-line tool "isabelle jedit" provides more flexible options
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    72
for session management:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    73
68472
581a1bfec8ad clarified documentation;
wenzelm
parents: 68469
diff changeset
    74
  - option -R builds an auxiliary logic image with all theories from
581a1bfec8ad clarified documentation;
wenzelm
parents: 68469
diff changeset
    75
    other sessions that are not already present in its parent
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    76
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    77
  - 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
    78
    descendants (this reduces startup time for big projects like AFP)
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    79
68472
581a1bfec8ad clarified documentation;
wenzelm
parents: 68469
diff changeset
    80
  - option -A specifies an alternative ancestor session for options -R
581a1bfec8ad clarified documentation;
wenzelm
parents: 68469
diff changeset
    81
    and -S
581a1bfec8ad clarified documentation;
wenzelm
parents: 68469
diff changeset
    82
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    83
  Examples:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    84
    isabelle jedit -R HOL-Number_Theory
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    85
    isabelle jedit -R HOL-Number_Theory -A HOL
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    86
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    87
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    88
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    89
* PIDE markup for session ROOT files: allows to complete session names,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    90
follow links to theories and document files etc.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    91
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    92
* Completion supports theory header imports, using theory base name.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    93
E.g. "Prob" may be completed to "HOL-Probability.Probability".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    94
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    95
* Named control symbols (without special Unicode rendering) are shown as
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    96
bold-italic keyword. This is particularly useful for the short form of
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    97
antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    98
"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
    99
arguments into this format.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   100
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   101
* Completion provides templates for named symbols with arguments,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   102
e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   103
68368
wenzelm
parents: 68364
diff changeset
   104
* Slightly more parallel checking, notably for high priority print
wenzelm
parents: 68364
diff changeset
   105
functions (e.g. State output).
wenzelm
parents: 68364
diff changeset
   106
68080
17f79ae49401 set view title dynamically;
wenzelm
parents: 68073
diff changeset
   107
* The view title is set dynamically, according to the Isabelle
17f79ae49401 set view title dynamically;
wenzelm
parents: 68073
diff changeset
   108
distribution and the logic session name. The user can override this via
17f79ae49401 set view title dynamically;
wenzelm
parents: 68073
diff changeset
   109
set-view-title (stored persistently in $JEDIT_SETTINGS/perspective.xml).
17f79ae49401 set view title dynamically;
wenzelm
parents: 68073
diff changeset
   110
67395
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67381
diff changeset
   111
* 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
   112
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
   113
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
   114
67248
68177abb2988 isabelle.preview presents bibtex database files as well;
wenzelm
parents: 67246
diff changeset
   115
* Action "isabelle.preview" is able to present more file formats,
67266
wenzelm
parents: 67263
diff changeset
   116
notably bibtex database files and ML files.
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67224
diff changeset
   117
67262
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67261
diff changeset
   118
* Action "isabelle.draft" is similar to "isabelle.preview", but shows a
68067
b91c4acc1aaf clarified menu actions;
wenzelm
parents: 68033
diff changeset
   119
plain-text document draft. Both are available via the menu "Plugins /
b91c4acc1aaf clarified menu actions;
wenzelm
parents: 68033
diff changeset
   120
Isabelle".
67262
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67261
diff changeset
   121
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   122
* Bibtex database files (.bib) are semantically checked.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   123
67304
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
   124
* 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
   125
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
   126
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
   127
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
   128
Unicode content when saving the file.
3cf05d7cf174 more robust treatment of conflicts with existing Unicode text;
wenzelm
parents: 67303
diff changeset
   129
67993
wenzelm
parents: 67928
diff changeset
   130
* Update to jedit-5.5.0, the latest release.
wenzelm
parents: 67928
diff changeset
   131
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67224
diff changeset
   132
67261
wenzelm
parents: 67248
diff changeset
   133
*** Isabelle/VSCode Prover IDE ***
wenzelm
parents: 67248
diff changeset
   134
wenzelm
parents: 67248
diff changeset
   135
* HTML preview of theories and other file-formats similar to
wenzelm
parents: 67248
diff changeset
   136
Isabelle/jEdit.
wenzelm
parents: 67248
diff changeset
   137
66768
f27488f47a47 completion supports theory header imports;
wenzelm
parents: 66764
diff changeset
   138
67140
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   139
*** Document preparation ***
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   140
67448
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   141
* Formal comments work uniformly in outer syntax, inner syntax (term
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   142
language), Isabelle/ML and some other embedded languages of Isabelle.
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   143
See also "Document comments" in the isar-ref manual. The following forms
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   144
are supported:
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   145
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   146
  - marginal text comment: \<comment> \<open>\<dots>\<close>
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   147
  - canceled source: \<^cancel>\<open>\<dots>\<close>
dbb1f02e667d more documentation;
wenzelm
parents: 67446
diff changeset
   148
  - raw LaTeX: \<^latex>\<open>\<dots>\<close>
67413
2555713586c8 added \<^cancel> operator for unused text;
wenzelm
parents: 67402
diff changeset
   149
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 67368
diff changeset
   150
* Outside of the inner theory body, the default presentation context is
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 67368
diff changeset
   151
theory Pure. Thus elementary antiquotations may be used in markup
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 67368
diff changeset
   152
commands (e.g. 'chapter', 'section', 'text') and formal comments.
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 67368
diff changeset
   153
68513
88b0e63d58a5 updated documentation;
wenzelm
parents: 68484
diff changeset
   154
* System option "document_tags" specifies alternative command tags. This
88b0e63d58a5 updated documentation;
wenzelm
parents: 68484
diff changeset
   155
is occasionally useful to control the global visibility of commands via
88b0e63d58a5 updated documentation;
wenzelm
parents: 68484
diff changeset
   156
session options (e.g. in ROOT).
67140
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   157
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   158
* Document markup commands ('section', 'text' etc.) are implicitly
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   159
tagged as "document" and visible by default. This avoids the application
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   160
of option "document_tags" to these commands.
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   161
67145
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
   162
* Isabelle names are mangled into LaTeX macro names to allow the full
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
   163
identifier syntax with underscore, prime, digits. This is relevant for
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
   164
antiquotations in control symbol notation, e.g. \<^const_name> becomes
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
   165
\isactrlconstUNDERSCOREname.
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 67140
diff changeset
   166
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   167
* Document preparation with skip_proofs option now preserves the content
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   168
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
   169
68484
59793df7f853 clarified document antiquotation @{theory};
wenzelm
parents: 68472
diff changeset
   170
* Document antiquotation @{theory name} requires the long
59793df7f853 clarified document antiquotation @{theory};
wenzelm
parents: 68472
diff changeset
   171
session-qualified theory name: this is what users reading the text
59793df7f853 clarified document antiquotation @{theory};
wenzelm
parents: 68472
diff changeset
   172
normally need to import.
59793df7f853 clarified document antiquotation @{theory};
wenzelm
parents: 68472
diff changeset
   173
67219
81e9804b2014 added document antiquotation @{session name};
wenzelm
parents: 67215
diff changeset
   174
* Document antiquotation @{session name} checks and prints the given
81e9804b2014 added document antiquotation @{session name};
wenzelm
parents: 67215
diff changeset
   175
session name verbatim.
81e9804b2014 added document antiquotation @{session name};
wenzelm
parents: 67215
diff changeset
   176
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   177
* Document antiquotation @{cite} now checks the given Bibtex entries
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   178
against the Bibtex database files -- only in batch-mode session builds.
67157
d0657c8b7616 clarified document preparation vs. skip_proofs;
wenzelm
parents: 67145
diff changeset
   179
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 67173
diff changeset
   180
* 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
   181
Isabelle/Scala, with simplified arguments and explicit errors from the
67203
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67199
diff changeset
   182
latex and bibtex process. Minor INCOMPATIBILITY.
67173
e746db6db903 more explicit latex errors;
wenzelm
parents: 67157
diff changeset
   183
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   184
* Session ROOT entry: empty 'document_files' means there is no document
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   185
for this session. There is no need to specify options [document = false]
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   186
anymore.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   187
67140
386a31d6d17a more documentation;
wenzelm
parents: 67133
diff changeset
   188
67702
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67616
diff changeset
   189
*** Isar ***
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67616
diff changeset
   190
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67616
diff changeset
   191
* 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
   192
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
   193
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
   194
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
   195
(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
   196
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   197
* The old 'def' command has been discontinued (legacy since
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   198
Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   199
object-logic equality or equivalence.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   200
67740
b6ce18784872 Proper rewrite morphisms in locale instances.
ballarin
parents: 67718
diff changeset
   201
* Rewrites clauses (keyword 'rewrites') were moved into the locale
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   202
expression syntax, where they are part of locale instances. In
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   203
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
   204
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
   205
rewriting may need to be pulled up into the surrounding theory.
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   206
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   207
* For 'rewrites' clauses, if activating a locale instance fails, fall
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   208
back to reading the clause first. This helps avoid qualification of
67764
0f8cb5568b63 Drop rewrites after defines in interpretations.
ballarin
parents: 67741
diff changeset
   209
locale instances where the qualifier's sole purpose is avoiding
0f8cb5568b63 Drop rewrites after defines in interpretations.
ballarin
parents: 67741
diff changeset
   210
duplicate constant declarations.
67741
d5a7f2c54655 Fall back to reading rewrite morphism first if activation fails without it.
ballarin
parents: 67740
diff changeset
   211
68403
223172b97d0b reorient -> split; documented split
nipkow
parents: 68373
diff changeset
   212
* Proof method 'simp' now supports a new modifier 'flip:' followed by a list
223172b97d0b reorient -> split; documented split
nipkow
parents: 68373
diff changeset
   213
of theorems. Each of these theorems is removed from the simpset
223172b97d0b reorient -> split; documented split
nipkow
parents: 68373
diff changeset
   214
(without warning if it is not there) and the symmetric version of the theorem
223172b97d0b reorient -> split; documented split
nipkow
parents: 68373
diff changeset
   215
(i.e. lhs and rhs exchanged) is added to the simpset.
223172b97d0b reorient -> split; documented split
nipkow
parents: 68373
diff changeset
   216
For 'auto' and friends the modifier is "simp flip:".
223172b97d0b reorient -> split; documented split
nipkow
parents: 68373
diff changeset
   217
67702
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67616
diff changeset
   218
67718
17874d43d3b3 notation for dummy sort;
wenzelm
parents: 67702
diff changeset
   219
*** Pure ***
17874d43d3b3 notation for dummy sort;
wenzelm
parents: 67702
diff changeset
   220
17874d43d3b3 notation for dummy sort;
wenzelm
parents: 67702
diff changeset
   221
* The inner syntax category "sort" now includes notation "_" for the
17874d43d3b3 notation for dummy sort;
wenzelm
parents: 67702
diff changeset
   222
dummy sort: it is effectively ignored in type-inference.
17874d43d3b3 notation for dummy sort;
wenzelm
parents: 67702
diff changeset
   223
17874d43d3b3 notation for dummy sort;
wenzelm
parents: 67702
diff changeset
   224
66661
fdab65297bd6 real oracle
blanchet
parents: 66651
diff changeset
   225
*** HOL ***
fdab65297bd6 real oracle
blanchet
parents: 66651
diff changeset
   226
68028
1f9f973eed2a proper datatype for 8-bit characters
haftmann
parents: 68027
diff changeset
   227
* Clarified relationship of characters, strings and code generation:
1f9f973eed2a proper datatype for 8-bit characters
haftmann
parents: 68027
diff changeset
   228
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   229
  - Type "char" is now a proper datatype of 8-bit values.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   230
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   231
  - Conversions "nat_of_char" and "char_of_nat" are gone; use more
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   232
    general conversions "of_char" and "char_of" with suitable type
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   233
    constraints instead.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   234
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   235
  - The zero character is just written "CHR 0x00", not "0" any longer.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   236
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   237
  - Type "String.literal" (for code generation) is now isomorphic to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   238
    lists of 7-bit (ASCII) values; concrete values can be written as
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   239
    "STR ''...''" for sequences of printable characters and "STR 0x..."
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   240
    for one single ASCII code point given as hexadecimal numeral.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   241
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   242
  - Type "String.literal" supports concatenation "... + ..." for all
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   243
    standard target languages.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   244
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   245
  - Theory HOL-Library.Code_Char is gone; study the explanations
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   246
    concerning "String.literal" in the tutorial on code generation to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   247
    get an idea how target-language string literals can be converted to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   248
    HOL string values and vice versa.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   249
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   250
  - Session Imperative-HOL: operation "raise" directly takes a value of
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   251
    type "String.literal" as argument, not type "string".
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   252
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   253
INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   254
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   255
* Code generation: Code generation takes an explicit option
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   256
"case_insensitive" to accomodate case-insensitive file systems.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   257
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   258
* 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
   259
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   260
* New, more general, axiomatization of complete_distrib_lattice. The
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   261
former axioms:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   262
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   263
  "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
   264
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   265
are replaced by:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   266
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   267
  "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
   268
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   269
The instantiations of sets and functions as complete_distrib_lattice are
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   270
moved to Hilbert_Choice.thy because their proofs need the Hilbert choice
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   271
operator. The dual of this property is also proved in theory
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   272
HOL.Hilbert_Choice.
67831
07f5588f2735 Removed stray 'sledgehammer' invocation
Manuel Eberl <eberlm@in.tum.de>
parents: 67830
diff changeset
   273
67999
1b05f74f2e5f tidying up including contributions from Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents: 67993
diff changeset
   274
* 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
   275
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
   276
67525
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
   277
* Clarifed theorem names:
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
   278
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
   279
  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
   280
  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
   281
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
   282
Minor INCOMPATIBILITY.
5d04d7bcd5f6 avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents: 67510
diff changeset
   283
66661
fdab65297bd6 real oracle
blanchet
parents: 66651
diff changeset
   284
* SMT module:
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   285
66661
fdab65297bd6 real oracle
blanchet
parents: 66651
diff changeset
   286
  - The 'smt_oracle' option is now necessary when using the 'smt' method
66662
4b10fa05423b document incompatibility
blanchet
parents: 66661
diff changeset
   287
    with a solver other than Z3. INCOMPATIBILITY.
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   288
66844
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   289
  - The encoding to first-order logic is now more complete in the
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   290
    presence of higher-order quantifiers. An 'smt_explicit_application'
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   291
    option has been added to control this. INCOMPATIBILITY.
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   292
66804
3f9bb52082c4 avoid name clashes on interpretation of abstract locales
haftmann
parents: 66803
diff changeset
   293
* Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
66844
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   294
sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   295
interpretation of abstract locales. INCOMPATIBILITY.
66804
3f9bb52082c4 avoid name clashes on interpretation of abstract locales
haftmann
parents: 66803
diff changeset
   296
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   297
* Predicate coprime is now a real definition, not a mere abbreviation.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   298
INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   299
66803
dd8922885a68 avoid trivial definition
haftmann
parents: 66801
diff changeset
   300
* Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
dd8922885a68 avoid trivial definition
haftmann
parents: 66801
diff changeset
   301
INCOMPATIBILITY.
dd8922885a68 avoid trivial definition
haftmann
parents: 66801
diff changeset
   302
68373
f254e383bfe9 NEWS: infinite products
paulson <lp15@cam.ac.uk>
parents: 68370
diff changeset
   303
* The relator rel_filter on filters has been strengthened to its
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   304
canonical categorical definition with better properties.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   305
INCOMPATIBILITY.
67616
1d005f514417 strengthen filter relator to canonical categorical definition with better properties
Andreas Lochbihler
parents: 67591
diff changeset
   306
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents: 67999
diff changeset
   307
* 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
   308
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
   309
Renamed:
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   310
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   311
  span_inc ~> span_superset
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   312
  span_superset ~> span_base
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   313
  span_eq ~> span_eq_iff
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   314
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   315
INCOMPATIBILITY.
66844
0746d4781674 tuned whitespace;
wenzelm
parents: 66843
diff changeset
   316
66937
a1a4a5e2933a rule out pathologic instances
haftmann
parents: 66909
diff changeset
   317
* Class linordered_semiring_1 covers zero_less_one also, ruling out
a1a4a5e2933a rule out pathologic instances
haftmann
parents: 66909
diff changeset
   318
pathologic instances. Minor INCOMPATIBILITY.
a1a4a5e2933a rule out pathologic instances
haftmann
parents: 66909
diff changeset
   319
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   320
* Theory HOL.List: functions "sorted_wrt" and "sorted" now compare every
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   321
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
   322
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   323
* Theory HOL.List syntax:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   324
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   325
  - filter-syntax "[x <- xs. P]" is no longer output syntax, but only
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   326
    input syntax
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   327
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   328
  - 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
   329
68450
41de07c7a0f3 Map.empty now qualified to avoid name clashes
nipkow
parents: 68404
diff changeset
   330
* Theory Map: "empty" must now be qualified as "Map.empty".
41de07c7a0f3 Map.empty now qualified to avoid name clashes
nipkow
parents: 68404
diff changeset
   331
67051
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 67043
diff changeset
   332
* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 67043
diff changeset
   333
68100
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   334
* Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   335
clash with fact mod_mult_self4 (on more generic semirings).
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   336
INCOMPATIBILITY.
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   337
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   338
* Eliminated some theorem aliasses:
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   339
  even_times_iff ~> even_mult_iff
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   340
  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
   341
  even_of_nat ~> even_int_iff
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   342
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   343
INCOMPATIBILITY.
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 68080
diff changeset
   344
68157
057d5b4ce47e removed some non-essential rules
haftmann
parents: 68125
diff changeset
   345
* Eliminated some theorem duplicate variations:
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   346
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   347
  - 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
   348
  - mod_Suc_eq_Suc_mod can be replaced by mod_Suc
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   349
  - mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   350
  - 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
   351
  - the witness of mod_eqD can be given directly as "_ div _"
68157
057d5b4ce47e removed some non-essential rules
haftmann
parents: 68125
diff changeset
   352
057d5b4ce47e removed some non-essential rules
haftmann
parents: 68125
diff changeset
   353
INCOMPATIBILITY.
057d5b4ce47e removed some non-essential rules
haftmann
parents: 68125
diff changeset
   354
68260
61188c781cdd avoid overaggressive classical rule
haftmann
parents: 68249
diff changeset
   355
* 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
   356
longer aggresively destroyed to "\<exists>q. m = d * q". INCOMPATIBILITY, adding
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   357
"elim!: dvd" to classical proof methods in most situations restores
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   358
broken proofs.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   359
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   360
* Theory HOL-Library.Conditional_Parametricity provides command
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   361
'parametric_constant' for proving parametricity of non-recursive
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   362
definitions. For constants that are not fully parametric the command
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   363
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
   364
class conditions such as "respects 0") sufficient for parametricity. See
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   365
theory HOL-ex.Conditional_Parametricity_Examples for some examples.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   366
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   367
* Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   368
generator to generate code for algebraic types with lazy evaluation
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   369
semantics even in call-by-value target languages. See theory
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   370
HOL-Codegenerator_Test.Code_Lazy_Test for some examples.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   371
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   372
* Theory HOL-Library.Landau_Symbols has been moved here from AFP.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   373
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   374
* Theory HOL-Library.Old_Datatype no longer provides the legacy command
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   375
'old_datatype'. INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   376
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   377
* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   378
instances of rat, real, complex as factorial rings etc. Import
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   379
HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   380
INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   381
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   382
* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   383
infix/prefix notation.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   384
68466
3d8241f4198b corrections to markup
paulson <lp15@cam.ac.uk>
parents: 68450
diff changeset
   385
* Session HOL-Algebra: Revamped with much new material.
3d8241f4198b corrections to markup
paulson <lp15@cam.ac.uk>
parents: 68450
diff changeset
   386
The set of isomorphisms between two groups is now denoted iso rather than iso_set.
3d8241f4198b corrections to markup
paulson <lp15@cam.ac.uk>
parents: 68450
diff changeset
   387
INCOMPATIBILITY.
3d8241f4198b corrections to markup
paulson <lp15@cam.ac.uk>
parents: 68450
diff changeset
   388
68499
d4312962161a Rationalisation of complex transcendentals, esp the Arg function
paulson <lp15@cam.ac.uk>
parents: 68484
diff changeset
   389
* Session HOL-Analysis: the Arg function now respects the same interval as
d4312962161a Rationalisation of complex transcendentals, esp the Arg function
paulson <lp15@cam.ac.uk>
parents: 68484
diff changeset
   390
Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi. 
d4312962161a Rationalisation of complex transcendentals, esp the Arg function
paulson <lp15@cam.ac.uk>
parents: 68484
diff changeset
   391
INCOMPATIBILITY.
d4312962161a Rationalisation of complex transcendentals, esp the Arg function
paulson <lp15@cam.ac.uk>
parents: 68484
diff changeset
   392
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   393
* Session HOL-Analysis: infinite products, Moebius functions, the
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   394
Riemann mapping theorem, the Vitali covering theorem,
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   395
change-of-variables results for integration and measures.
68260
61188c781cdd avoid overaggressive classical rule
haftmann
parents: 68249
diff changeset
   396
68522
d9cbc1e8644d example for Types_To_Sets: transfer from type-based linear algebra to subspaces
immler
parents: 68515
diff changeset
   397
* Session HOL-Types_To_Sets: more tool support
d9cbc1e8644d example for Types_To_Sets: transfer from type-based linear algebra to subspaces
immler
parents: 68515
diff changeset
   398
(unoverload_type combines internalize_sorts and unoverload) and larger
d9cbc1e8644d example for Types_To_Sets: transfer from type-based linear algebra to subspaces
immler
parents: 68515
diff changeset
   399
experimental application (type based linear algebra transferred to linear
d9cbc1e8644d example for Types_To_Sets: transfer from type-based linear algebra to subspaces
immler
parents: 68515
diff changeset
   400
algebra on subspaces).
d9cbc1e8644d example for Types_To_Sets: transfer from type-based linear algebra to subspaces
immler
parents: 68515
diff changeset
   401
66651
435cb8d69e27 back to post-release mode -- after fork point;
wenzelm
parents: 66650
diff changeset
   402
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68100
diff changeset
   403
*** ML ***
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68100
diff changeset
   404
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68100
diff changeset
   405
* Operation Export.export emits theory exports (arbitrary blobs), which
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68100
diff changeset
   406
are stored persistently in the session build database.
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68100
diff changeset
   407
68276
cbee43ff4ceb added command 'ML_export';
wenzelm
parents: 68260
diff changeset
   408
* Command 'ML_export' exports ML toplevel bindings to the global
cbee43ff4ceb added command 'ML_export';
wenzelm
parents: 68260
diff changeset
   409
bootstrap environment of the ML process. This allows ML evaluation
cbee43ff4ceb added command 'ML_export';
wenzelm
parents: 68260
diff changeset
   410
without a formal theory context, e.g. in command-line tools like
cbee43ff4ceb added command 'ML_export';
wenzelm
parents: 68260
diff changeset
   411
"isabelle process".
cbee43ff4ceb added command 'ML_export';
wenzelm
parents: 68260
diff changeset
   412
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68100
diff changeset
   413
66729
wenzelm
parents: 66712
diff changeset
   414
*** System ***
wenzelm
parents: 66712
diff changeset
   415
67088
89e82aed7813 Mac OS X 10.10 Yosemite is baseline;
wenzelm
parents: 67069
diff changeset
   416
* Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no
89e82aed7813 Mac OS X 10.10 Yosemite is baseline;
wenzelm
parents: 67069
diff changeset
   417
longer supported.
89e82aed7813 Mac OS X 10.10 Yosemite is baseline;
wenzelm
parents: 67069
diff changeset
   418
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   419
* Linux and Windows/Cygwin is for x86_64 only, old 32bit platform
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   420
support has been discontinued.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   421
66906
03a96b8c7c06 updated to jdk-8u152, which is for x86_64 only;
wenzelm
parents: 66851
diff changeset
   422
* Java runtime is for x86_64 only. Corresponding Isabelle settings have
03a96b8c7c06 updated to jdk-8u152, which is for x86_64 only;
wenzelm
parents: 66851
diff changeset
   423
been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS,
03a96b8c7c06 updated to jdk-8u152, which is for x86_64 only;
wenzelm
parents: 66851
diff changeset
   424
instead of former 32/64 variants. INCOMPATIBILITY.
03a96b8c7c06 updated to jdk-8u152, which is for x86_64 only;
wenzelm
parents: 66851
diff changeset
   425
68003
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   426
* Old settings ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM should be
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   427
phased out due to unclear preference of 32bit vs. 64bit architecture.
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   428
Explicit GNU bash expressions are now preferred, for example (with
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   429
quotes):
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   430
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   431
  #Posix executables (Unix or Cygwin), with preference for 64bit
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   432
  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   433
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   434
  #native Windows or Unix executables, with preference for 64bit
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   435
  "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   436
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   437
  #native Windows (32bit) or Unix executables (preference for 64bit)
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   438
  "${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}"
9b89d831dc80 prefer explicit 32/64 bit platform settings;
wenzelm
parents: 67999
diff changeset
   439
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66739
diff changeset
   440
* Command-line tool "isabelle build" supports new options:
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66739
diff changeset
   441
  - option -B NAME: include session NAME and all descendants
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66739
diff changeset
   442
  - option -S: only observe changes of sources, not heap images
66841
5c32a072ca8b added isablle build option -f;
wenzelm
parents: 66826
diff changeset
   443
  - option -f: forces a fresh build
66737
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66729
diff changeset
   444
66843
be08a7691c62 clarified meta_digest;
wenzelm
parents: 66841
diff changeset
   445
* Command-line tool "isabelle build" takes "condition" options with the
be08a7691c62 clarified meta_digest;
wenzelm
parents: 66841
diff changeset
   446
corresponding environment values into account, when determining the
be08a7691c62 clarified meta_digest;
wenzelm
parents: 66841
diff changeset
   447
up-to-date status of a session.
be08a7691c62 clarified meta_digest;
wenzelm
parents: 66841
diff changeset
   448
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   449
* The command-line tool "dump" dumps information from the cumulative
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   450
PIDE session database: many sessions may be loaded into a given logic
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   451
image, results from all loaded theories are written to the output
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   452
directory.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   453
66851
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66844
diff changeset
   454
* Command-line tool "isabelle imports -I" also reports actual session
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66844
diff changeset
   455
imports. This helps to minimize the session dependency graph.
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66844
diff changeset
   456
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   457
* The command-line tool "export" and 'export_files' in session ROOT
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   458
entries retrieve theory exports from the session build database.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   459
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   460
* The command-line tools "isabelle server" and "isabelle client" provide
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   461
access to the Isabelle Server: it supports responsive session management
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   462
and concurrent use of theories, based on Isabelle/PIDE infrastructure.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   463
See also the "system" manual.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   464
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   465
* The command-line tool "isabelle update_comments" normalizes formal
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   466
comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   467
approximate the appearance in document output). This is more specific
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   468
than former "isabelle update_cartouches -c": the latter tool option has
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   469
been discontinued.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   470
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   471
* The command-line tool "isabelle mkroot" now always produces a document
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   472
outline: its options have been adapted accordingly. INCOMPATIBILITY.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   473
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   474
* The command-line tool "isabelle mkroot -I" initializes a Mercurial
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   475
repository for the generated session files.
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   476
68523
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
   477
* Settings ISABELLE_HEAPS + ISABELLE_BROWSER_INFO (or
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
   478
ISABELLE_HEAPS_SYSTEM + ISABELLE_BROWSER_INFO_SYSTEM in "system build
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
   479
mode") determine the directory locations of the main build artefacts --
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
   480
instead of hard-wired directories in ISABELLE_HOME_USER (or
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
   481
ISABELLE_HOME).
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
   482
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   483
* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   484
heap images and session databases are always stored in
68523
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
   485
$ISABELLE_HEAPS/$ML_IDENTIFIER (command-line default) or
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68522
diff changeset
   486
$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER (main Isabelle application or
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   487
"isabelle jedit -s" or "isabelle build -s").
67099
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 67088
diff changeset
   488
67199
wenzelm
parents: 67194
diff changeset
   489
* ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific
wenzelm
parents: 67194
diff changeset
   490
options for improved error reporting. Potential INCOMPATIBILITY with
wenzelm
parents: 67194
diff changeset
   491
unusual LaTeX installations, may have to adapt these settings.
wenzelm
parents: 67194
diff changeset
   492
68393
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   493
* Update to Poly/ML 5.7.1 with slightly improved performance and PIDE
b9989df11c78 misc tuning and updates for release;
wenzelm
parents: 68391
diff changeset
   494
markup for identifier bindings. It now uses The GNU Multiple Precision
67591
wenzelm
parents: 67525
diff changeset
   495
Arithmetic Library (libgmp) on all platforms, notably Mac OS X with
wenzelm
parents: 67525
diff changeset
   496
32/64 bit.
wenzelm
parents: 67525
diff changeset
   497
67099
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 67088
diff changeset
   498
66729
wenzelm
parents: 66712
diff changeset
   499
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   500
New in Isabelle2017 (October 2017)
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   501
----------------------------------
64439
2bafda87b524 back to post-release mode -- after fork point;
wenzelm
parents: 64391
diff changeset
   502
64986
b81a048960a3 more uniform use of Reconstruct.clean_proof_of;
wenzelm
parents: 64917
diff changeset
   503
*** General ***
b81a048960a3 more uniform use of Reconstruct.clean_proof_of;
wenzelm
parents: 64917
diff changeset
   504
66238
wenzelm
parents: 66181
diff changeset
   505
* Experimental support for Visual Studio Code (VSCode) as alternative
wenzelm
parents: 66181
diff changeset
   506
Isabelle/PIDE front-end, see also
66599
34b20f7236ea proper URL;
wenzelm
parents: 66574
diff changeset
   507
https://marketplace.visualstudio.com/items?itemName=makarius.Isabelle2017
66238
wenzelm
parents: 66181
diff changeset
   508
wenzelm
parents: 66181
diff changeset
   509
VSCode is a new type of application that continues the concepts of
wenzelm
parents: 66181
diff changeset
   510
"programmer's editor" and "integrated development environment" towards
wenzelm
parents: 66181
diff changeset
   511
fully semantic editing and debugging -- in a relatively light-weight
wenzelm
parents: 66181
diff changeset
   512
manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure.
wenzelm
parents: 66181
diff changeset
   513
Technically, VSCode is based on the Electron application framework
wenzelm
parents: 66181
diff changeset
   514
(Node.js + Chromium browser + V8), which is implemented in JavaScript
wenzelm
parents: 66181
diff changeset
   515
and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala
wenzelm
parents: 66181
diff changeset
   516
modules around a Language Server implementation.
wenzelm
parents: 66181
diff changeset
   517
65504
b80477da30eb some documentation;
wenzelm
parents: 65465
diff changeset
   518
* Theory names are qualified by the session name that they belong to.
66454
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
   519
This affects imports, but not the theory name space prefix (which is
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
   520
just the theory base name as before).
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
   521
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
   522
In order to import theories from other sessions, the ROOT file format
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
   523
provides a new 'sessions' keyword. In contrast, a theory that is
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
   524
imported in the old-fashioned manner via an explicit file-system path
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   525
belongs to the current session, and might cause theory name conflicts
66454
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
   526
later on. Theories that are imported from other sessions are excluded
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
   527
from the current session document. The command-line tool "isabelle
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
   528
imports" helps to update theory imports.
1a73ad1c06dd more NEWS;
wenzelm
parents: 66450
diff changeset
   529
65451
wenzelm
parents: 65448
diff changeset
   530
* The main theory entry points for some non-HOL sessions have changed,
wenzelm
parents: 65448
diff changeset
   531
to avoid confusion with the global name "Main" of the session HOL. This
wenzelm
parents: 65448
diff changeset
   532
leads to the follow renamings:
wenzelm
parents: 65448
diff changeset
   533
wenzelm
parents: 65448
diff changeset
   534
  CTT/Main.thy    ~>  CTT/CTT.thy
wenzelm
parents: 65448
diff changeset
   535
  ZF/Main.thy     ~>  ZF/ZF.thy
wenzelm
parents: 65448
diff changeset
   536
  ZF/Main_ZF.thy  ~>  ZF/ZF.thy
wenzelm
parents: 65448
diff changeset
   537
  ZF/Main_ZFC.thy ~>  ZF/ZFC.thy
wenzelm
parents: 65448
diff changeset
   538
  ZF/ZF.thy       ~>  ZF/ZF_Base.thy
wenzelm
parents: 65448
diff changeset
   539
wenzelm
parents: 65448
diff changeset
   540
INCOMPATIBILITY.
wenzelm
parents: 65448
diff changeset
   541
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   542
* Commands 'alias' and 'type_alias' introduce aliases for constants and
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   543
type constructors, respectively. This allows adhoc changes to name-space
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   544
accesses within global or local theory contexts, e.g. within a 'bundle'.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   545
64986
b81a048960a3 more uniform use of Reconstruct.clean_proof_of;
wenzelm
parents: 64917
diff changeset
   546
* Document antiquotations @{prf} and @{full_prf} output proof terms
b81a048960a3 more uniform use of Reconstruct.clean_proof_of;
wenzelm
parents: 64917
diff changeset
   547
(again) in the same way as commands 'prf' and 'full_prf'.
b81a048960a3 more uniform use of Reconstruct.clean_proof_of;
wenzelm
parents: 64917
diff changeset
   548
65055
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
   549
* Computations generated by the code generator can be embedded directly
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
   550
into ML, alongside with @{code} antiquotations, using the following
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
   551
antiquotations:
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
   552
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
   553
  @{computation ... terms: ... datatypes: ...} :
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
   554
    ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
   555
  @{computation_conv ... terms: ... datatypes: ...} :
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
   556
    (Proof.context -> 'ml -> conv) -> Proof.context -> conv
65045
b69ef432438d avoid Unicode that conflicts with Isabelle symbol rendering;
wenzelm
parents: 65042
diff changeset
   557
  @{computation_check terms: ... datatypes: ...} : Proof.context -> conv
65041
2525e680f94f basic documentation for computations
haftmann
parents: 65027
diff changeset
   558
65055
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
   559
See src/HOL/ex/Computations.thy,
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
   560
src/HOL/Decision_Procs/Commutative_Ring.thy and
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
   561
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
12189e86c49d tuned whitespace;
wenzelm
parents: 65050
diff changeset
   562
tutorial on code generation.
65041
2525e680f94f basic documentation for computations
haftmann
parents: 65027
diff changeset
   563
64986
b81a048960a3 more uniform use of Reconstruct.clean_proof_of;
wenzelm
parents: 64917
diff changeset
   564
64602
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 64593
diff changeset
   565
*** Prover IDE -- Isabelle/Scala/jEdit ***
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 64593
diff changeset
   566
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   567
* Session-qualified theory imports allow the Prover IDE to process
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   568
arbitrary theory hierarchies independently of the underlying logic
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   569
session image (e.g. option "isabelle jedit -l"), but the directory
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   570
structure needs to be known in advance (e.g. option "isabelle jedit -d"
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   571
or a line in the file $ISABELLE_HOME_USER/ROOTS).
64602
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 64593
diff changeset
   572
64842
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
   573
* The PIDE document model maintains file content independently of the
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
   574
status of jEdit editor buffers. Reloading jEdit buffers no longer causes
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
   575
changes of formal document content. Theory dependencies are always
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
   576
resolved internally, without the need for corresponding editor buffers.
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
   577
The system option "jedit_auto_load" has been discontinued: it is
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
   578
effectively always enabled.
9c69b495c05d more documentation;
wenzelm
parents: 64787
diff changeset
   579
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64846
diff changeset
   580
* The Theories dockable provides a "Purge" button, in order to restrict
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64846
diff changeset
   581
the document model to theories that are required for open editor
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64846
diff changeset
   582
buffers.
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64846
diff changeset
   583
66424
wenzelm
parents: 66345
diff changeset
   584
* The Theories dockable indicates the overall status of checking of each
wenzelm
parents: 66345
diff changeset
   585
entry. When all forked tasks of a theory are finished, the border is
wenzelm
parents: 66345
diff changeset
   586
painted with thick lines; remaining errors in this situation are
wenzelm
parents: 66345
diff changeset
   587
represented by a different border color.
wenzelm
parents: 66345
diff changeset
   588
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   589
* Automatic indentation is more careful to avoid redundant spaces in
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   590
intermediate situations. Keywords are indented after input (via typed
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   591
characters or completion); see also option "jedit_indent_input".
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   592
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   593
* Action "isabelle.preview" opens an HTML preview of the current theory
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   594
document in the default web browser.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   595
66574
e16b27bd3f76 reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
wenzelm
parents: 66563
diff changeset
   596
* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
e16b27bd3f76 reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
wenzelm
parents: 66563
diff changeset
   597
entry of the specified logic session in the editor, while its parent is
e16b27bd3f76 reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
wenzelm
parents: 66563
diff changeset
   598
used for formal checking.
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   599
66462
0a8277e9cfd6 officially allow restart of Isabelle plugin;
wenzelm
parents: 66455
diff changeset
   600
* The main Isabelle/jEdit plugin may be restarted manually (using the
0a8277e9cfd6 officially allow restart of Isabelle plugin;
wenzelm
parents: 66455
diff changeset
   601
jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
0a8277e9cfd6 officially allow restart of Isabelle plugin;
wenzelm
parents: 66455
diff changeset
   602
enabled at all times.
0a8277e9cfd6 officially allow restart of Isabelle plugin;
wenzelm
parents: 66455
diff changeset
   603
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   604
* Update to current jedit-5.4.0.
65329
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 65170
diff changeset
   605
64602
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 64593
diff changeset
   606
66149
4bf16fb7c14d deleting a code equation never leads to unimplemented function
haftmann
parents: 66135
diff changeset
   607
*** Pure ***
4bf16fb7c14d deleting a code equation never leads to unimplemented function
haftmann
parents: 66135
diff changeset
   608
4bf16fb7c14d deleting a code equation never leads to unimplemented function
haftmann
parents: 66135
diff changeset
   609
* Deleting the last code equations for a particular function using
4bf16fb7c14d deleting a code equation never leads to unimplemented function
haftmann
parents: 66135
diff changeset
   610
[code del] results in function with no equations (runtime abort) rather
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   611
than an unimplemented function (generation time abort). Use explicit
66665
ec78c84bfc44 spelling
haftmann
parents: 66650
diff changeset
   612
[[code drop:]] to enforce the latter. Minor INCOMPATIBILITY.
66149
4bf16fb7c14d deleting a code equation never leads to unimplemented function
haftmann
parents: 66135
diff changeset
   613
66310
e8d2862ec203 simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents: 66298
diff changeset
   614
* Proper concept of code declarations in code.ML:
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   615
  - Regular code declarations act only on the global theory level, being
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   616
    ignored with warnings if syntactically malformed.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   617
  - Explicitly global code declarations yield errors if syntactically
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   618
    malformed.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   619
  - Default code declarations are silently ignored if syntactically
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   620
    malformed.
66310
e8d2862ec203 simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents: 66298
diff changeset
   621
Minor INCOMPATIBILITY.
e8d2862ec203 simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents: 66298
diff changeset
   622
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   623
* Clarified and standardized internal data bookkeeping of code
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   624
declarations: history of serials allows to track potentially
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   625
non-monotonous declarations appropriately. Minor INCOMPATIBILITY.
66310
e8d2862ec203 simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents: 66298
diff changeset
   626
66149
4bf16fb7c14d deleting a code equation never leads to unimplemented function
haftmann
parents: 66135
diff changeset
   627
64593
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
   628
*** HOL ***
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
   629
66614
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents: 66599
diff changeset
   630
* The Nunchaku model finder is now part of "Main".
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents: 66599
diff changeset
   631
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   632
* SMT module:
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   633
  - A new option, 'smt_nat_as_int', has been added to translate 'nat' to
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   634
    'int' and benefit from the SMT solver's theory reasoning. It is
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   635
    disabled by default.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   636
  - The legacy module "src/HOL/Library/Old_SMT.thy" has been removed.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   637
  - Several small issues have been rectified in the 'smt' command.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   638
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   639
* (Co)datatype package: The 'size_gen_o_map' lemma is no longer
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   640
generated for datatypes with type class annotations. As a result, the
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   641
tactic that derives it no longer fails on nested datatypes. Slight
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   642
INCOMPATIBILITY.
66450
a8299195ed82 NEWS: Removed constant subseq; subsumed by strict_mono
eberlm <eberlm@in.tum.de>
parents: 66449
diff changeset
   643
66345
882abe912da9 do not fall back on nbe if plain evaluation fails
haftmann
parents: 66310
diff changeset
   644
* Command and antiquotation "value" with modified default strategy:
882abe912da9 do not fall back on nbe if plain evaluation fails
haftmann
parents: 66310
diff changeset
   645
terms without free variables are always evaluated using plain evaluation
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   646
only, with no fallback on normalization by evaluation. Minor
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   647
INCOMPATIBILITY.
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 65841
diff changeset
   648
65552
f533820e7248 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents: 65544
diff changeset
   649
* Theories "GCD" and "Binomial" are already included in "Main" (instead
65575
wenzelm
parents: 65572
diff changeset
   650
of "Complex_Main").
65552
f533820e7248 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents: 65544
diff changeset
   651
65170
53675f36820d restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents: 65099
diff changeset
   652
* Constant "surj" is a full input/output abbreviation (again).
53675f36820d restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents: 65099
diff changeset
   653
Minor INCOMPATIBILITY.
53675f36820d restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents: 65099
diff changeset
   654
64632
9df24b8b6c0a dropped aliasses
haftmann
parents: 64603
diff changeset
   655
* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
9df24b8b6c0a dropped aliasses
haftmann
parents: 64603
diff changeset
   656
INCOMPATIBILITY.
9df24b8b6c0a dropped aliasses
haftmann
parents: 64603
diff changeset
   657
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   658
* Renamed ii to imaginary_unit in order to free up ii as a variable
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   659
name. The syntax \<i> remains available. INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   660
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   661
* Dropped abbreviations transP, antisymP, single_valuedP; use constants
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   662
transp, antisymp, single_valuedp instead. INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   663
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   664
* Constant "subseq" in Topological_Spaces has been removed -- it is
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   665
subsumed by "strict_mono". Some basic lemmas specific to "subseq" have
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   666
been renamed accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   667
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   668
* Theory List: "sublist" renamed to "nths" in analogy with "nth", and
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   669
"sublisteq" renamed to "subseq". Minor INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   670
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   671
* Theory List: new generic function "sorted_wrt".
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   672
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   673
* Named theorems mod_simps covers various congruence rules concerning
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   674
mod, replacing former zmod_simps. INCOMPATIBILITY.
64787
067cacdd1117 tuned NEWS
haftmann
parents: 64786
diff changeset
   675
64593
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
   676
* Swapped orientation of congruence rules mod_add_left_eq,
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
   677
mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
   678
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   679
mod_diff_eq. INCOMPATIBILITY.
64593
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
   680
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
   681
* Generalized some facts:
64876
65a247444100 generalized types in lemmas
blanchet
parents: 64867
diff changeset
   682
    measure_induct_rule
65a247444100 generalized types in lemmas
blanchet
parents: 64867
diff changeset
   683
    measure_induct
64593
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
   684
    zminus_zmod ~> mod_minus_eq
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
   685
    zdiff_zmod_left ~> mod_diff_left_eq
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
   686
    zdiff_zmod_right ~> mod_diff_right_eq
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
   687
    zmod_eq_dvd_iff ~> mod_eq_dvd_iff
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
   688
INCOMPATIBILITY.
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64555
diff changeset
   689
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   690
* Algebraic type class hierarchy of euclidean (semi)rings in HOL:
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   691
euclidean_(semi)ring, euclidean_(semi)ring_cancel,
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   692
unique_euclidean_(semi)ring; instantiation requires provision of a
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   693
euclidean size.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   694
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   695
* Theory "HOL-Number_Theory.Euclidean_Algorithm" has been reworked:
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   696
  - Euclidean induction is available as rule eucl_induct.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   697
  - Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   698
    Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   699
    easy instantiation of euclidean (semi)rings as GCD (semi)rings.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   700
  - Coefficients obtained by extended euclidean algorithm are
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   701
    available as "bezout_coefficients".
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   702
INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   703
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   704
* Theory "Number_Theory.Totient" introduces basic notions about Euler's
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   705
totient function previously hidden as solitary example in theory
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   706
Residues. Definition changed so that "totient 1 = 1" in agreement with
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   707
the literature. Minor INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   708
66542
075bbb78d33c proper theory name;
wenzelm
parents: 66541
diff changeset
   709
* New styles in theory "HOL-Library.LaTeXsugar":
66541
nipkow
parents: 66488
diff changeset
   710
  - "dummy_pats" for printing equations with "_" on the lhs;
nipkow
parents: 66488
diff changeset
   711
  - "eta_expand" for printing eta-expanded terms.
nipkow
parents: 66488
diff changeset
   712
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   713
* Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   714
been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   715
66643
f7e38b8583a0 Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents: 66641
diff changeset
   716
* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F"
66488
9d83e8fe3de3 HOL-Library: going_to filter
Manuel Eberl <eberlm@in.tum.de>
parents: 66481
diff changeset
   717
filter for describing points x such that f(x) is in the filter F.
9d83e8fe3de3 HOL-Library: going_to filter
Manuel Eberl <eberlm@in.tum.de>
parents: 66481
diff changeset
   718
66480
4b8d1df8933b HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents: 66474
diff changeset
   719
* Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been
4b8d1df8933b HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents: 66474
diff changeset
   720
renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   721
space. INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   722
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   723
* Theory "HOL-Library.FinFun" has been moved to AFP (again).
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   724
INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   725
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   726
* Theory "HOL-Library.FuncSet": some old and rarely used ASCII
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   727
replacement syntax has been removed. INCOMPATIBILITY, standard syntax
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   728
with symbols should be used instead. The subsequent commands help to
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   729
reproduce the old forms, e.g. to simplify porting old theories:
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   730
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   731
syntax (ASCII)
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   732
  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   733
  "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   734
  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   735
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   736
* Theory "HOL-Library.Multiset": the simprocs on subsets operators of
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   737
multisets have been renamed:
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   738
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   739
  msetless_cancel_numerals ~> msetsubset_cancel
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   740
  msetle_cancel_numerals ~> msetsubset_eq_cancel
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   741
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   742
INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   743
66481
d35f7a9f92e2 output syntax for pattern aliases
Lars Hupel <lars.hupel@mytum.de>
parents: 66480
diff changeset
   744
* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax
d35f7a9f92e2 output syntax for pattern aliases
Lars Hupel <lars.hupel@mytum.de>
parents: 66480
diff changeset
   745
for pattern aliases as known from Haskell, Scala and ML.
65515
f595b7532dc9 removed Old_SMT legacy module
blanchet
parents: 65511
diff changeset
   746
66563
87b9eb69d5ba add type of unordered pairs
Andreas Lochbihler
parents: 66542
diff changeset
   747
* Theory "HOL-Library.Uprod" formalizes the type of unordered pairs.
87b9eb69d5ba add type of unordered pairs
Andreas Lochbihler
parents: 66542
diff changeset
   748
64898
49aa13b1b592 tuned whitespace;
wenzelm
parents: 64876
diff changeset
   749
* Session HOL-Analysis: more material involving arcs, paths, covering
66650
wenzelm
parents: 66643
diff changeset
   750
spaces, innessential maps, retracts, infinite products, simplicial
wenzelm
parents: 66643
diff changeset
   751
complexes. Baire Category theorem. Major results include the Jordan
wenzelm
parents: 66643
diff changeset
   752
Curve Theorem and the Great Picard Theorem.
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   753
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   754
* Session HOL-Algebra has been extended by additional lattice theory:
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   755
the Knaster-Tarski fixed point theorem and Galois Connections.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   756
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   757
* Sessions HOL-Computational_Algebra and HOL-Number_Theory: new notions
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   758
of squarefreeness, n-th powers, and prime powers.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   759
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   760
* Session "HOL-Computional_Algebra" covers many previously scattered
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   761
theories, notably Euclidean_Algorithm, Factorial_Ring,
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   762
Formal_Power_Series, Fraction_Field, Fundamental_Theorem_Algebra,
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   763
Normalized_Fraction, Polynomial_FPS, Polynomial, Primes. Minor
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   764
INCOMPATIBILITY.
65027
2b8583507891 renaming multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 64986
diff changeset
   765
60331
f215fd466e30 discontinued legacy;
wenzelm
parents: 60310
diff changeset
   766
64844
bb70dc05cd38 NEWS for VSCode;
wenzelm
parents: 64842
diff changeset
   767
*** System ***
bb70dc05cd38 NEWS for VSCode;
wenzelm
parents: 64842
diff changeset
   768
66474
wenzelm
parents: 66473
diff changeset
   769
* Isabelle/Scala: the SQL module supports access to relational
wenzelm
parents: 66473
diff changeset
   770
databases, either as plain file (SQLite) or full-scale server
wenzelm
parents: 66473
diff changeset
   771
(PostgreSQL via local port or remote ssh connection).
wenzelm
parents: 66473
diff changeset
   772
wenzelm
parents: 66473
diff changeset
   773
* Results of "isabelle build" are recorded as SQLite database (i.e.
wenzelm
parents: 66473
diff changeset
   774
"Application File Format" in the sense of
wenzelm
parents: 66473
diff changeset
   775
https://www.sqlite.org/appfileformat.html). This allows systematic
wenzelm
parents: 66473
diff changeset
   776
access via operations from module Sessions.Store in Isabelle/Scala.
wenzelm
parents: 66473
diff changeset
   777
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   778
* System option "parallel_proofs" is 1 by default (instead of more
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   779
aggressive 2). This requires less heap space and avoids burning parallel
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   780
CPU cycles, while full subproof parallelization is enabled for repeated
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   781
builds (according to parallel_subproofs_threshold).
65072
36c650d1a90d more detailed platform information;
wenzelm
parents: 65064
diff changeset
   782
65448
9bc3b57c1fa7 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents: 65417
diff changeset
   783
* System option "record_proofs" allows to change the global
9bc3b57c1fa7 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents: 65417
diff changeset
   784
Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;
9bc3b57c1fa7 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents: 65417
diff changeset
   785
a negative value means the current state in the ML heap image remains
9bc3b57c1fa7 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents: 65417
diff changeset
   786
unchanged.
9bc3b57c1fa7 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents: 65417
diff changeset
   787
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   788
* Isabelle settings variable ISABELLE_SCALA_BUILD_OPTIONS has been
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   789
renamed to ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY.
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   790
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   791
* Isabelle settings variables ISABELLE_WINDOWS_PLATFORM,
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   792
ISABELLE_WINDOWS_PLATFORM32, ISABELLE_WINDOWS_PLATFORM64 indicate the
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   793
native Windows platform (independently of the Cygwin installation). This
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   794
is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32,
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   795
ISABELLE_PLATFORM64.
65557
29c69a599743 clarified tool name -- more official status;
wenzelm
parents: 65552
diff changeset
   796
66786
61617dafcd60 more NEWS;
wenzelm
parents: 66671
diff changeset
   797
* Command-line tool "isabelle build_docker" builds a Docker image from
61617dafcd60 more NEWS;
wenzelm
parents: 66671
diff changeset
   798
the Isabelle application bundle for Linux. See also
61617dafcd60 more NEWS;
wenzelm
parents: 66671
diff changeset
   799
https://hub.docker.com/r/makarius/isabelle
61617dafcd60 more NEWS;
wenzelm
parents: 66671
diff changeset
   800
66473
wenzelm
parents: 66472
diff changeset
   801
* Command-line tool "isabelle vscode_server" provides a Language Server
wenzelm
parents: 66472
diff changeset
   802
Protocol implementation, e.g. for the Visual Studio Code editor. It
wenzelm
parents: 66472
diff changeset
   803
serves as example for alternative PIDE front-ends.
wenzelm
parents: 66472
diff changeset
   804
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   805
* Command-line tool "isabelle imports" helps to maintain theory imports
66671
41b64e53b6a1 more documentation;
wenzelm
parents: 66665
diff changeset
   806
wrt. session structure. Examples for the main Isabelle distribution:
66472
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   807
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   808
  isabelle imports -I -a
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   809
  isabelle imports -U -a
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   810
  isabelle imports -U -i -a
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   811
  isabelle imports -M -a -d '~~/src/Benchmarks'
1b7d66d62035 misc tuning and updates for release;
wenzelm
parents: 66462
diff changeset
   812
64844
bb70dc05cd38 NEWS for VSCode;
wenzelm
parents: 64842
diff changeset
   813
67099
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 67088
diff changeset
   814
64072
9f96e4da3064 updated for release;
wenzelm
parents: 64013
diff changeset
   815
New in Isabelle2016-1 (December 2016)
9f96e4da3064 updated for release;
wenzelm
parents: 64013
diff changeset
   816
-------------------------------------
62216
5fb86150a579 back to post-release mode -- after fork point;
wenzelm
parents: 62209
diff changeset
   817
62440
31fa592761da symbol interpretation for \<circle>;
wenzelm
parents: 62430
diff changeset
   818
*** General ***
31fa592761da symbol interpretation for \<circle>;
wenzelm
parents: 62430
diff changeset
   819
64390
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   820
* Splitter in proof methods "simp", "auto" and friends:
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   821
  - The syntax "split add" has been discontinued, use plain "split",
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   822
    INCOMPATIBILITY.
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   823
  - For situations with many conditional or case expressions, there is
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   824
    an alternative splitting strategy that can be much faster. It is
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   825
    selected by writing "split!" instead of "split". It applies safe
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   826
    introduction and elimination rules after each split rule. As a
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   827
    result the subgoal may be split into several subgoals.
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   828
63273
302daf918966 prefer hybrid 'bundle' command;
wenzelm
parents: 63272
diff changeset
   829
* Command 'bundle' provides a local theory target to define a bundle
302daf918966 prefer hybrid 'bundle' command;
wenzelm
parents: 63272
diff changeset
   830
from the body of specification commands (such as 'declare',
302daf918966 prefer hybrid 'bundle' command;
wenzelm
parents: 63272
diff changeset
   831
'declaration', 'notation', 'lemmas', 'lemma'). For example:
302daf918966 prefer hybrid 'bundle' command;
wenzelm
parents: 63272
diff changeset
   832
302daf918966 prefer hybrid 'bundle' command;
wenzelm
parents: 63272
diff changeset
   833
bundle foo
302daf918966 prefer hybrid 'bundle' command;
wenzelm
parents: 63272
diff changeset
   834
begin
302daf918966 prefer hybrid 'bundle' command;
wenzelm
parents: 63272
diff changeset
   835
  declare a [simp]
302daf918966 prefer hybrid 'bundle' command;
wenzelm
parents: 63272
diff changeset
   836
  declare b [intro]
302daf918966 prefer hybrid 'bundle' command;
wenzelm
parents: 63272
diff changeset
   837
end
63272
6d8a67a77bad documentation;
wenzelm
parents: 63260
diff changeset
   838
63282
7c509ddf29a5 added command 'unbundle';
wenzelm
parents: 63273
diff changeset
   839
* Command 'unbundle' is like 'include', but works within a local theory
7c509ddf29a5 added command 'unbundle';
wenzelm
parents: 63273
diff changeset
   840
context. Unlike "context includes ... begin", the effect of 'unbundle'
7c509ddf29a5 added command 'unbundle';
wenzelm
parents: 63273
diff changeset
   841
on the target context persists, until different declarations are given.
7c509ddf29a5 added command 'unbundle';
wenzelm
parents: 63273
diff changeset
   842
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   843
* Simplified outer syntax: uniform category "name" includes long
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   844
identifiers. Former "xname" / "nameref" / "name reference" has been
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   845
discontinued.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   846
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   847
* Embedded content (e.g. the inner syntax of types, terms, props) may be
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   848
delimited uniformly via cartouches. This works better than old-fashioned
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   849
quotes when sub-languages are nested.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   850
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   851
* Mixfix annotations support general block properties, with syntax
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   852
"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   853
"unbreakable", "markup". The existing notation "(DIGITS" is equivalent
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   854
to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   855
is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY.
63650
50cadecbe5bc "split add" -> "split".
nipkow
parents: 63635
diff changeset
   856
63383
wenzelm
parents: 63354
diff changeset
   857
* Proof method "blast" is more robust wrt. corner cases of Pure
wenzelm
parents: 63354
diff changeset
   858
statements without object-logic judgment.
wenzelm
parents: 63354
diff changeset
   859
63624
994d1a1105ef more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
wenzelm
parents: 63610
diff changeset
   860
* Commands 'prf' and 'full_prf' are somewhat more informative (again):
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   861
proof terms are reconstructed and cleaned from administrative thm nodes.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   862
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   863
* Code generator: config option "code_timing" triggers measurements of
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   864
different phases of code generation. See src/HOL/ex/Code_Timing.thy for
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   865
examples.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   866
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   867
* Code generator: implicits in Scala (stemming from type class
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   868
instances) are generated into companion object of corresponding type
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   869
class, to resolve some situations where ambiguities may occur.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   870
64390
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   871
* Solve direct: option "solve_direct_strict_warnings" gives explicit
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   872
warnings for lemma statements with trivial proofs.
64013
048b7dbfdfa3 option to report results of solve_direct as explicit warnings
haftmann
parents: 63995
diff changeset
   873
64602
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 64593
diff changeset
   874
62904
wenzelm
parents: 62886
diff changeset
   875
*** Prover IDE -- Isabelle/Scala/jEdit ***
wenzelm
parents: 62886
diff changeset
   876
64527
49708cffb98d NEWS for e6a3c55b929b;
wenzelm
parents: 64523
diff changeset
   877
* More aggressive flushing of machine-generated input, according to
49708cffb98d NEWS for e6a3c55b929b;
wenzelm
parents: 64523
diff changeset
   878
system option editor_generated_input_delay (in addition to existing
49708cffb98d NEWS for e6a3c55b929b;
wenzelm
parents: 64523
diff changeset
   879
editor_input_delay for regular user edits). This may affect overall PIDE
49708cffb98d NEWS for e6a3c55b929b;
wenzelm
parents: 64523
diff changeset
   880
reactivity and CPU usage.
49708cffb98d NEWS for e6a3c55b929b;
wenzelm
parents: 64523
diff changeset
   881
64390
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   882
* Syntactic indentation according to Isabelle outer syntax. Action
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   883
"indent-lines" (shortcut C+i) indents the current line according to
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   884
command keywords and some command substructure. Action
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   885
"isabelle.newline" (shortcut ENTER) indents the old and the new line
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   886
according to command keywords only; see also option
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   887
"jedit_indent_newline".
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   888
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   889
* Semantic indentation for unstructured proof scripts ('apply' etc.) via
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   890
number of subgoals. This requires information of ongoing document
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   891
processing and may thus lag behind, when the user is editing too
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   892
quickly; see also option "jedit_script_indent" and
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   893
"jedit_script_indent_limit".
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   894
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   895
* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   896
are treated as delimiters for fold structure; 'begin' and 'end'
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   897
structure of theory specifications is treated as well.
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   898
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   899
* Command 'proof' provides information about proof outline with cases,
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   900
e.g. for proof methods "cases", "induct", "goal_cases".
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   901
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   902
* Completion templates for commands involving "begin ... end" blocks,
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   903
e.g. 'context', 'notepad'.
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   904
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   905
* Sidekick parser "isabelle-context" shows nesting of context blocks
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   906
according to 'begin' and 'end' structure.
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   907
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   908
* Highlighting of entity def/ref positions wrt. cursor.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   909
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   910
* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
64514
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64457
diff changeset
   911
occurrences of the formal entity at the caret position. This facilitates
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   912
systematic renaming.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   913
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   914
* PIDE document markup works across multiple Isar commands, e.g. the
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   915
results established at the end of a proof are properly identified in the
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   916
theorem statement.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   917
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   918
* Cartouche abbreviations work both for " and ` to accomodate typical
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   919
situations where old ASCII notation may be updated.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   920
63875
wenzelm
parents: 63871
diff changeset
   921
* Dockable window "Symbols" also provides access to 'abbrevs' from the
wenzelm
parents: 63871
diff changeset
   922
outer syntax of the current theory buffer. This provides clickable
wenzelm
parents: 63871
diff changeset
   923
syntax templates, including entries with empty abbrevs name (which are
wenzelm
parents: 63871
diff changeset
   924
inaccessible via keyboard completion).
wenzelm
parents: 63871
diff changeset
   925
63022
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   926
* IDE support for the Isabelle/Pure bootstrap process, with the
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   927
following independent stages:
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   928
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   929
  src/Pure/ROOT0.ML
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   930
  src/Pure/ROOT.ML
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   931
  src/Pure/Pure.thy
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   932
  src/Pure/ML_Bootstrap.thy
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   933
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   934
The ML ROOT files act like quasi-theories in the context of theory
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   935
ML_Bootstrap: this allows continuous checking of all loaded ML files.
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   936
The theory files are presented with a modified header to import Pure
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   937
from the running Isabelle instance. Results from changed versions of
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   938
each stage are *not* propagated to the next stage, and isolated from the
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62994
diff changeset
   939
actual Isabelle/Pure that runs the IDE itself. The sequential
63307
wenzelm
parents: 63303
diff changeset
   940
dependencies of the above files are only observed for batch build.
62904
wenzelm
parents: 62886
diff changeset
   941
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   942
* Isabelle/ML and Standard ML files are presented in Sidekick with the
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   943
tree structure of section headings: this special comment format is
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   944
described in "implementation" chapter 0, e.g. (*** section ***).
63461
wenzelm
parents: 63455
diff changeset
   945
63581
wenzelm
parents: 63579
diff changeset
   946
* Additional abbreviations for syntactic completion may be specified
63871
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63855
diff changeset
   947
within the theory header as 'abbrevs'. The theory syntax for 'keywords'
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63855
diff changeset
   948
has been simplified accordingly: optional abbrevs need to go into the
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63855
diff changeset
   949
new 'abbrevs' section.
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63855
diff changeset
   950
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63855
diff changeset
   951
* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63855
diff changeset
   952
$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63855
diff changeset
   953
INCOMPATIBILITY, use 'abbrevs' within theory header instead.
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63560
diff changeset
   954
64390
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   955
* Action "isabelle.keymap-merge" asks the user to resolve pending
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   956
Isabelle keymap changes that are in conflict with the current jEdit
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   957
keymap; non-conflicting changes are always applied implicitly. This
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   958
action is automatically invoked on Isabelle/jEdit startup and thus
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   959
increases chances that users see new keyboard shortcuts when re-using
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   960
old keymaps.
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
   961
63675
e217525d6b64 uniform ML and document antiquotations;
wenzelm
parents: 63669
diff changeset
   962
* ML and document antiquotations for file-systems paths are more uniform
e217525d6b64 uniform ML and document antiquotations;
wenzelm
parents: 63669
diff changeset
   963
and diverse:
e217525d6b64 uniform ML and document antiquotations;
wenzelm
parents: 63669
diff changeset
   964
e217525d6b64 uniform ML and document antiquotations;
wenzelm
parents: 63669
diff changeset
   965
  @{path NAME}   -- no file-system check
e217525d6b64 uniform ML and document antiquotations;
wenzelm
parents: 63669
diff changeset
   966
  @{file NAME}   -- check for plain file
e217525d6b64 uniform ML and document antiquotations;
wenzelm
parents: 63669
diff changeset
   967
  @{dir NAME}    -- check for directory
e217525d6b64 uniform ML and document antiquotations;
wenzelm
parents: 63669
diff changeset
   968
e217525d6b64 uniform ML and document antiquotations;
wenzelm
parents: 63669
diff changeset
   969
Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may
e217525d6b64 uniform ML and document antiquotations;
wenzelm
parents: 63669
diff changeset
   970
have to be changed.
63669
256fc20716f2 clarified antiquotations;
wenzelm
parents: 63656
diff changeset
   971
256fc20716f2 clarified antiquotations;
wenzelm
parents: 63656
diff changeset
   972
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   973
*** Document preparation ***
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   974
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   975
* New symbol \<circle>, e.g. for temporal operator.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   976
64073
cffd5f537206 moved to proper release (cf. 4a72b37ac4b8);
wenzelm
parents: 64072
diff changeset
   977
* New document and ML antiquotation @{locale} for locales, similar to
cffd5f537206 moved to proper release (cf. 4a72b37ac4b8);
wenzelm
parents: 64072
diff changeset
   978
existing antiquotation @{class}.
cffd5f537206 moved to proper release (cf. 4a72b37ac4b8);
wenzelm
parents: 64072
diff changeset
   979
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   980
* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> --
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   981
this allows special forms of document output.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   982
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   983
* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   984
symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   985
derivatives.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   986
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   987
* \<^raw:...> symbols are no longer supported.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   988
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   989
* Old 'header' command is no longer supported (legacy since
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   990
Isabelle2015).
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   991
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
   992
62312
5e5a881ebc12 command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents: 62284
diff changeset
   993
*** Isar ***
5e5a881ebc12 command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents: 62284
diff changeset
   994
63180
ddfd021884b4 clarified check_open_spec / read_open_spec;
wenzelm
parents: 63178
diff changeset
   995
* Many specification elements support structured statements with 'if' /
ddfd021884b4 clarified check_open_spec / read_open_spec;
wenzelm
parents: 63178
diff changeset
   996
'for' eigen-context, e.g. 'axiomatization', 'abbreviation',
ddfd021884b4 clarified check_open_spec / read_open_spec;
wenzelm
parents: 63178
diff changeset
   997
'definition', 'inductive', 'function'.
ddfd021884b4 clarified check_open_spec / read_open_spec;
wenzelm
parents: 63178
diff changeset
   998
63094
056ea294c256 toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents: 63078
diff changeset
   999
* Toplevel theorem statements support eigen-context notation with 'if' /
63284
c20946f5b6fb spelling;
wenzelm
parents: 63283
diff changeset
  1000
'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the
63094
056ea294c256 toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents: 63078
diff changeset
  1001
traditional long statement form (in prefix). Local premises are called
056ea294c256 toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents: 63078
diff changeset
  1002
"that" or "assms", respectively. Empty premises are *not* bound in the
056ea294c256 toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents: 63078
diff changeset
  1003
context: INCOMPATIBILITY.
056ea294c256 toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents: 63078
diff changeset
  1004
63039
1a20fd9cf281 added Isar command 'define';
wenzelm
parents: 63032
diff changeset
  1005
* Command 'define' introduces a local (non-polymorphic) definition, with
1a20fd9cf281 added Isar command 'define';
wenzelm
parents: 63032
diff changeset
  1006
optional abstraction over local parameters. The syntax resembles
63043
df83a961d3a8 old 'def' is legacy;
wenzelm
parents: 63039
diff changeset
  1007
'definition' and 'obtain'. It fits better into the Isar language than
df83a961d3a8 old 'def' is legacy;
wenzelm
parents: 63039
diff changeset
  1008
old 'def', which is now a legacy feature.
63039
1a20fd9cf281 added Isar command 'define';
wenzelm
parents: 63032
diff changeset
  1009
63059
3f577308551e 'obtain' supports structured statements (similar to 'define');
wenzelm
parents: 63043
diff changeset
  1010
* Command 'obtain' supports structured statements with 'if' / 'for'
3f577308551e 'obtain' supports structured statements (similar to 'define');
wenzelm
parents: 63043
diff changeset
  1011
context.
3f577308551e 'obtain' supports structured statements (similar to 'define');
wenzelm
parents: 63043
diff changeset
  1012
62312
5e5a881ebc12 command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents: 62284
diff changeset
  1013
* Command '\<proof>' is an alias for 'sorry', with different
5e5a881ebc12 command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents: 62284
diff changeset
  1014
typesetting. E.g. to produce proof holes in examples and documentation.
62216
5fb86150a579 back to post-release mode -- after fork point;
wenzelm
parents: 62209
diff changeset
  1015
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1016
* The defining position of a literal fact \<open>prop\<close> is maintained more
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1017
carefully, and made accessible as hyperlink in the Prover IDE.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1018
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1019
* Commands 'finally' and 'ultimately' used to expose the result as
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1020
literal fact: this accidental behaviour has been discontinued. Rare
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1021
INCOMPATIBILITY, use more explicit means to refer to facts in Isar.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1022
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1023
* Command 'axiomatization' has become more restrictive to correspond
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1024
better to internal axioms as singleton facts with mandatory name. Minor
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1025
INCOMPATIBILITY.
62939
ef8d840f39fb removed old proof method "default";
wenzelm
parents: 62932
diff changeset
  1026
63259
wenzelm
parents: 63237
diff changeset
  1027
* Proof methods may refer to the main facts via the dynamic fact
wenzelm
parents: 63237
diff changeset
  1028
"method_facts". This is particularly useful for Eisbach method
wenzelm
parents: 63237
diff changeset
  1029
definitions.
wenzelm
parents: 63237
diff changeset
  1030
63527
59eff6e56d81 moved method "use" to Pure;
wenzelm
parents: 63513
diff changeset
  1031
* Proof method "use" allows to modify the main facts of a given method
59eff6e56d81 moved method "use" to Pure;
wenzelm
parents: 63513
diff changeset
  1032
expression, e.g.
63259
wenzelm
parents: 63237
diff changeset
  1033
wenzelm
parents: 63237
diff changeset
  1034
  (use facts in simp)
wenzelm
parents: 63237
diff changeset
  1035
  (use facts in \<open>simp add: ...\<close>)
wenzelm
parents: 63237
diff changeset
  1036
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1037
* The old proof method "default" has been removed (legacy since
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1038
Isabelle2016). INCOMPATIBILITY, use "standard" instead.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1039
62216
5fb86150a579 back to post-release mode -- after fork point;
wenzelm
parents: 62209
diff changeset
  1040
63165
c12845e8e80a examples and documentation for code generator time measurements
haftmann
parents: 63161
diff changeset
  1041
*** Pure ***
c12845e8e80a examples and documentation for code generator time measurements
haftmann
parents: 63161
diff changeset
  1042
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1043
* Pure provides basic versions of proof methods "simp" and "simp_all"
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1044
that only know about meta-equality (==). Potential INCOMPATIBILITY in
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1045
theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1046
is relevant to avoid confusion of Pure.simp vs. HOL.simp.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1047
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1048
* The command 'unfolding' and proof method "unfold" include a second
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1049
stage where given equations are passed through the attribute "abs_def"
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1050
before rewriting. This ensures that definitions are fully expanded,
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1051
regardless of the actual parameters that are provided. Rare
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1052
INCOMPATIBILITY in some corner cases: use proof method (simp only:)
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1053
instead, or declare [[unfold_abs_def = false]] in the proof context.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1054
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1055
* Type-inference improves sorts of newly introduced type variables for
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1056
the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1057
Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1058
produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1059
INCOMPATIBILITY, need to provide explicit type constraints for Pure
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1060
types where this is really intended.
63350
705229ed856e compiling implicit instances into companion objects for classes avoids ambiguities
haftmann
parents: 63343
diff changeset
  1061
63165
c12845e8e80a examples and documentation for code generator time measurements
haftmann
parents: 63161
diff changeset
  1062
62327
112eefe85ff0 document new 'primrec' feature
blanchet
parents: 62312
diff changeset
  1063
*** HOL ***
112eefe85ff0 document new 'primrec' feature
blanchet
parents: 62312
diff changeset
  1064
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1065
* New proof method "argo" using the built-in Argo solver based on SMT
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1066
technology. The method can be used to prove goals of quantifier-free
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1067
propositional logic, goals based on a combination of quantifier-free
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1068
propositional logic with equality, and goals based on a combination of
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1069
quantifier-free propositional logic with linear real arithmetic
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1070
including min/max/abs. See HOL/ex/Argo_Examples.thy for examples.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1071
66614
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents: 66599
diff changeset
  1072
* The new "nunchaku" command integrates the Nunchaku model finder. The
64390
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1073
tool is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details.
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1074
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1075
* Metis: The problem encoding has changed very slightly. This might
63785
c882ba741244 added warning
blanchet
parents: 63751
diff changeset
  1076
break existing proofs. INCOMPATIBILITY.
c882ba741244 added warning
blanchet
parents: 63751
diff changeset
  1077
63116
32492105b015 generate Vampire 4.0 compatible output
blanchet
parents: 63113
diff changeset
  1078
* Sledgehammer:
63967
2aa42596edc3 new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents: 63963
diff changeset
  1079
  - The MaSh relevance filter is now faster than before.
63116
32492105b015 generate Vampire 4.0 compatible output
blanchet
parents: 63113
diff changeset
  1080
  - Produce syntactically correct Vampire 4.0 problem files.
32492105b015 generate Vampire 4.0 compatible output
blanchet
parents: 63113
diff changeset
  1081
62327
112eefe85ff0 document new 'primrec' feature
blanchet
parents: 62312
diff changeset
  1082
* (Co)datatype package:
62693
0ae225877b68 document addition of 'corec'
blanchet
parents: 62678
diff changeset
  1083
  - New commands for defining corecursive functions and reasoning about
0ae225877b68 document addition of 'corec'
blanchet
parents: 62678
diff changeset
  1084
    them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
0ae225877b68 document addition of 'corec'
blanchet
parents: 62678
diff changeset
  1085
    'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof
62842
db9f95ca2a8f added reference from NEWS to docs
blanchet
parents: 62840
diff changeset
  1086
    method. See 'isabelle doc corec'.
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1087
  - The predicator :: ('a \<Rightarrow> bool) \<Rightarrow> 'a F \<Rightarrow> bool is now a first-class
63855
blanchet
parents: 63830
diff changeset
  1088
    citizen in bounded natural functors.
62693
0ae225877b68 document addition of 'corec'
blanchet
parents: 62678
diff changeset
  1089
  - 'primrec' now allows nested calls through the predicator in addition
62327
112eefe85ff0 document new 'primrec' feature
blanchet
parents: 62312
diff changeset
  1090
    to the map function.
63855
blanchet
parents: 63830
diff changeset
  1091
  - 'bnf' automatically discharges reflexive proof obligations.
62693
0ae225877b68 document addition of 'corec'
blanchet
parents: 62678
diff changeset
  1092
  - 'bnf' outputs a slightly modified proof obligation expressing rel in
62332
traytel
parents: 62327
diff changeset
  1093
       terms of map and set
63855
blanchet
parents: 63830
diff changeset
  1094
       (not giving a specification for rel makes this one reflexive).
62693
0ae225877b68 document addition of 'corec'
blanchet
parents: 62678
diff changeset
  1095
  - 'bnf' outputs a new proof obligation expressing pred in terms of set
63855
blanchet
parents: 63830
diff changeset
  1096
       (not giving a specification for pred makes this one reflexive).
blanchet
parents: 63830
diff changeset
  1097
    INCOMPATIBILITY: manual 'bnf' declarations may need adjustment.
62335
e85c42f4f30a making 'pred_inject' a first-class BNF citizen
blanchet
parents: 62332
diff changeset
  1098
  - Renamed lemmas:
e85c42f4f30a making 'pred_inject' a first-class BNF citizen
blanchet
parents: 62332
diff changeset
  1099
      rel_prod_apply ~> rel_prod_inject
e85c42f4f30a making 'pred_inject' a first-class BNF citizen
blanchet
parents: 62332
diff changeset
  1100
      pred_prod_apply ~> pred_prod_inject
e85c42f4f30a making 'pred_inject' a first-class BNF citizen
blanchet
parents: 62332
diff changeset
  1101
    INCOMPATIBILITY.
62536
656e9653c645 made 'size' plugin compatible with locales again (and added regression test)
blanchet
parents: 62525
diff changeset
  1102
  - The "size" plugin has been made compatible again with locales.
63855
blanchet
parents: 63830
diff changeset
  1103
  - The theorems about "rel" and "set" may have a slightly different (but
blanchet
parents: 63830
diff changeset
  1104
    equivalent) form.
blanchet
parents: 63830
diff changeset
  1105
    INCOMPATIBILITY.
62327
112eefe85ff0 document new 'primrec' feature
blanchet
parents: 62312
diff changeset
  1106
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1107
* The 'coinductive' command produces a proper coinduction rule for
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1108
mutual coinductive predicates. This new rule replaces the old rule,
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1109
which exposed details of the internal fixpoint construction and was
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1110
hard to use. INCOMPATIBILITY.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1111
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1112
* New abbreviations for negated existence (but not bounded existence):
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1113
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1114
  \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1115
  \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1116
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1117
* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1118
has been removed for output. It is retained for input only, until it is
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1119
eliminated altogether.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1120
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1121
* The unique existence quantifier no longer provides 'binder' syntax,
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1122
but uses syntax translations (as for bounded unique existence). Thus
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1123
iterated quantification \<exists>!x y. P x y with its slightly confusing
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1124
sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead,
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1125
pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1126
(analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1127
INCOMPATIBILITY in rare situations.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1128
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1129
* Conventional syntax "%(). t" for unit abstractions. Slight syntactic
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1130
INCOMPATIBILITY.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1131
64390
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1132
* Renamed constants and corresponding theorems:
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1133
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1134
    setsum ~> sum
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1135
    setprod ~> prod
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1136
    listsum ~> sum_list
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1137
    listprod ~> prod_list
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1138
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1139
INCOMPATIBILITY.
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1140
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1141
* Sligthly more standardized theorem names:
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1142
    sgn_times ~> sgn_mult
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1143
    sgn_mult' ~> Real_Vector_Spaces.sgn_mult
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1144
    divide_zero_left ~> div_0
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1145
    zero_mod_left ~> mod_0
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1146
    divide_zero ~> div_by_0
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1147
    divide_1 ~> div_by_1
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1148
    nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1149
    div_mult_self1_is_id ~> nonzero_mult_div_cancel_left
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1150
    nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1151
    div_mult_self2_is_id ~> nonzero_mult_div_cancel_right
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1152
    is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1153
    is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1154
    mod_div_equality ~> div_mult_mod_eq
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1155
    mod_div_equality2 ~> mult_div_mod_eq
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1156
    mod_div_equality3 ~> mod_div_mult_eq
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1157
    mod_div_equality4 ~> mod_mult_div_eq
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1158
    minus_div_eq_mod ~> minus_div_mult_eq_mod
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1159
    minus_div_eq_mod2 ~> minus_mult_div_eq_mod
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1160
    minus_mod_eq_div ~> minus_mod_eq_div_mult
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1161
    minus_mod_eq_div2 ~> minus_mod_eq_mult_div
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1162
    div_mod_equality' ~> minus_mod_eq_div_mult [symmetric]
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1163
    mod_div_equality' ~> minus_div_mult_eq_mod [symmetric]
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1164
    zmod_zdiv_equality ~> mult_div_mod_eq [symmetric]
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1165
    zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric]
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1166
    Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1167
    mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1168
    zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1169
    div_1 ~> div_by_Suc_0
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1170
    mod_1 ~> mod_by_Suc_0
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1171
INCOMPATIBILITY.
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1172
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1173
* New type class "idom_abs_sgn" specifies algebraic properties
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1174
of sign and absolute value functions.  Type class "sgn_if" has
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1175
disappeared.  Slight INCOMPATIBILITY.
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1176
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1177
* Dedicated syntax LENGTH('a) for length of types.
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1178
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1179
* Characters (type char) are modelled as finite algebraic type
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1180
corresponding to {0..255}.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1181
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1182
  - Logical representation:
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1183
    * 0 is instantiated to the ASCII zero character.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1184
    * All other characters are represented as "Char n"
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1185
      with n being a raw numeral expression less than 256.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1186
    * Expressions of the form "Char n" with n greater than 255
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1187
      are non-canonical.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1188
  - Printing and parsing:
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1189
    * Printable characters are printed and parsed as "CHR ''\<dots>''"
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1190
      (as before).
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1191
    * The ASCII zero character is printed and parsed as "0".
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1192
    * All other canonical characters are printed as "CHR 0xXX"
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1193
      with XX being the hexadecimal character code.  "CHR n"
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1194
      is parsable for every numeral expression n.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1195
    * Non-canonical characters have no special syntax and are
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1196
      printed as their logical representation.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1197
  - Explicit conversions from and to the natural numbers are
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1198
    provided as char_of_nat, nat_of_char (as before).
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1199
  - The auxiliary nibble type has been discontinued.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1200
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1201
INCOMPATIBILITY.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1202
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1203
* Type class "div" with operation "mod" renamed to type class "modulo"
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1204
with operation "modulo", analogously to type class "divide". This
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1205
eliminates the need to qualify any of those names in the presence of
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1206
infix "mod" syntax. INCOMPATIBILITY.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1207
63979
95c3ae4baba8 clarified lfp/gfp statements and proofs;
wenzelm
parents: 63977
diff changeset
  1208
* Statements and proofs of Knaster-Tarski fixpoint combinators lfp/gfp
95c3ae4baba8 clarified lfp/gfp statements and proofs;
wenzelm
parents: 63977
diff changeset
  1209
have been clarified. The fixpoint properties are lfp_fixpoint, its
95c3ae4baba8 clarified lfp/gfp statements and proofs;
wenzelm
parents: 63977
diff changeset
  1210
symmetric lfp_unfold (as before), and the duals for gfp. Auxiliary items
95c3ae4baba8 clarified lfp/gfp statements and proofs;
wenzelm
parents: 63977
diff changeset
  1211
for the proof (lfp_lemma2 etc.) are no longer exported, but can be
95c3ae4baba8 clarified lfp/gfp statements and proofs;
wenzelm
parents: 63977
diff changeset
  1212
easily recovered by composition with eq_refl. Minor INCOMPATIBILITY.
95c3ae4baba8 clarified lfp/gfp statements and proofs;
wenzelm
parents: 63977
diff changeset
  1213
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1214
* Constant "surj" is a mere input abbreviation, to avoid hiding an
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1215
equation in term output. Minor INCOMPATIBILITY.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1216
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1217
* Command 'code_reflect' accepts empty constructor lists for datatypes,
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1218
which renders those abstract effectively.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1219
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1220
* Command 'export_code' checks given constants for abstraction
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1221
violations: a small guarantee that given constants specify a safe
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1222
interface for the generated code.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1223
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1224
* Code generation for Scala: ambiguous implicts in class diagrams are
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1225
spelt out explicitly.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1226
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1227
* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1228
explicitly provided auxiliary definitions for required type class
64390
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1229
dictionaries rather than half-working magic. INCOMPATIBILITY, see the
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1230
tutorial on code generation for details.
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1231
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1232
* Theory Set_Interval: substantial new theorems on indexed sums and
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1233
products.
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1234
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1235
* Locale bijection establishes convenient default simp rules such as
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1236
"inv f (f a) = a" for total bijections.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1237
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1238
* Abstract locales semigroup, abel_semigroup, semilattice,
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1239
semilattice_neutr, ordering, ordering_top, semilattice_order,
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1240
semilattice_neutr_order, comm_monoid_set, semilattice_set,
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1241
semilattice_neutr_set, semilattice_order_set,
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1242
semilattice_order_neutr_set monoid_list, comm_monoid_list,
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1243
comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1244
syntax uniformly that does not clash with corresponding global syntax.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1245
INCOMPATIBILITY.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1246
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1247
* Former locale lifting_syntax is now a bundle, which is easier to
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1248
include in a local context or theorem statement, e.g. "context includes
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1249
lifting_syntax begin ... end". Minor INCOMPATIBILITY.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1250
63807
5f77017055a3 clarified obscure facts;
wenzelm
parents: 63795
diff changeset
  1251
* Some old / obsolete theorems have been renamed / removed, potential
5f77017055a3 clarified obscure facts;
wenzelm
parents: 63795
diff changeset
  1252
INCOMPATIBILITY.
5f77017055a3 clarified obscure facts;
wenzelm
parents: 63795
diff changeset
  1253
5f77017055a3 clarified obscure facts;
wenzelm
parents: 63795
diff changeset
  1254
  nat_less_cases  --  removed, use linorder_cases instead
5f77017055a3 clarified obscure facts;
wenzelm
parents: 63795
diff changeset
  1255
  inv_image_comp  --  removed, use image_inv_f_f instead
5f77017055a3 clarified obscure facts;
wenzelm
parents: 63795
diff changeset
  1256
  image_surj_f_inv_f  ~>  image_f_inv_f
63113
fe31996e3898 removed odd cases rule (see also 8cb42cd97579);
wenzelm
parents: 63094
diff changeset
  1257
63456
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1258
* Some theorems about groups and orders have been generalised from
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1259
  groups to semi-groups that are also monoids:
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1260
    le_add_same_cancel1
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1261
    le_add_same_cancel2
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1262
    less_add_same_cancel1
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1263
    less_add_same_cancel2
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1264
    add_le_same_cancel1
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1265
    add_le_same_cancel2
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1266
    add_less_same_cancel1
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1267
    add_less_same_cancel2
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1268
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1269
* Some simplifications theorems about rings have been removed, since
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1270
  superseeded by a more general version:
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1271
    less_add_cancel_left_greater_zero ~> less_add_same_cancel1
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1272
    less_add_cancel_right_greater_zero ~> less_add_same_cancel2
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1273
    less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1274
    less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1275
    less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1276
    less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1277
    less_add_cancel_left_less_zero ~> add_less_same_cancel1
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1278
    less_add_cancel_right_less_zero ~> add_less_same_cancel2
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1279
INCOMPATIBILITY.
3365c8ec67bd sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63455
diff changeset
  1280
62407
wenzelm
parents: 62396
diff changeset
  1281
* Renamed split_if -> if_split and split_if_asm -> if_split_asm to
wenzelm
parents: 62396
diff changeset
  1282
resemble the f.split naming convention, INCOMPATIBILITY.
62396
nipkow
parents: 62376
diff changeset
  1283
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1284
* Added class topological_monoid.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1285
64391
wenzelm
parents: 64390
diff changeset
  1286
* The following theorems have been renamed:
wenzelm
parents: 64390
diff changeset
  1287
64457
nipkow
parents: 64391
diff changeset
  1288
  setsum_left_distrib ~> sum_distrib_right
nipkow
parents: 64391
diff changeset
  1289
  setsum_right_distrib ~> sum_distrib_left
64391
wenzelm
parents: 64390
diff changeset
  1290
wenzelm
parents: 64390
diff changeset
  1291
INCOMPATIBILITY.
wenzelm
parents: 64390
diff changeset
  1292
wenzelm
parents: 64390
diff changeset
  1293
* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
wenzelm
parents: 64390
diff changeset
  1294
INCOMPATIBILITY.
wenzelm
parents: 64390
diff changeset
  1295
wenzelm
parents: 64390
diff changeset
  1296
* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional
wenzelm
parents: 64390
diff changeset
  1297
comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f `
wenzelm
parents: 64390
diff changeset
  1298
A)".
wenzelm
parents: 64390
diff changeset
  1299
wenzelm
parents: 64390
diff changeset
  1300
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY.
wenzelm
parents: 64390
diff changeset
  1301
wenzelm
parents: 64390
diff changeset
  1302
* The type class ordered_comm_monoid_add is now called
wenzelm
parents: 64390
diff changeset
  1303
ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add
wenzelm
parents: 64390
diff changeset
  1304
is introduced as the combination of ordered_ab_semigroup_add +
wenzelm
parents: 64390
diff changeset
  1305
comm_monoid_add. INCOMPATIBILITY.
wenzelm
parents: 64390
diff changeset
  1306
wenzelm
parents: 64390
diff changeset
  1307
* Introduced the type classes canonically_ordered_comm_monoid_add and
wenzelm
parents: 64390
diff changeset
  1308
dioid.
wenzelm
parents: 64390
diff changeset
  1309
wenzelm
parents: 64390
diff changeset
  1310
* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When
wenzelm
parents: 64390
diff changeset
  1311
instantiating linordered_semiring_strict and ordered_ab_group_add, an
wenzelm
parents: 64390
diff changeset
  1312
explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might
wenzelm
parents: 64390
diff changeset
  1313
be required. INCOMPATIBILITY.
63117
acb6d72fc42e renamed prefix* in Library/Sublist
nipkow
parents: 63113
diff changeset
  1314
62348
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1315
* Dropped various legacy fact bindings, whose replacements are often
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1316
of a more general type also:
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1317
  lcm_left_commute_nat ~> lcm.left_commute
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1318
  lcm_left_commute_int ~> lcm.left_commute
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1319
  gcd_left_commute_nat ~> gcd.left_commute
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1320
  gcd_left_commute_int ~> gcd.left_commute
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1321
  gcd_greatest_iff_nat ~> gcd_greatest_iff
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1322
  gcd_greatest_iff_int ~> gcd_greatest_iff
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1323
  coprime_dvd_mult_nat ~> coprime_dvd_mult
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1324
  coprime_dvd_mult_int ~> coprime_dvd_mult
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1325
  zpower_numeral_even ~> power_numeral_even
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1326
  gcd_mult_cancel_nat ~> gcd_mult_cancel
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1327
  gcd_mult_cancel_int ~> gcd_mult_cancel
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1328
  div_gcd_coprime_nat ~> div_gcd_coprime
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1329
  div_gcd_coprime_int ~> div_gcd_coprime
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1330
  zpower_numeral_odd ~> power_numeral_odd
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1331
  zero_less_int_conv ~> of_nat_0_less_iff
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1332
  gcd_greatest_nat ~> gcd_greatest
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1333
  gcd_greatest_int ~> gcd_greatest
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1334
  coprime_mult_nat ~> coprime_mult
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1335
  coprime_mult_int ~> coprime_mult
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1336
  lcm_commute_nat ~> lcm.commute
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1337
  lcm_commute_int ~> lcm.commute
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1338
  int_less_0_conv ~> of_nat_less_0_iff
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1339
  gcd_commute_nat ~> gcd.commute
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1340
  gcd_commute_int ~> gcd.commute
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1341
  Gcd_insert_nat ~> Gcd_insert
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1342
  Gcd_insert_int ~> Gcd_insert
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1343
  of_int_int_eq ~> of_int_of_nat_eq
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1344
  lcm_least_nat ~> lcm_least
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1345
  lcm_least_int ~> lcm_least
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1346
  lcm_assoc_nat ~> lcm.assoc
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1347
  lcm_assoc_int ~> lcm.assoc
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1348
  int_le_0_conv ~> of_nat_le_0_iff
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1349
  int_eq_0_conv ~> of_nat_eq_0_iff
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1350
  Gcd_empty_nat ~> Gcd_empty
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1351
  Gcd_empty_int ~> Gcd_empty
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1352
  gcd_assoc_nat ~> gcd.assoc
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1353
  gcd_assoc_int ~> gcd.assoc
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1354
  zero_zle_int ~> of_nat_0_le_iff
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1355
  lcm_dvd2_nat ~> dvd_lcm2
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1356
  lcm_dvd2_int ~> dvd_lcm2
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1357
  lcm_dvd1_nat ~> dvd_lcm1
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1358
  lcm_dvd1_int ~> dvd_lcm1
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1359
  gcd_zero_nat ~> gcd_eq_0_iff
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1360
  gcd_zero_int ~> gcd_eq_0_iff
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1361
  gcd_dvd2_nat ~> gcd_dvd2
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1362
  gcd_dvd2_int ~> gcd_dvd2
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1363
  gcd_dvd1_nat ~> gcd_dvd1
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1364
  gcd_dvd1_int ~> gcd_dvd1
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1365
  int_numeral ~> of_nat_numeral
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1366
  lcm_ac_nat ~> ac_simps
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1367
  lcm_ac_int ~> ac_simps
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1368
  gcd_ac_nat ~> ac_simps
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1369
  gcd_ac_int ~> ac_simps
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1370
  abs_int_eq ~> abs_of_nat
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1371
  zless_int ~> of_nat_less_iff
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1372
  zdiff_int ~> of_nat_diff
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1373
  zadd_int ~> of_nat_add
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1374
  int_mult ~> of_nat_mult
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1375
  int_Suc ~> of_nat_Suc
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1376
  inj_int ~> inj_of_nat
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1377
  int_1 ~> of_nat_1
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1378
  int_0 ~> of_nat_0
62353
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1379
  Lcm_empty_nat ~> Lcm_empty
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1380
  Lcm_empty_int ~> Lcm_empty
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1381
  Lcm_insert_nat ~> Lcm_insert
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1382
  Lcm_insert_int ~> Lcm_insert
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1383
  comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1384
  comp_fun_idem_gcd_int ~> comp_fun_idem_gcd
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1385
  comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1386
  comp_fun_idem_lcm_int ~> comp_fun_idem_lcm
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1387
  Lcm_eq_0 ~> Lcm_eq_0_I
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1388
  Lcm0_iff ~> Lcm_0_iff
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1389
  Lcm_dvd_int ~> Lcm_least
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1390
  divides_mult_nat ~> divides_mult
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1391
  divides_mult_int ~> divides_mult
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1392
  lcm_0_nat ~> lcm_0_right
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1393
  lcm_0_int ~> lcm_0_right
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1394
  lcm_0_left_nat ~> lcm_0_left
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1395
  lcm_0_left_int ~> lcm_0_left
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1396
  dvd_gcd_D1_nat ~> dvd_gcdD1
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1397
  dvd_gcd_D1_int ~> dvd_gcdD1
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1398
  dvd_gcd_D2_nat ~> dvd_gcdD2
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1399
  dvd_gcd_D2_int ~> dvd_gcdD2
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1400
  coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1401
  coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff
62348
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1402
  realpow_minus_mult ~> power_minus_mult
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
  1403
  realpow_Suc_le_self ~> power_Suc_le_self
62353
7f927120b5a2 dropped various legacy fact bindings and tuned proofs
haftmann
parents: 62352
diff changeset
  1404
  dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest
62347
2230b7047376 generalized some lemmas;
haftmann
parents: 62345
diff changeset
  1405
INCOMPATIBILITY.
2230b7047376 generalized some lemmas;
haftmann
parents: 62345
diff changeset
  1406
63967
2aa42596edc3 new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents: 63963
diff changeset
  1407
* Renamed HOL/Quotient_Examples/FSet.thy to
63977
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1408
HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY.
ec0fb01c6d50 misc tuning for release;
wenzelm
parents: 63967
diff changeset
  1409
64390
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1410
* Session HOL-Library: theory FinFun bundles "finfun_syntax" and
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1411
"no_finfun_syntax" allow to control optional syntax in local contexts;
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1412
this supersedes former theory FinFun_Syntax. INCOMPATIBILITY, e.g. use
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1413
"unbundle finfun_syntax" to imitate import of
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1414
"~~/src/HOL/Library/FinFun_Syntax".
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1415
ad2c5f37f659 misc tuning for release;
wenzelm
parents: 64389
diff changeset
  1416
* Session HOL-Library: theory Multiset_Permutations (executabl