NEWS
author wenzelm
Sun May 24 21:01:51 2020 +0200 (2 months ago)
changeset 71884 2bf0283fc975
parent 71845 b8d7b623e274
child 71901 0408f6814224
permissions -rw-r--r--
proper stack_limit;
     1 Isabelle NEWS -- history of user-relevant changes
     2 =================================================
     3 
     4 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
     5 
     6 
     7 New in this Isabelle version
     8 ----------------------------
     9 
    10 *** System ***
    11 
    12 * The command-line tool "isabelle console" now supports interrupts
    13 properly (on Linux and macOS).
    14 
    15 * The command-line tool "isabelle sessions" explores the structure of
    16 Isabelle sessions and prints result names in topological order (on
    17 stdout).
    18 
    19 * The Isabelle/Scala "Progress" interface changed slightly and
    20 "No_Progress" has been discontinued. INCOMPATIBILITY, use "new Progress"
    21 instead.
    22 
    23 * General support for Isabelle/Scala system services, configured via the
    24 shell function "isabelle_scala_service" in etc/settings (e.g. of an
    25 Isabelle component); see implementations of class
    26 Isabelle_System.Service in Isabelle/Scala. This supersedes former
    27 "isabelle_scala_tools" and "isabelle_file_format": minor
    28 INCOMPATIBILITY.
    29 
    30 * Isabelle/Phabricator setup has been updated to follow ongoing
    31 development: libphutil has been discontinued. Minor INCOMPATIBILITY:
    32 existing server installations should remove libphutil from
    33 /usr/local/bin/isabelle-phabricator-upgrade and each installation root
    34 directory (e.g. /var/www/phabricator-vcs/libphutil).
    35 
    36 
    37 *** Pure ***
    38 
    39 * Definitions in locales produce rule which can be added as congruence
    40 rule to protect foundational terms during simplification.
    41 
    42 *** HOL ***
    43 
    44 * New constant "power_int" for exponentiation with integer exponent,
    45 written as "x powi n".
    46 
    47 * Added the "at most 1" quantifier, Uniq.
    48 
    49 * For the natural numbers, Sup{} = 0.
    50 
    51 *** FOL ***
    52 
    53 * Added the "at most 1" quantifier, Uniq, as in HOL.
    54 
    55 New in Isabelle2020 (April 2020)
    56 --------------------------------
    57 
    58 *** General ***
    59 
    60 * Session ROOT files need to specify explicit 'directories' for import
    61 of theory files. Directories cannot be shared by different sessions.
    62 (Recall that import of theories from other sessions works via
    63 session-qualified theory names, together with suitable 'sessions'
    64 declarations in the ROOT.)
    65 
    66 * Internal derivations record dependencies on oracles and other theorems
    67 accurately, including the implicit type-class reasoning wrt. proven
    68 class relations and type arities. In particular, the formal tagging with
    69 "Pure.skip_proofs" of results stemming from "instance ... sorry" is now
    70 propagated properly to theorems depending on such type instances.
    71 
    72 * Command 'sorry' (oracle "Pure.skip_proofs") is more precise about the
    73 actual proposition that is assumed in the goal and proof context. This
    74 requires at least Proofterm.proofs = 1 to show up in theorem
    75 dependencies.
    76 
    77 * Command 'thm_oracles' prints all oracles used in given theorems,
    78 covering the full graph of transitive dependencies.
    79 
    80 * Command 'thm_deps' prints immediate theorem dependencies of the given
    81 facts. The former graph visualization has been discontinued, because it
    82 was hardly usable.
    83 
    84 * Refined treatment of proof terms, including type-class proofs for
    85 minor object-logics (FOL, FOLP, Sequents).
    86 
    87 * The inference kernel is now confined to one main module: structure
    88 Thm, without the former circular dependency on structure Axclass.
    89 
    90 * Mixfix annotations may use "' " (single quote followed by space) to
    91 separate delimiters (as documented in the isar-ref manual), without
    92 requiring an auxiliary empty block. A literal single quote needs to be
    93 escaped properly. Minor INCOMPATIBILITY.
    94 
    95 
    96 *** Isar ***
    97 
    98 * The proof method combinator (subproofs m) applies the method
    99 expression m consecutively to each subgoal, constructing individual
   100 subproofs internally. This impacts the internal construction of proof
   101 terms: it makes a cascade of let-expressions within the derivation tree
   102 and may thus improve scalability.
   103 
   104 * Attribute "trace_locales" activates tracing of locale instances during
   105 roundup. It replaces the diagnostic command 'print_dependencies', which
   106 has been discontinued.
   107 
   108 
   109 *** Isabelle/jEdit Prover IDE ***
   110 
   111 * Prover IDE startup is now much faster, because theory dependencies are
   112 no longer explored in advance. The overall session structure with its
   113 declarations of 'directories' is sufficient to locate theory files. Thus
   114 the "session focus" of option "isabelle jedit -S" has become obsolete
   115 (likewise for "isabelle vscode_server -S"). Existing option "-R" is both
   116 sufficient and more convenient to start editing a particular session.
   117 
   118 * Actions isabelle.tooltip (CS+b) and isabelle.message (CS+m) display
   119 tooltip message popups, corresponding to mouse hovering with/without the
   120 CONTROL/COMMAND key pressed.
   121 
   122 * The following actions allow to navigate errors within the current
   123 document snapshot:
   124 
   125   isabelle.first-error (CS+a)
   126   isabelle.last-error (CS+z)
   127   isabelle.next-error (CS+n)
   128   isabelle.prev-error (CS+p)
   129 
   130 * Support more brackets: \<llangle> \<rrangle> (intended for implicit argument syntax).
   131 
   132 * Action isabelle.jconsole (menu item Plugins / Isabelle / Java/VM
   133 Monitor) applies the jconsole tool on the running Isabelle/jEdit
   134 process. This allows to monitor resource usage etc.
   135 
   136 * More adequate default font sizes for Linux on HD / UHD displays:
   137 automatic font scaling is usually absent on Linux, in contrast to
   138 Windows and macOS.
   139 
   140 * The default value for the jEdit property "view.antiAlias" (menu item
   141 Utilities / Global Options / Text Area / Anti Aliased smooth text) is
   142 now "subpixel HRGB", instead of former "standard". Especially on Linux
   143 this often leads to faster text rendering, but can also cause problems
   144 with odd color shades. An alternative is to switch back to "standard"
   145 here, and set the following Java system property:
   146 
   147     isabelle jedit -Dsun.java2d.opengl=true
   148 
   149 This can be made persistent via JEDIT_JAVA_OPTIONS in
   150 $ISABELLE_HOME_USER/etc/settings. For the "Isabelle2020" desktop
   151 application there is a corresponding options file in the same directory.
   152 
   153 
   154 *** Isabelle/VSCode Prover IDE ***
   155 
   156 * Update of State and Preview panels to use new WebviewPanel API of
   157 VSCode.
   158 
   159 
   160 *** HOL ***
   161 
   162 * Improvements of the 'lift_bnf' command:
   163   - Add support for quotient types.
   164   - Generate transfer rules for the lifted map/set/rel/pred constants
   165     (theorems "<type>.<constant>_transfer_raw").
   166 
   167 * Term_XML.Encode/Decode.term uses compact representation of Const
   168 "typargs" from the given declaration environment. This also makes more
   169 sense for translations to lambda-calculi with explicit polymorphism.
   170 INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special
   171 applications.
   172 
   173 * ASCII membership syntax concerning big operators for infimum and
   174 supremum has been discontinued. INCOMPATIBILITY.
   175 
   176 * Removed multiplicativity assumption from class
   177 "normalization_semidom". Introduced various new intermediate classes
   178 with the multiplicativity assumption; many theorem statements
   179 (especially involving GCD/LCM) had to be adapted. This allows for a more
   180 natural instantiation of the algebraic typeclasses for e.g. Gaussian
   181 integers. INCOMPATIBILITY.
   182 
   183 * Clear distinction between types for bits (False / True) and Z2 (0 /
   184 1): theory HOL-Library.Bit has been renamed accordingly.
   185 INCOMPATIBILITY.
   186 
   187 * Dynamic facts "algebra_split_simps" and "field_split_simps" correspond
   188 to algebra_simps and field_simps but contain more aggressive rules
   189 potentially splitting goals; algebra_split_simps roughly replaces
   190 sign_simps and field_split_simps can be used instead of divide_simps.
   191 INCOMPATIBILITY.
   192 
   193 * Theory HOL.Complete_Lattices:
   194 renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf
   195 
   196 * Theory HOL-Library.Monad_Syntax: infix operation "bind" (\<bind>)
   197 associates to the left now as is customary.
   198 
   199 * Theory HOL-Library.Ramsey: full finite Ramsey's theorem with
   200 multiple colours and arbitrary exponents.
   201 
   202 * Session HOL-Proofs: build faster thanks to better treatment of proof
   203 terms in Isabelle/Pure.
   204 
   205 * Session HOL-Word: bitwise NOT-operator has proper prefix syntax. Minor
   206 INCOMPATIBILITY.
   207 
   208 * Session HOL-Analysis: proof method "metric" implements a decision
   209 procedure for simple linear statements in metric spaces.
   210 
   211 * Session HOL-Complex_Analysis has been split off from HOL-Analysis.
   212 
   213 
   214 *** ML ***
   215 
   216 * Theory construction may be forked internally, the operation
   217 Theory.join_theory recovers a single result theory. See also the example
   218 in theory "HOL-ex.Join_Theory".
   219 
   220 * Antiquotation @{oracle_name} inlines a formally checked oracle name.
   221 
   222 * Minimal support for a soft-type system within the Isabelle logical
   223 framework (module Soft_Type_System).
   224 
   225 * Former Variable.auto_fixes has been replaced by slightly more general
   226 Proof_Context.augment: it is subject to an optional soft-type system of
   227 the underlying object-logic. Minor INCOMPATIBILITY.
   228 
   229 * More scalable Export.export using XML.tree to avoid premature string
   230 allocations, with convenient shortcut XML.blob. Minor INCOMPATIBILITY.
   231 
   232 * Prover IDE support for the underlying Poly/ML compiler (not the basis
   233 library). Open $ML_SOURCES/ROOT.ML in Isabelle/jEdit to browse the
   234 implementation with full markup.
   235 
   236 
   237 *** System ***
   238 
   239 * Standard rendering for more Isabelle symbols: \<llangle> \<rrangle> \<bbar> \<sqdot>
   240 
   241 * The command-line tool "isabelle scala_project" creates a Gradle
   242 project configuration for Isabelle/Scala/jEdit, to support Scala IDEs
   243 such as IntelliJ IDEA.
   244 
   245 * The command-line tool "isabelle phabricator_setup" facilitates
   246 self-hosting of the Phabricator software-development platform, with
   247 support for Git, Mercurial, Subversion repositories. This helps to avoid
   248 monoculture and to escape the gravity of centralized version control by
   249 Github and/or Bitbucket. For further documentation, see chapter
   250 "Phabricator server administration" in the "system" manual. A notable
   251 example installation is https://isabelle-dev.sketis.net/.
   252 
   253 * The command-line tool "isabelle hg_setup" simplifies the setup of
   254 Mercurial repositories, with hosting via Phabricator or SSH file server
   255 access.
   256 
   257 * The command-line tool "isabelle imports" has been discontinued: strict
   258 checking of session directories enforces session-qualified theory names
   259 in applications -- users are responsible to specify session ROOT entries
   260 properly.
   261 
   262 * The command-line tool "isabelle dump" and its underlying
   263 Isabelle/Scala module isabelle.Dump has become more scalable, by
   264 splitting sessions and supporting a base logic image. Minor
   265 INCOMPATIBILITY in options and parameters.
   266 
   267 * The command-line tool "isabelle build_docker" has been slightly
   268 improved: it is now properly documented in the "system" manual.
   269 
   270 * Isabelle/Scala support for the Linux platform (Ubuntu): packages,
   271 users, system services.
   272 
   273 * Isabelle/Scala support for proof terms (with full type/term
   274 information) in module isabelle.Term.
   275 
   276 * Isabelle/Scala: more scalable output of YXML files, e.g. relevant for
   277 "isabelle dump".
   278 
   279 * Theory export via Isabelle/Scala has been reworked. The former "fact"
   280 name space is now split into individual "thm" items: names are
   281 potentially indexed, such as "foo" for singleton facts, or "bar(1)",
   282 "bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now
   283 exported as well: this spans an overall dependency graph of internal
   284 inferences; it might help to reconstruct the formal structure of theory
   285 libraries. See also the module isabelle.Export_Theory in Isabelle/Scala.
   286 
   287 * Theory export of structured specifications, based on internal
   288 declarations of Spec_Rules by packages like 'definition', 'inductive',
   289 'primrec', 'function'.
   290 
   291 * Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
   292 have been discontinued -- deprecated since Isabelle2018.
   293 
   294 * More complete x86_64 platform support on macOS, notably Catalina where
   295 old x86 has been discontinued.
   296 
   297 * Update to GHC stack 2.1.3 with stackage lts-13.19/ghc-8.6.4.
   298 
   299 * Update to OCaml Opam 2.0.6 (using ocaml 4.05.0 as before).
   300 
   301 
   302 
   303 New in Isabelle2019 (June 2019)
   304 -------------------------------
   305 
   306 *** General ***
   307 
   308 * The font collection "Isabelle DejaVu" is systematically derived from
   309 the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif"
   310 and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
   311 The DejaVu base fonts are retricted to well-defined Unicode ranges and
   312 augmented by special Isabelle symbols, taken from the former
   313 "IsabelleText" font (which is no longer provided separately). The line
   314 metrics and overall rendering quality is closer to original DejaVu.
   315 INCOMPATIBILITY with display configuration expecting the old
   316 "IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead.
   317 
   318 * The Isabelle fonts render "\<inverse>" properly as superscript "-1".
   319 
   320 * Old-style inner comments (* ... *) within the term language are no
   321 longer supported (legacy feature in Isabelle2018).
   322 
   323 * Old-style {* verbatim *} tokens are explicitly marked as legacy
   324 feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
   325 via "isabelle update_cartouches -t" (available since Isabelle2015).
   326 
   327 * Infix operators that begin or end with a "*" are now parenthesized
   328 without additional spaces, e.g. "(*)" instead of "( * )". Minor
   329 INCOMPATIBILITY.
   330 
   331 * Mixfix annotations may use cartouches instead of old-style double
   332 quotes, e.g. (infixl \<open>+\<close> 60). The command-line tool "isabelle update -u
   333 mixfix_cartouches" allows to update existing theory sources
   334 automatically.
   335 
   336 * ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation')
   337 need to provide a closed expression -- without trailing semicolon. Minor
   338 INCOMPATIBILITY.
   339 
   340 * Commands 'generate_file', 'export_generated_files', and
   341 'compile_generated_files' support a stateless (PIDE-conformant) model
   342 for generated sources and compiled binaries of other languages. The
   343 compilation process is managed in Isabelle/ML, and results exported to
   344 the session database for further use (e.g. with "isabelle export" or
   345 "isabelle build -e").
   346 
   347 
   348 *** Isabelle/jEdit Prover IDE ***
   349 
   350 * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
   351 DejaVu" collection by default, which provides uniform rendering quality
   352 with the usual Isabelle symbols. Line spacing no longer needs to be
   353 adjusted: properties for the old IsabelleText font had "Global Options /
   354 Text Area / Extra vertical line spacing (in pixels): -2", it now
   355 defaults to 1, but 0 works as well.
   356 
   357 * The jEdit File Browser is more prominent in the default GUI layout of
   358 Isabelle/jEdit: various virtual file-systems provide access to Isabelle
   359 resources, notably via "favorites:" (or "Edit Favorites").
   360 
   361 * Further markup and rendering for "plain text" (e.g. informal prose)
   362 and "raw text" (e.g. verbatim sources). This improves the visual
   363 appearance of formal comments inside the term language, or in general
   364 for repeated alternation of formal and informal text.
   365 
   366 * Action "isabelle-export-browser" points the File Browser to the theory
   367 exports of the current buffer, based on the "isabelle-export:" virtual
   368 file-system. The directory view needs to be reloaded manually to follow
   369 ongoing document processing.
   370 
   371 * Action "isabelle-session-browser" points the File Browser to session
   372 information, based on the "isabelle-session:" virtual file-system. Its
   373 entries are structured according to chapter / session names, the open
   374 operation is redirected to the session ROOT file.
   375 
   376 * Support for user-defined file-formats via class isabelle.File_Format
   377 in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via
   378 the shell function "isabelle_file_format" in etc/settings (e.g. of an
   379 Isabelle component).
   380 
   381 * System option "jedit_text_overview" allows to disable the text
   382 overview column.
   383 
   384 * Command-line options "-s" and "-u" of "isabelle jedit" override the
   385 default for system option "system_heaps" that determines the heap
   386 storage directory for "isabelle build". Option "-n" is now clearly
   387 separated from option "-s".
   388 
   389 * The Isabelle/jEdit desktop application uses the same options as
   390 "isabelle jedit" for its internal "isabelle build" process: the implicit
   391 option "-o system_heaps" (or "-s") has been discontinued. This reduces
   392 the potential for surprise wrt. command-line tools.
   393 
   394 * The official download of the Isabelle/jEdit application already
   395 contains heap images for Isabelle/HOL within its main directory: thus
   396 the first encounter becomes faster and more robust (e.g. when run from a
   397 read-only directory).
   398 
   399 * Isabelle DejaVu fonts are available with hinting by default, which is
   400 relevant for low-resolution displays. This may be disabled via system
   401 option "isabelle_fonts_hinted = false" in
   402 $ISABELLE_HOME_USER/etc/preferences -- it occasionally yields better
   403 results.
   404 
   405 * OpenJDK 11 has quite different font rendering, with better glyph
   406 shapes and improved sub-pixel anti-aliasing. In some situations results
   407 might be *worse* than Oracle Java 8, though -- a proper HiDPI / UHD
   408 display is recommended.
   409 
   410 * OpenJDK 11 supports GTK version 2.2 and 3 (according to system
   411 property jdk.gtk.version). The factory default is version 3, but
   412 ISABELLE_JAVA_SYSTEM_OPTIONS includes "-Djdk.gtk.version=2.2" to make
   413 this more conservative (as in Java 8). Depending on the GTK theme
   414 configuration, "-Djdk.gtk.version=3" might work better or worse.
   415 
   416 
   417 *** Document preparation ***
   418 
   419 * Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that
   420 are stripped from document output: the effect is to modify the semantic
   421 presentation context or to emit markup to the PIDE document. Some
   422 predefined markers are taken from the Dublin Core Metadata Initiative,
   423 e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that
   424 can be retrieved from the document database.
   425 
   426 * Old-style command tags %name are re-interpreted as markers with
   427 proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as
   428 before. Potential INCOMPATIBILITY: multiple markers are composed in
   429 canonical order, resulting in a reversed list of tags in the
   430 presentation context.
   431 
   432 * Marker \<^marker>\<open>tag name\<close> does not apply to the proof of a top-level goal
   433 statement by default (e.g. 'theorem', 'lemma'). This is a subtle change
   434 of semantics wrt. old-style %name.
   435 
   436 * In Isabelle/jEdit, the string "\tag" may be completed to a "\<^marker>\<open>tag \<close>"
   437 template.
   438 
   439 * Document antiquotation option "cartouche" indicates if the output
   440 should be delimited as cartouche; this takes precedence over the
   441 analogous option "quotes".
   442 
   443 * Many document antiquotations are internally categorized as "embedded"
   444 and expect one cartouche argument, which is typically used with the
   445 \<^control>\<open>cartouche\<close> notation (e.g. \<^term>\<open>\<lambda>x y. x\<close>). The cartouche
   446 delimiters are stripped in output of the source (antiquotation option
   447 "source"), but it is possible to enforce delimiters via option
   448 "source_cartouche", e.g. @{term [source_cartouche] \<open>\<lambda>x y. x\<close>}.
   449 
   450 
   451 *** Isar ***
   452 
   453 * Implicit cases goal1, goal2, goal3, etc. have been discontinued
   454 (legacy feature since Isabelle2016).
   455 
   456 * More robust treatment of structural errors: begin/end blocks take
   457 precedence over goal/proof. This is particularly relevant for the
   458 headless PIDE session and server.
   459 
   460 * Command keywords of kind thy_decl / thy_goal may be more specifically
   461 fit into the traditional document model of "definition-statement-proof"
   462 via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt.
   463 
   464 
   465 *** HOL ***
   466 
   467 * Simproc 'datatype_no_proper_subterm' rewrites equalities 'lhs = rhs'
   468 on datatypes to 'False' if either side is a proper subexpression of the
   469 other (for any datatype with a reasonable size function).
   470 
   471 * Command 'export_code' produces output as logical files within the
   472 theory context, as well as formal session exports that can be
   473 materialized via command-line tools "isabelle export" or "isabelle build
   474 -e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
   475 provides a virtual file-system "isabelle-export:" that can be explored
   476 in the regular file-browser. A 'file_prefix' argument allows to specify
   477 an explicit name prefix for the target file (SML, OCaml, Scala) or
   478 directory (Haskell); the default is "export" with a consecutive number
   479 within each theory.
   480 
   481 * Command 'export_code': the 'file' argument is now legacy and will be
   482 removed soon: writing to the physical file-system is not well-defined in
   483 a reactive/parallel application like Isabelle. The empty 'file' argument
   484 has been discontinued already: it is superseded by the file-browser in
   485 Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.
   486 
   487 * Command 'code_reflect' no longer supports the 'file' argument: it has
   488 been superseded by 'file_prefix' for stateless file management as in
   489 'export_code'. Minor INCOMPATIBILITY.
   490 
   491 * Code generation for OCaml: proper strings are used for literals.
   492 Minor INCOMPATIBILITY.
   493 
   494 * Code generation for OCaml: Zarith supersedes Nums as library for
   495 proper integer arithmetic. The library is located via standard
   496 invocations of "ocamlfind" (via ISABELLE_OCAMLFIND settings variable).
   497 The environment provided by "isabelle ocaml_setup" already contains this
   498 tool and the required packages. Minor INCOMPATIBILITY.
   499 
   500 * Code generation for Haskell: code includes for Haskell must contain
   501 proper module frame, nothing is added magically any longer.
   502 INCOMPATIBILITY.
   503 
   504 * Code generation: slightly more conventional syntax for 'code_stmts'
   505 antiquotation. Minor INCOMPATIBILITY.
   506 
   507 * Theory List: the precedence of the list_update operator has changed:
   508 "f a [n := x]" now needs to be written "(f a)[n := x]".
   509 
   510 * The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter> (not the corresponding binding operators)
   511 now have the same precedence as any other prefix function symbol. Minor
   512 INCOMPATIBILITY.
   513 
   514 * Simplified syntax setup for big operators under image. In rare
   515 situations, type conversions are not inserted implicitly any longer
   516 and need to be given explicitly. Auxiliary abbreviations INFIMUM,
   517 SUPREMUM, UNION, INTER should now rarely occur in output and are just
   518 retained as migration auxiliary. Abbreviations MINIMUM and MAXIMUM
   519 are gone INCOMPATIBILITY.
   520 
   521 * The simplifier uses image_cong_simp as a congruence rule. The historic
   522 and not really well-formed congruence rules INF_cong*, SUP_cong*, are
   523 not used by default any longer. INCOMPATIBILITY; consider using declare
   524 image_cong_simp [cong del] in extreme situations.
   525 
   526 * INF_image and SUP_image are no default simp rules any longer.
   527 INCOMPATIBILITY, prefer image_comp as simp rule if needed.
   528 
   529 * Strong congruence rules (with =simp=> in the premises) for constant f
   530 are now uniformly called f_cong_simp, in accordance with congruence
   531 rules produced for mappers by the datatype package. INCOMPATIBILITY.
   532 
   533 * Retired lemma card_Union_image; use the simpler card_UN_disjoint
   534 instead. INCOMPATIBILITY.
   535 
   536 * Facts sum_mset.commute and prod_mset.commute have been renamed to
   537 sum_mset.swap and prod_mset.swap, similarly to sum.swap and prod.swap.
   538 INCOMPATIBILITY.
   539 
   540 * ML structure Inductive: slightly more conventional naming schema.
   541 Minor INCOMPATIBILITY.
   542 
   543 * ML: Various _global variants of specification tools have been removed.
   544 Minor INCOMPATIBILITY, prefer combinators
   545 Named_Target.theory_map[_result] to lift specifications to the global
   546 theory level.
   547 
   548 * Theory HOL-Library.Simps_Case_Conv: 'case_of_simps' now supports
   549 overlapping and non-exhaustive patterns and handles arbitrarily nested
   550 patterns. It uses on the same algorithm as HOL-Library.Code_Lazy, which
   551 assumes sequential left-to-right pattern matching. The generated
   552 equation no longer tuples the arguments on the right-hand side.
   553 INCOMPATIBILITY.
   554 
   555 * Theory HOL-Library.Multiset: the \<Union># operator now has the same
   556 precedence as any other prefix function symbol.
   557 
   558 * Theory HOL-Library.Cardinal_Notations has been discontinued in favor
   559 of the bundle cardinal_syntax (available in theory Main). Minor
   560 INCOMPATIBILITY.
   561 
   562 * Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring,
   563 used for computing powers in class "monoid_mult" and modular
   564 exponentiation.
   565 
   566 * Session HOL-Computational_Algebra: Formal Laurent series and overhaul
   567 of Formal power series.
   568 
   569 * Session HOL-Number_Theory: More material on residue rings in
   570 Carmichael's function, primitive roots, more properties for "ord".
   571 
   572 * Session HOL-Analysis: Better organization and much more material
   573 at the level of abstract topological spaces.
   574 
   575 * Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
   576  algebraic closure of a field by de Vilhena and Baillon.
   577 
   578 * Session HOL-Homology has been added. It is a port of HOL Light's
   579 homology library, with new proofs of "invariance of domain" and related
   580 results.
   581 
   582 * Session HOL-SPARK: .prv files are no longer written to the
   583 file-system, but exported to the session database. Results may be
   584 retrieved via "isabelle build -e HOL-SPARK-Examples" on the
   585 command-line.
   586 
   587 * Sledgehammer:
   588   - The URL for SystemOnTPTP, which is used by remote provers, has been
   589     updated.
   590   - The machine-learning-based filter MaSh has been optimized to take
   591     less time (in most cases).
   592 
   593 * SMT: reconstruction is now possible using the SMT solver veriT.
   594 
   595 * Session HOL-Word:
   596   * New theory More_Word as comprehensive entrance point.
   597   * Merged type class bitss into type class bits.
   598   INCOMPATIBILITY.
   599 
   600 
   601 *** ML ***
   602 
   603 * Command 'generate_file' allows to produce sources for other languages,
   604 with antiquotations in the Isabelle context (only the control-cartouche
   605 form). The default "cartouche" antiquotation evaluates an ML expression
   606 of type string and inlines the result as a string literal of the target
   607 language. For example, this works for Haskell as follows:
   608 
   609   generate_file "Pure.hs" = \<open>
   610   module Isabelle.Pure where
   611     allConst, impConst, eqConst :: String
   612     allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
   613     impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
   614     eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
   615   \<close>
   616 
   617 See also commands 'export_generated_files' and 'compile_generated_files'
   618 to use the results.
   619 
   620 * ML evaluation (notably via command 'ML' or 'ML_file') is subject to
   621 option ML_environment to select a named environment, such as "Isabelle"
   622 for Isabelle/ML, or "SML" for official Standard ML.
   623 
   624 * ML antiquotation @{master_dir} refers to the master directory of the
   625 underlying theory, i.e. the directory of the theory file.
   626 
   627 * ML antiquotation @{verbatim} inlines its argument as string literal,
   628 preserving newlines literally. The short form \<^verbatim>\<open>abc\<close> is particularly
   629 useful.
   630 
   631 * Local_Theory.reset is no longer available in user space. Regular
   632 definitional packages should use balanced blocks of
   633 Local_Theory.open_target versus Local_Theory.close_target instead, or
   634 the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.
   635 
   636 * Original PolyML.pointerEq is retained as a convenience for tools that
   637 don't use Isabelle/ML (where this is called "pointer_eq").
   638 
   639 
   640 *** System ***
   641 
   642 * Update to OpenJDK 11: the current long-term support version of Java.
   643 
   644 * Update to Poly/ML 5.8 allows to use the native x86_64 platform without
   645 the full overhead of 64-bit values everywhere. This special x86_64_32
   646 mode provides up to 16GB ML heap, while program code and stacks are
   647 allocated elsewhere. Thus approx. 5 times more memory is available for
   648 applications compared to old x86 mode (which is no longer used by
   649 Isabelle). The switch to the x86_64 CPU architecture also avoids
   650 compatibility problems with Linux and macOS, where 32-bit applications
   651 are gradually phased out.
   652 
   653 * System option "checkpoint" has been discontinued: obsolete thanks to
   654 improved memory management in Poly/ML.
   655 
   656 * System option "system_heaps" determines where to store the session
   657 image of "isabelle build" (and other tools using that internally).
   658 Former option "-s" is superseded by option "-o system_heaps".
   659 INCOMPATIBILITY in command-line syntax.
   660 
   661 * Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
   662 source modules for Isabelle tools implemented in Haskell, notably for
   663 Isabelle/PIDE.
   664 
   665 * The command-line tool "isabelle build -e" retrieves theory exports
   666 from the session build database, using 'export_files' in session ROOT
   667 entries.
   668 
   669 * The command-line tool "isabelle update" uses Isabelle/PIDE in
   670 batch-mode to update theory sources based on semantic markup produced in
   671 Isabelle/ML. Actual updates depend on system options that may be enabled
   672 via "-u OPT" (for "update_OPT"), see also $ISABELLE_HOME/etc/options
   673 section "Theory update". Theory sessions are specified as in "isabelle
   674 dump".
   675 
   676 * The command-line tool "isabelle update -u control_cartouches" changes
   677 antiquotations into control-symbol format (where possible): @{NAME}
   678 becomes \<^NAME> and @{NAME ARG} becomes \<^NAME>\<open>ARG\<close>.
   679 
   680 * Support for Isabelle command-line tools defined in Isabelle/Scala.
   681 Instances of class Isabelle_Scala_Tools may be configured via the shell
   682 function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
   683 component).
   684 
   685 * Isabelle Server command "use_theories" supports "nodes_status_delay"
   686 for continuous output of node status information. The time interval is
   687 specified in seconds; a negative value means it is disabled (default).
   688 
   689 * Isabelle Server command "use_theories" terminates more robustly in the
   690 presence of structurally broken sources: full consolidation of theories
   691 is no longer required.
   692 
   693 * OCaml tools and libraries are now accesed via ISABELLE_OCAMLFIND,
   694 which needs to point to a suitable version of "ocamlfind" (e.g. via
   695 OPAM, see below). INCOMPATIBILITY: settings variables ISABELLE_OCAML and
   696 ISABELLE_OCAMLC are no longer supported.
   697 
   698 * Support for managed installations of Glasgow Haskell Compiler and
   699 OCaml via the following command-line tools:
   700 
   701   isabelle ghc_setup
   702   isabelle ghc_stack
   703 
   704   isabelle ocaml_setup
   705   isabelle ocaml_opam
   706 
   707 The global installation state is determined by the following settings
   708 (and corresponding directory contents):
   709 
   710   ISABELLE_STACK_ROOT
   711   ISABELLE_STACK_RESOLVER
   712   ISABELLE_GHC_VERSION
   713 
   714   ISABELLE_OPAM_ROOT
   715   ISABELLE_OCAML_VERSION
   716 
   717 After setup, the following Isabelle settings are automatically
   718 redirected (overriding existing user settings):
   719 
   720   ISABELLE_GHC
   721 
   722   ISABELLE_OCAMLFIND
   723 
   724 The old meaning of these settings as locally installed executables may
   725 be recovered by purging the directories ISABELLE_STACK_ROOT /
   726 ISABELLE_OPAM_ROOT, or by resetting these variables in
   727 $ISABELLE_HOME_USER/etc/settings.
   728 
   729 
   730 
   731 New in Isabelle2018 (August 2018)
   732 ---------------------------------
   733 
   734 *** General ***
   735 
   736 * Session-qualified theory names are mandatory: it is no longer possible
   737 to refer to unqualified theories from the parent session.
   738 INCOMPATIBILITY for old developments that have not been updated to
   739 Isabelle2017 yet (using the "isabelle imports" tool).
   740 
   741 * Only the most fundamental theory names are global, usually the entry
   742 points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
   743 FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
   744 formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
   745 
   746 * Global facts need to be closed: no free variables and no hypotheses.
   747 Rare INCOMPATIBILITY.
   748 
   749 * Facts stemming from locale interpretation are subject to lazy
   750 evaluation for improved performance. Rare INCOMPATIBILITY: errors
   751 stemming from interpretation morphisms might be deferred and thus
   752 difficult to locate; enable system option "strict_facts" temporarily to
   753 avoid this.
   754 
   755 * Marginal comments need to be written exclusively in the new-style form
   756 "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
   757 supported. INCOMPATIBILITY, use the command-line tool "isabelle
   758 update_comments" to update existing theory files.
   759 
   760 * Old-style inner comments (* ... *) within the term language are legacy
   761 and will be discontinued soon: use formal comments "\<comment> \<open>...\<close>" or "\<^cancel>\<open>...\<close>"
   762 instead.
   763 
   764 * The "op <infix-op>" syntax for infix operators has been replaced by
   765 "(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
   766 be a space between the "*" and the corresponding parenthesis.
   767 INCOMPATIBILITY, use the command-line tool "isabelle update_op" to
   768 convert theory and ML files to the new syntax. Because it is based on
   769 regular expression matching, the result may need a bit of manual
   770 postprocessing. Invoking "isabelle update_op" converts all files in the
   771 current directory (recursively). In case you want to exclude conversion
   772 of ML files (because the tool frequently also converts ML's "op"
   773 syntax), use option "-m".
   774 
   775 * Theory header 'abbrevs' specifications need to be separated by 'and'.
   776 INCOMPATIBILITY.
   777 
   778 * Command 'external_file' declares the formal dependency on the given
   779 file name, such that the Isabelle build process knows about it, but
   780 without specific Prover IDE management.
   781 
   782 * Session ROOT entries no longer allow specification of 'files'. Rare
   783 INCOMPATIBILITY, use command 'external_file' within a proper theory
   784 context.
   785 
   786 * Session root directories may be specified multiple times: each
   787 accessible ROOT file is processed only once. This facilitates
   788 specification of $ISABELLE_HOME_USER/ROOTS or command-line options like
   789 -d or -D for "isabelle build" and "isabelle jedit". Example:
   790 
   791   isabelle build -D '~~/src/ZF'
   792 
   793 * The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
   794 use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
   795 
   796 * In HTML output, the Isabelle symbol "\<hyphen>" is rendered as explicit
   797 Unicode hyphen U+2010, to avoid unclear meaning of the old "soft hyphen"
   798 U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML
   799 output.
   800 
   801 
   802 *** Isabelle/jEdit Prover IDE ***
   803 
   804 * The command-line tool "isabelle jedit" provides more flexible options
   805 for session management:
   806 
   807   - option -R builds an auxiliary logic image with all theories from
   808     other sessions that are not already present in its parent
   809 
   810   - option -S is like -R, with a focus on the selected session and its
   811     descendants (this reduces startup time for big projects like AFP)
   812 
   813   - option -A specifies an alternative ancestor session for options -R
   814     and -S
   815 
   816   - option -i includes additional sessions into the name-space of
   817     theories
   818 
   819   Examples:
   820     isabelle jedit -R HOL-Number_Theory
   821     isabelle jedit -R HOL-Number_Theory -A HOL
   822     isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
   823     isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
   824     isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL
   825 
   826 * PIDE markup for session ROOT files: allows to complete session names,
   827 follow links to theories and document files etc.
   828 
   829 * Completion supports theory header imports, using theory base name.
   830 E.g. "Prob" may be completed to "HOL-Probability.Probability".
   831 
   832 * Named control symbols (without special Unicode rendering) are shown as
   833 bold-italic keyword. This is particularly useful for the short form of
   834 antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
   835 "isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
   836 arguments into this format.
   837 
   838 * Completion provides templates for named symbols with arguments,
   839 e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
   840 
   841 * Slightly more parallel checking, notably for high priority print
   842 functions (e.g. State output).
   843 
   844 * The view title is set dynamically, according to the Isabelle
   845 distribution and the logic session name. The user can override this via
   846 set-view-title (stored persistently in $JEDIT_SETTINGS/perspective.xml).
   847 
   848 * System options "spell_checker_include" and "spell_checker_exclude"
   849 supersede former "spell_checker_elements" to determine regions of text
   850 that are subject to spell-checking. Minor INCOMPATIBILITY.
   851 
   852 * Action "isabelle.preview" is able to present more file formats,
   853 notably bibtex database files and ML files.
   854 
   855 * Action "isabelle.draft" is similar to "isabelle.preview", but shows a
   856 plain-text document draft. Both are available via the menu "Plugins /
   857 Isabelle".
   858 
   859 * When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
   860 is only used if there is no conflict with existing Unicode sequences in
   861 the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle
   862 symbols remain in literal \<symbol> form. This avoids accidental loss of
   863 Unicode content when saving the file.
   864 
   865 * Bibtex database files (.bib) are semantically checked.
   866 
   867 * Update to jedit-5.5.0, the latest release.
   868 
   869 
   870 *** Isabelle/VSCode Prover IDE ***
   871 
   872 * HTML preview of theories and other file-formats similar to
   873 Isabelle/jEdit.
   874 
   875 * Command-line tool "isabelle vscode_server" accepts the same options
   876 -A, -R, -S, -i for session selection as "isabelle jedit". This is
   877 relevant for isabelle.args configuration settings in VSCode. The former
   878 option -A (explore all known session files) has been discontinued: it is
   879 enabled by default, unless option -S is used to focus on a particular
   880 spot in the session structure. INCOMPATIBILITY.
   881 
   882 
   883 *** Document preparation ***
   884 
   885 * Formal comments work uniformly in outer syntax, inner syntax (term
   886 language), Isabelle/ML and some other embedded languages of Isabelle.
   887 See also "Document comments" in the isar-ref manual. The following forms
   888 are supported:
   889 
   890   - marginal text comment: \<comment> \<open>\<dots>\<close>
   891   - canceled source: \<^cancel>\<open>\<dots>\<close>
   892   - raw LaTeX: \<^latex>\<open>\<dots>\<close>
   893 
   894 * Outside of the inner theory body, the default presentation context is
   895 theory Pure. Thus elementary antiquotations may be used in markup
   896 commands (e.g. 'chapter', 'section', 'text') and formal comments.
   897 
   898 * System option "document_tags" specifies alternative command tags. This
   899 is occasionally useful to control the global visibility of commands via
   900 session options (e.g. in ROOT).
   901 
   902 * Document markup commands ('section', 'text' etc.) are implicitly
   903 tagged as "document" and visible by default. This avoids the application
   904 of option "document_tags" to these commands.
   905 
   906 * Isabelle names are mangled into LaTeX macro names to allow the full
   907 identifier syntax with underscore, prime, digits. This is relevant for
   908 antiquotations in control symbol notation, e.g. \<^const_name> becomes
   909 \isactrlconstUNDERSCOREname.
   910 
   911 * Document preparation with skip_proofs option now preserves the content
   912 more accurately: only terminal proof steps ('by' etc.) are skipped.
   913 
   914 * Document antiquotation @{theory name} requires the long
   915 session-qualified theory name: this is what users reading the text
   916 normally need to import.
   917 
   918 * Document antiquotation @{session name} checks and prints the given
   919 session name verbatim.
   920 
   921 * Document antiquotation @{cite} now checks the given Bibtex entries
   922 against the Bibtex database files -- only in batch-mode session builds.
   923 
   924 * Command-line tool "isabelle document" has been re-implemented in
   925 Isabelle/Scala, with simplified arguments and explicit errors from the
   926 latex and bibtex process. Minor INCOMPATIBILITY.
   927 
   928 * Session ROOT entry: empty 'document_files' means there is no document
   929 for this session. There is no need to specify options [document = false]
   930 anymore.
   931 
   932 
   933 *** Isar ***
   934 
   935 * Command 'interpret' no longer exposes resulting theorems as literal
   936 facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This
   937 improves modularity of proofs and scalability of locale interpretation.
   938 Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
   939 (e.g. use 'find_theorems' or 'try' to figure this out).
   940 
   941 * The old 'def' command has been discontinued (legacy since
   942 Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
   943 object-logic equality or equivalence.
   944 
   945 
   946 *** Pure ***
   947 
   948 * The inner syntax category "sort" now includes notation "_" for the
   949 dummy sort: it is effectively ignored in type-inference.
   950 
   951 * Rewrites clauses (keyword 'rewrites') were moved into the locale
   952 expression syntax, where they are part of locale instances. In
   953 interpretation commands rewrites clauses now need to occur before 'for'
   954 and 'defines'. Rare INCOMPATIBILITY; definitions immediately subject to
   955 rewriting may need to be pulled up into the surrounding theory.
   956 
   957 * For 'rewrites' clauses, if activating a locale instance fails, fall
   958 back to reading the clause first. This helps avoid qualification of
   959 locale instances where the qualifier's sole purpose is avoiding
   960 duplicate constant declarations.
   961 
   962 * Proof method "simp" now supports a new modifier "flip:" followed by a
   963 list of theorems. Each of these theorems is removed from the simpset
   964 (without warning if it is not there) and the symmetric version of the
   965 theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto"
   966 and friends the modifier is "simp flip:".
   967 
   968 
   969 *** HOL ***
   970 
   971 * Sledgehammer: bundled version of "vampire" (for non-commercial users)
   972 helps to avoid fragility of "remote_vampire" service.
   973 
   974 * Clarified relationship of characters, strings and code generation:
   975 
   976   - Type "char" is now a proper datatype of 8-bit values.
   977 
   978   - Conversions "nat_of_char" and "char_of_nat" are gone; use more
   979     general conversions "of_char" and "char_of" with suitable type
   980     constraints instead.
   981 
   982   - The zero character is just written "CHR 0x00", not "0" any longer.
   983 
   984   - Type "String.literal" (for code generation) is now isomorphic to
   985     lists of 7-bit (ASCII) values; concrete values can be written as
   986     "STR ''...''" for sequences of printable characters and "STR 0x..."
   987     for one single ASCII code point given as hexadecimal numeral.
   988 
   989   - Type "String.literal" supports concatenation "... + ..." for all
   990     standard target languages.
   991 
   992   - Theory HOL-Library.Code_Char is gone; study the explanations
   993     concerning "String.literal" in the tutorial on code generation to
   994     get an idea how target-language string literals can be converted to
   995     HOL string values and vice versa.
   996 
   997   - Session Imperative-HOL: operation "raise" directly takes a value of
   998     type "String.literal" as argument, not type "string".
   999 
  1000 INCOMPATIBILITY.
  1001 
  1002 * Code generation: Code generation takes an explicit option
  1003 "case_insensitive" to accomodate case-insensitive file systems.
  1004 
  1005 * Abstract bit operations as part of Main: push_bit, take_bit, drop_bit.
  1006 
  1007 * New, more general, axiomatization of complete_distrib_lattice. The
  1008 former axioms:
  1009 
  1010   "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
  1011 
  1012 are replaced by:
  1013 
  1014   "Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
  1015 
  1016 The instantiations of sets and functions as complete_distrib_lattice are
  1017 moved to Hilbert_Choice.thy because their proofs need the Hilbert choice
  1018 operator. The dual of this property is also proved in theory
  1019 HOL.Hilbert_Choice.
  1020 
  1021 * New syntax for the minimum/maximum of a function over a finite set:
  1022 MIN x\<in>A. B and even MIN x. B (only useful for finite types), also MAX.
  1023 
  1024 * Clarifed theorem names:
  1025 
  1026   Min.antimono ~> Min.subset_imp
  1027   Max.antimono ~> Max.subset_imp
  1028 
  1029 Minor INCOMPATIBILITY.
  1030 
  1031 * SMT module:
  1032 
  1033   - The 'smt_oracle' option is now necessary when using the 'smt' method
  1034     with a solver other than Z3. INCOMPATIBILITY.
  1035 
  1036   - The encoding to first-order logic is now more complete in the
  1037     presence of higher-order quantifiers. An 'smt_explicit_application'
  1038     option has been added to control this. INCOMPATIBILITY.
  1039 
  1040 * Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
  1041 sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
  1042 interpretation of abstract locales. INCOMPATIBILITY.
  1043 
  1044 * Predicate coprime is now a real definition, not a mere abbreviation.
  1045 INCOMPATIBILITY.
  1046 
  1047 * Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
  1048 INCOMPATIBILITY.
  1049 
  1050 * The relator rel_filter on filters has been strengthened to its
  1051 canonical categorical definition with better properties.
  1052 INCOMPATIBILITY.
  1053 
  1054 * Generalized linear algebra involving linear, span, dependent, dim
  1055 from type class real_vector to locales module and vector_space.
  1056 Renamed:
  1057 
  1058   span_inc ~> span_superset
  1059   span_superset ~> span_base
  1060   span_eq ~> span_eq_iff
  1061 
  1062 INCOMPATIBILITY.
  1063 
  1064 * Class linordered_semiring_1 covers zero_less_one also, ruling out
  1065 pathologic instances. Minor INCOMPATIBILITY.
  1066 
  1067 * Theory HOL.List: functions "sorted_wrt" and "sorted" now compare every
  1068 element in a list to all following elements, not just the next one.
  1069 
  1070 * Theory HOL.List syntax:
  1071 
  1072   - filter-syntax "[x <- xs. P]" is no longer output syntax, but only
  1073     input syntax
  1074 
  1075   - list comprehension syntax now supports tuple patterns in "pat <- xs"
  1076 
  1077 * Theory Map: "empty" must now be qualified as "Map.empty".
  1078 
  1079 * Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
  1080 
  1081 * Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
  1082 clash with fact mod_mult_self4 (on more generic semirings).
  1083 INCOMPATIBILITY.
  1084 
  1085 * Eliminated some theorem aliasses:
  1086   even_times_iff ~> even_mult_iff
  1087   mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1
  1088   even_of_nat ~> even_int_iff
  1089 
  1090 INCOMPATIBILITY.
  1091 
  1092 * Eliminated some theorem duplicate variations:
  1093 
  1094   - dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0
  1095   - mod_Suc_eq_Suc_mod can be replaced by mod_Suc
  1096   - mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps
  1097   - mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def
  1098   - the witness of mod_eqD can be given directly as "_ div _"
  1099 
  1100 INCOMPATIBILITY.
  1101 
  1102 * Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no
  1103 longer aggresively destroyed to "\<exists>q. m = d * q". INCOMPATIBILITY, adding
  1104 "elim!: dvd" to classical proof methods in most situations restores
  1105 broken proofs.
  1106 
  1107 * Theory HOL-Library.Conditional_Parametricity provides command
  1108 'parametric_constant' for proving parametricity of non-recursive
  1109 definitions. For constants that are not fully parametric the command
  1110 will infer conditions on relations (e.g., bi_unique, bi_total, or type
  1111 class conditions such as "respects 0") sufficient for parametricity. See
  1112 theory HOL-ex.Conditional_Parametricity_Examples for some examples.
  1113 
  1114 * Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
  1115 generator to generate code for algebraic types with lazy evaluation
  1116 semantics even in call-by-value target languages. See the theories
  1117 HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for some
  1118 examples.
  1119 
  1120 * Theory HOL-Library.Landau_Symbols has been moved here from AFP.
  1121 
  1122 * Theory HOL-Library.Old_Datatype no longer provides the legacy command
  1123 'old_datatype'. INCOMPATIBILITY.
  1124 
  1125 * Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
  1126 instances of rat, real, complex as factorial rings etc. Import
  1127 HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
  1128 INCOMPATIBILITY.
  1129 
  1130 * Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
  1131 infix/prefix notation.
  1132 
  1133 * Session HOL-Algebra: revamped with much new material. The set of
  1134 isomorphisms between two groups is now denoted iso rather than iso_set.
  1135 INCOMPATIBILITY.
  1136 
  1137 * Session HOL-Analysis: the Arg function now respects the same interval
  1138 as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi.
  1139 INCOMPATIBILITY.
  1140 
  1141 * Session HOL-Analysis: the functions zorder, zer_poly, porder and
  1142 pol_poly have been redefined. All related lemmas have been reworked.
  1143 INCOMPATIBILITY.
  1144 
  1145 * Session HOL-Analysis: infinite products, Moebius functions, the
  1146 Riemann mapping theorem, the Vitali covering theorem,
  1147 change-of-variables results for integration and measures.
  1148 
  1149 * Session HOL-Real_Asymp: proof method "real_asymp" proves asymptotics
  1150 or real-valued functions (limits, "Big-O", etc.) automatically.
  1151 See also ~~/src/HOL/Real_Asymp/Manual for some documentation.
  1152 
  1153 * Session HOL-Types_To_Sets: more tool support (unoverload_type combines
  1154 internalize_sorts and unoverload) and larger experimental application
  1155 (type based linear algebra transferred to linear algebra on subspaces).
  1156 
  1157 
  1158 *** ML ***
  1159 
  1160 * Operation Export.export emits theory exports (arbitrary blobs), which
  1161 are stored persistently in the session build database.
  1162 
  1163 * Command 'ML_export' exports ML toplevel bindings to the global
  1164 bootstrap environment of the ML process. This allows ML evaluation
  1165 without a formal theory context, e.g. in command-line tools like
  1166 "isabelle process".
  1167 
  1168 
  1169 *** System ***
  1170 
  1171 * Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no
  1172 longer supported.
  1173 
  1174 * Linux and Windows/Cygwin is for x86_64 only, old 32bit platform
  1175 support has been discontinued.
  1176 
  1177 * Java runtime is for x86_64 only. Corresponding Isabelle settings have
  1178 been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS,
  1179 instead of former 32/64 variants. INCOMPATIBILITY.
  1180 
  1181 * Old settings ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM should be
  1182 phased out due to unclear preference of 32bit vs. 64bit architecture.
  1183 Explicit GNU bash expressions are now preferred, for example (with
  1184 quotes):
  1185 
  1186   #Posix executables (Unix or Cygwin), with preference for 64bit
  1187   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
  1188 
  1189   #native Windows or Unix executables, with preference for 64bit
  1190   "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"
  1191 
  1192   #native Windows (32bit) or Unix executables (preference for 64bit)
  1193   "${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}"
  1194 
  1195 * Command-line tool "isabelle build" supports new options:
  1196   - option -B NAME: include session NAME and all descendants
  1197   - option -S: only observe changes of sources, not heap images
  1198   - option -f: forces a fresh build
  1199 
  1200 * Command-line tool "isabelle build" options -c -x -B refer to
  1201 descendants wrt. the session parent or import graph. Subtle
  1202 INCOMPATIBILITY: options -c -x used to refer to the session parent graph
  1203 only.
  1204 
  1205 * Command-line tool "isabelle build" takes "condition" options with the
  1206 corresponding environment values into account, when determining the
  1207 up-to-date status of a session.
  1208 
  1209 * The command-line tool "dump" dumps information from the cumulative
  1210 PIDE session database: many sessions may be loaded into a given logic
  1211 image, results from all loaded theories are written to the output
  1212 directory.
  1213 
  1214 * Command-line tool "isabelle imports -I" also reports actual session
  1215 imports. This helps to minimize the session dependency graph.
  1216 
  1217 * The command-line tool "export" and 'export_files' in session ROOT
  1218 entries retrieve theory exports from the session build database.
  1219 
  1220 * The command-line tools "isabelle server" and "isabelle client" provide
  1221 access to the Isabelle Server: it supports responsive session management
  1222 and concurrent use of theories, based on Isabelle/PIDE infrastructure.
  1223 See also the "system" manual.
  1224 
  1225 * The command-line tool "isabelle update_comments" normalizes formal
  1226 comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
  1227 approximate the appearance in document output). This is more specific
  1228 than former "isabelle update_cartouches -c": the latter tool option has
  1229 been discontinued.
  1230 
  1231 * The command-line tool "isabelle mkroot" now always produces a document
  1232 outline: its options have been adapted accordingly. INCOMPATIBILITY.
  1233 
  1234 * The command-line tool "isabelle mkroot -I" initializes a Mercurial
  1235 repository for the generated session files.
  1236 
  1237 * Settings ISABELLE_HEAPS + ISABELLE_BROWSER_INFO (or
  1238 ISABELLE_HEAPS_SYSTEM + ISABELLE_BROWSER_INFO_SYSTEM in "system build
  1239 mode") determine the directory locations of the main build artefacts --
  1240 instead of hard-wired directories in ISABELLE_HOME_USER (or
  1241 ISABELLE_HOME).
  1242 
  1243 * Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
  1244 heap images and session databases are always stored in
  1245 $ISABELLE_HEAPS/$ML_IDENTIFIER (command-line default) or
  1246 $ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER (main Isabelle application or
  1247 "isabelle jedit -s" or "isabelle build -s").
  1248 
  1249 * ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific
  1250 options for improved error reporting. Potential INCOMPATIBILITY with
  1251 unusual LaTeX installations, may have to adapt these settings.
  1252 
  1253 * Update to Poly/ML 5.7.1 with slightly improved performance and PIDE
  1254 markup for identifier bindings. It now uses The GNU Multiple Precision
  1255 Arithmetic Library (libgmp) on all platforms, notably Mac OS X with
  1256 32/64 bit.
  1257 
  1258 
  1259 
  1260 New in Isabelle2017 (October 2017)
  1261 ----------------------------------
  1262 
  1263 *** General ***
  1264 
  1265 * Experimental support for Visual Studio Code (VSCode) as alternative
  1266 Isabelle/PIDE front-end, see also
  1267 https://marketplace.visualstudio.com/items?itemName=makarius.Isabelle2017
  1268 
  1269 VSCode is a new type of application that continues the concepts of
  1270 "programmer's editor" and "integrated development environment" towards
  1271 fully semantic editing and debugging -- in a relatively light-weight
  1272 manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure.
  1273 Technically, VSCode is based on the Electron application framework
  1274 (Node.js + Chromium browser + V8), which is implemented in JavaScript
  1275 and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala
  1276 modules around a Language Server implementation.
  1277 
  1278 * Theory names are qualified by the session name that they belong to.
  1279 This affects imports, but not the theory name space prefix (which is
  1280 just the theory base name as before).
  1281 
  1282 In order to import theories from other sessions, the ROOT file format
  1283 provides a new 'sessions' keyword. In contrast, a theory that is
  1284 imported in the old-fashioned manner via an explicit file-system path
  1285 belongs to the current session, and might cause theory name conflicts
  1286 later on. Theories that are imported from other sessions are excluded
  1287 from the current session document. The command-line tool "isabelle
  1288 imports" helps to update theory imports.
  1289 
  1290 * The main theory entry points for some non-HOL sessions have changed,
  1291 to avoid confusion with the global name "Main" of the session HOL. This
  1292 leads to the follow renamings:
  1293 
  1294   CTT/Main.thy    ~>  CTT/CTT.thy
  1295   ZF/Main.thy     ~>  ZF/ZF.thy
  1296   ZF/Main_ZF.thy  ~>  ZF/ZF.thy
  1297   ZF/Main_ZFC.thy ~>  ZF/ZFC.thy
  1298   ZF/ZF.thy       ~>  ZF/ZF_Base.thy
  1299 
  1300 INCOMPATIBILITY.
  1301 
  1302 * Commands 'alias' and 'type_alias' introduce aliases for constants and
  1303 type constructors, respectively. This allows adhoc changes to name-space
  1304 accesses within global or local theory contexts, e.g. within a 'bundle'.
  1305 
  1306 * Document antiquotations @{prf} and @{full_prf} output proof terms
  1307 (again) in the same way as commands 'prf' and 'full_prf'.
  1308 
  1309 * Computations generated by the code generator can be embedded directly
  1310 into ML, alongside with @{code} antiquotations, using the following
  1311 antiquotations:
  1312 
  1313   @{computation ... terms: ... datatypes: ...} :
  1314     ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
  1315   @{computation_conv ... terms: ... datatypes: ...} :
  1316     (Proof.context -> 'ml -> conv) -> Proof.context -> conv
  1317   @{computation_check terms: ... datatypes: ...} : Proof.context -> conv
  1318 
  1319 See src/HOL/ex/Computations.thy,
  1320 src/HOL/Decision_Procs/Commutative_Ring.thy and
  1321 src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
  1322 tutorial on code generation.
  1323 
  1324 
  1325 *** Prover IDE -- Isabelle/Scala/jEdit ***
  1326 
  1327 * Session-qualified theory imports allow the Prover IDE to process
  1328 arbitrary theory hierarchies independently of the underlying logic
  1329 session image (e.g. option "isabelle jedit -l"), but the directory
  1330 structure needs to be known in advance (e.g. option "isabelle jedit -d"
  1331 or a line in the file $ISABELLE_HOME_USER/ROOTS).
  1332 
  1333 * The PIDE document model maintains file content independently of the
  1334 status of jEdit editor buffers. Reloading jEdit buffers no longer causes
  1335 changes of formal document content. Theory dependencies are always
  1336 resolved internally, without the need for corresponding editor buffers.
  1337 The system option "jedit_auto_load" has been discontinued: it is
  1338 effectively always enabled.
  1339 
  1340 * The Theories dockable provides a "Purge" button, in order to restrict
  1341 the document model to theories that are required for open editor
  1342 buffers.
  1343 
  1344 * The Theories dockable indicates the overall status of checking of each
  1345 entry. When all forked tasks of a theory are finished, the border is
  1346 painted with thick lines; remaining errors in this situation are
  1347 represented by a different border color.
  1348 
  1349 * Automatic indentation is more careful to avoid redundant spaces in
  1350 intermediate situations. Keywords are indented after input (via typed
  1351 characters or completion); see also option "jedit_indent_input".
  1352 
  1353 * Action "isabelle.preview" opens an HTML preview of the current theory
  1354 document in the default web browser.
  1355 
  1356 * Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
  1357 entry of the specified logic session in the editor, while its parent is
  1358 used for formal checking.
  1359 
  1360 * The main Isabelle/jEdit plugin may be restarted manually (using the
  1361 jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
  1362 enabled at all times.
  1363 
  1364 * Update to current jedit-5.4.0.
  1365 
  1366 
  1367 *** Pure ***
  1368 
  1369 * Deleting the last code equations for a particular function using
  1370 [code del] results in function with no equations (runtime abort) rather
  1371 than an unimplemented function (generation time abort). Use explicit
  1372 [[code drop:]] to enforce the latter. Minor INCOMPATIBILITY.
  1373 
  1374 * Proper concept of code declarations in code.ML:
  1375   - Regular code declarations act only on the global theory level, being
  1376     ignored with warnings if syntactically malformed.
  1377   - Explicitly global code declarations yield errors if syntactically
  1378     malformed.
  1379   - Default code declarations are silently ignored if syntactically
  1380     malformed.
  1381 Minor INCOMPATIBILITY.
  1382 
  1383 * Clarified and standardized internal data bookkeeping of code
  1384 declarations: history of serials allows to track potentially
  1385 non-monotonous declarations appropriately. Minor INCOMPATIBILITY.
  1386 
  1387 
  1388 *** HOL ***
  1389 
  1390 * The Nunchaku model finder is now part of "Main".
  1391 
  1392 * SMT module:
  1393   - A new option, 'smt_nat_as_int', has been added to translate 'nat' to
  1394     'int' and benefit from the SMT solver's theory reasoning. It is
  1395     disabled by default.
  1396   - The legacy module "src/HOL/Library/Old_SMT.thy" has been removed.
  1397   - Several small issues have been rectified in the 'smt' command.
  1398 
  1399 * (Co)datatype package: The 'size_gen_o_map' lemma is no longer
  1400 generated for datatypes with type class annotations. As a result, the
  1401 tactic that derives it no longer fails on nested datatypes. Slight
  1402 INCOMPATIBILITY.
  1403 
  1404 * Command and antiquotation "value" with modified default strategy:
  1405 terms without free variables are always evaluated using plain evaluation
  1406 only, with no fallback on normalization by evaluation. Minor
  1407 INCOMPATIBILITY.
  1408 
  1409 * Theories "GCD" and "Binomial" are already included in "Main" (instead
  1410 of "Complex_Main").
  1411 
  1412 * Constant "surj" is a full input/output abbreviation (again).
  1413 Minor INCOMPATIBILITY.
  1414 
  1415 * Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
  1416 INCOMPATIBILITY.
  1417 
  1418 * Renamed ii to imaginary_unit in order to free up ii as a variable
  1419 name. The syntax \<i> remains available. INCOMPATIBILITY.
  1420 
  1421 * Dropped abbreviations transP, antisymP, single_valuedP; use constants
  1422 transp, antisymp, single_valuedp instead. INCOMPATIBILITY.
  1423 
  1424 * Constant "subseq" in Topological_Spaces has been removed -- it is
  1425 subsumed by "strict_mono". Some basic lemmas specific to "subseq" have
  1426 been renamed accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.
  1427 
  1428 * Theory List: "sublist" renamed to "nths" in analogy with "nth", and
  1429 "sublisteq" renamed to "subseq". Minor INCOMPATIBILITY.
  1430 
  1431 * Theory List: new generic function "sorted_wrt".
  1432 
  1433 * Named theorems mod_simps covers various congruence rules concerning
  1434 mod, replacing former zmod_simps. INCOMPATIBILITY.
  1435 
  1436 * Swapped orientation of congruence rules mod_add_left_eq,
  1437 mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
  1438 mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
  1439 mod_diff_eq. INCOMPATIBILITY.
  1440 
  1441 * Generalized some facts:
  1442     measure_induct_rule
  1443     measure_induct
  1444     zminus_zmod ~> mod_minus_eq
  1445     zdiff_zmod_left ~> mod_diff_left_eq
  1446     zdiff_zmod_right ~> mod_diff_right_eq
  1447     zmod_eq_dvd_iff ~> mod_eq_dvd_iff
  1448 INCOMPATIBILITY.
  1449 
  1450 * Algebraic type class hierarchy of euclidean (semi)rings in HOL:
  1451 euclidean_(semi)ring, euclidean_(semi)ring_cancel,
  1452 unique_euclidean_(semi)ring; instantiation requires provision of a
  1453 euclidean size.
  1454 
  1455 * Theory "HOL-Number_Theory.Euclidean_Algorithm" has been reworked:
  1456   - Euclidean induction is available as rule eucl_induct.
  1457   - Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,
  1458     Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow
  1459     easy instantiation of euclidean (semi)rings as GCD (semi)rings.
  1460   - Coefficients obtained by extended euclidean algorithm are
  1461     available as "bezout_coefficients".
  1462 INCOMPATIBILITY.
  1463 
  1464 * Theory "Number_Theory.Totient" introduces basic notions about Euler's
  1465 totient function previously hidden as solitary example in theory
  1466 Residues. Definition changed so that "totient 1 = 1" in agreement with
  1467 the literature. Minor INCOMPATIBILITY.
  1468 
  1469 * New styles in theory "HOL-Library.LaTeXsugar":
  1470   - "dummy_pats" for printing equations with "_" on the lhs;
  1471   - "eta_expand" for printing eta-expanded terms.
  1472 
  1473 * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
  1474 been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
  1475 
  1476 * New theory "HOL-Library.Going_To_Filter" providing the "f going_to F"
  1477 filter for describing points x such that f(x) is in the filter F.
  1478 
  1479 * Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been
  1480 renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
  1481 space. INCOMPATIBILITY.
  1482 
  1483 * Theory "HOL-Library.FinFun" has been moved to AFP (again).
  1484 INCOMPATIBILITY.
  1485 
  1486 * Theory "HOL-Library.FuncSet": some old and rarely used ASCII
  1487 replacement syntax has been removed. INCOMPATIBILITY, standard syntax
  1488 with symbols should be used instead. The subsequent commands help to
  1489 reproduce the old forms, e.g. to simplify porting old theories:
  1490 
  1491 syntax (ASCII)
  1492   "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
  1493   "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
  1494   "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
  1495 
  1496 * Theory "HOL-Library.Multiset": the simprocs on subsets operators of
  1497 multisets have been renamed:
  1498 
  1499   msetless_cancel_numerals ~> msetsubset_cancel
  1500   msetle_cancel_numerals ~> msetsubset_eq_cancel
  1501 
  1502 INCOMPATIBILITY.
  1503 
  1504 * Theory "HOL-Library.Pattern_Aliases" provides input and output syntax
  1505 for pattern aliases as known from Haskell, Scala and ML.
  1506 
  1507 * Theory "HOL-Library.Uprod" formalizes the type of unordered pairs.
  1508 
  1509 * Session HOL-Analysis: more material involving arcs, paths, covering
  1510 spaces, innessential maps, retracts, infinite products, simplicial
  1511 complexes. Baire Category theorem. Major results include the Jordan
  1512 Curve Theorem and the Great Picard Theorem.
  1513 
  1514 * Session HOL-Algebra has been extended by additional lattice theory:
  1515 the Knaster-Tarski fixed point theorem and Galois Connections.
  1516 
  1517 * Sessions HOL-Computational_Algebra and HOL-Number_Theory: new notions
  1518 of squarefreeness, n-th powers, and prime powers.
  1519 
  1520 * Session "HOL-Computional_Algebra" covers many previously scattered
  1521 theories, notably Euclidean_Algorithm, Factorial_Ring,
  1522 Formal_Power_Series, Fraction_Field, Fundamental_Theorem_Algebra,
  1523 Normalized_Fraction, Polynomial_FPS, Polynomial, Primes. Minor
  1524 INCOMPATIBILITY.
  1525 
  1526 
  1527 *** System ***
  1528 
  1529 * Isabelle/Scala: the SQL module supports access to relational
  1530 databases, either as plain file (SQLite) or full-scale server
  1531 (PostgreSQL via local port or remote ssh connection).
  1532 
  1533 * Results of "isabelle build" are recorded as SQLite database (i.e.
  1534 "Application File Format" in the sense of
  1535 https://www.sqlite.org/appfileformat.html). This allows systematic
  1536 access via operations from module Sessions.Store in Isabelle/Scala.
  1537 
  1538 * System option "parallel_proofs" is 1 by default (instead of more
  1539 aggressive 2). This requires less heap space and avoids burning parallel
  1540 CPU cycles, while full subproof parallelization is enabled for repeated
  1541 builds (according to parallel_subproofs_threshold).
  1542 
  1543 * System option "record_proofs" allows to change the global
  1544 Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;
  1545 a negative value means the current state in the ML heap image remains
  1546 unchanged.
  1547 
  1548 * Isabelle settings variable ISABELLE_SCALA_BUILD_OPTIONS has been
  1549 renamed to ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY.
  1550 
  1551 * Isabelle settings variables ISABELLE_WINDOWS_PLATFORM,
  1552 ISABELLE_WINDOWS_PLATFORM32, ISABELLE_WINDOWS_PLATFORM64 indicate the
  1553 native Windows platform (independently of the Cygwin installation). This
  1554 is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32,
  1555 ISABELLE_PLATFORM64.
  1556 
  1557 * Command-line tool "isabelle build_docker" builds a Docker image from
  1558 the Isabelle application bundle for Linux. See also
  1559 https://hub.docker.com/r/makarius/isabelle
  1560 
  1561 * Command-line tool "isabelle vscode_server" provides a Language Server
  1562 Protocol implementation, e.g. for the Visual Studio Code editor. It
  1563 serves as example for alternative PIDE front-ends.
  1564 
  1565 * Command-line tool "isabelle imports" helps to maintain theory imports
  1566 wrt. session structure. Examples for the main Isabelle distribution:
  1567 
  1568   isabelle imports -I -a
  1569   isabelle imports -U -a
  1570   isabelle imports -U -i -a
  1571   isabelle imports -M -a -d '~~/src/Benchmarks'
  1572 
  1573 
  1574 
  1575 New in Isabelle2016-1 (December 2016)
  1576 -------------------------------------
  1577 
  1578 *** General ***
  1579 
  1580 * Splitter in proof methods "simp", "auto" and friends:
  1581   - The syntax "split add" has been discontinued, use plain "split",
  1582     INCOMPATIBILITY.
  1583   - For situations with many conditional or case expressions, there is
  1584     an alternative splitting strategy that can be much faster. It is
  1585     selected by writing "split!" instead of "split". It applies safe
  1586     introduction and elimination rules after each split rule. As a
  1587     result the subgoal may be split into several subgoals.
  1588 
  1589 * Command 'bundle' provides a local theory target to define a bundle
  1590 from the body of specification commands (such as 'declare',
  1591 'declaration', 'notation', 'lemmas', 'lemma'). For example:
  1592 
  1593 bundle foo
  1594 begin
  1595   declare a [simp]
  1596   declare b [intro]
  1597 end
  1598 
  1599 * Command 'unbundle' is like 'include', but works within a local theory
  1600 context. Unlike "context includes ... begin", the effect of 'unbundle'
  1601 on the target context persists, until different declarations are given.
  1602 
  1603 * Simplified outer syntax: uniform category "name" includes long
  1604 identifiers. Former "xname" / "nameref" / "name reference" has been
  1605 discontinued.
  1606 
  1607 * Embedded content (e.g. the inner syntax of types, terms, props) may be
  1608 delimited uniformly via cartouches. This works better than old-fashioned
  1609 quotes when sub-languages are nested.
  1610 
  1611 * Mixfix annotations support general block properties, with syntax
  1612 "(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
  1613 "unbreakable", "markup". The existing notation "(DIGITS" is equivalent
  1614 to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks
  1615 is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY.
  1616 
  1617 * Proof method "blast" is more robust wrt. corner cases of Pure
  1618 statements without object-logic judgment.
  1619 
  1620 * Commands 'prf' and 'full_prf' are somewhat more informative (again):
  1621 proof terms are reconstructed and cleaned from administrative thm nodes.
  1622 
  1623 * Code generator: config option "code_timing" triggers measurements of
  1624 different phases of code generation. See src/HOL/ex/Code_Timing.thy for
  1625 examples.
  1626 
  1627 * Code generator: implicits in Scala (stemming from type class
  1628 instances) are generated into companion object of corresponding type
  1629 class, to resolve some situations where ambiguities may occur.
  1630 
  1631 * Solve direct: option "solve_direct_strict_warnings" gives explicit
  1632 warnings for lemma statements with trivial proofs.
  1633 
  1634 
  1635 *** Prover IDE -- Isabelle/Scala/jEdit ***
  1636 
  1637 * More aggressive flushing of machine-generated input, according to
  1638 system option editor_generated_input_delay (in addition to existing
  1639 editor_input_delay for regular user edits). This may affect overall PIDE
  1640 reactivity and CPU usage.
  1641 
  1642 * Syntactic indentation according to Isabelle outer syntax. Action
  1643 "indent-lines" (shortcut C+i) indents the current line according to
  1644 command keywords and some command substructure. Action
  1645 "isabelle.newline" (shortcut ENTER) indents the old and the new line
  1646 according to command keywords only; see also option
  1647 "jedit_indent_newline".
  1648 
  1649 * Semantic indentation for unstructured proof scripts ('apply' etc.) via
  1650 number of subgoals. This requires information of ongoing document
  1651 processing and may thus lag behind, when the user is editing too
  1652 quickly; see also option "jedit_script_indent" and
  1653 "jedit_script_indent_limit".
  1654 
  1655 * Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
  1656 are treated as delimiters for fold structure; 'begin' and 'end'
  1657 structure of theory specifications is treated as well.
  1658 
  1659 * Command 'proof' provides information about proof outline with cases,
  1660 e.g. for proof methods "cases", "induct", "goal_cases".
  1661 
  1662 * Completion templates for commands involving "begin ... end" blocks,
  1663 e.g. 'context', 'notepad'.
  1664 
  1665 * Sidekick parser "isabelle-context" shows nesting of context blocks
  1666 according to 'begin' and 'end' structure.
  1667 
  1668 * Highlighting of entity def/ref positions wrt. cursor.
  1669 
  1670 * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
  1671 occurrences of the formal entity at the caret position. This facilitates
  1672 systematic renaming.
  1673 
  1674 * PIDE document markup works across multiple Isar commands, e.g. the
  1675 results established at the end of a proof are properly identified in the
  1676 theorem statement.
  1677 
  1678 * Cartouche abbreviations work both for " and ` to accomodate typical
  1679 situations where old ASCII notation may be updated.
  1680 
  1681 * Dockable window "Symbols" also provides access to 'abbrevs' from the
  1682 outer syntax of the current theory buffer. This provides clickable
  1683 syntax templates, including entries with empty abbrevs name (which are
  1684 inaccessible via keyboard completion).
  1685 
  1686 * IDE support for the Isabelle/Pure bootstrap process, with the
  1687 following independent stages:
  1688 
  1689   src/Pure/ROOT0.ML
  1690   src/Pure/ROOT.ML
  1691   src/Pure/Pure.thy
  1692   src/Pure/ML_Bootstrap.thy
  1693 
  1694 The ML ROOT files act like quasi-theories in the context of theory
  1695 ML_Bootstrap: this allows continuous checking of all loaded ML files.
  1696 The theory files are presented with a modified header to import Pure
  1697 from the running Isabelle instance. Results from changed versions of
  1698 each stage are *not* propagated to the next stage, and isolated from the
  1699 actual Isabelle/Pure that runs the IDE itself. The sequential
  1700 dependencies of the above files are only observed for batch build.
  1701 
  1702 * Isabelle/ML and Standard ML files are presented in Sidekick with the
  1703 tree structure of section headings: this special comment format is
  1704 described in "implementation" chapter 0, e.g. (*** section ***).
  1705 
  1706 * Additional abbreviations for syntactic completion may be specified
  1707 within the theory header as 'abbrevs'. The theory syntax for 'keywords'
  1708 has been simplified accordingly: optional abbrevs need to go into the
  1709 new 'abbrevs' section.
  1710 
  1711 * Global abbreviations via $ISABELLE_HOME/etc/abbrevs and
  1712 $ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor
  1713 INCOMPATIBILITY, use 'abbrevs' within theory header instead.
  1714 
  1715 * Action "isabelle.keymap-merge" asks the user to resolve pending
  1716 Isabelle keymap changes that are in conflict with the current jEdit
  1717 keymap; non-conflicting changes are always applied implicitly. This
  1718 action is automatically invoked on Isabelle/jEdit startup and thus
  1719 increases chances that users see new keyboard shortcuts when re-using
  1720 old keymaps.
  1721 
  1722 * ML and document antiquotations for file-systems paths are more uniform
  1723 and diverse:
  1724 
  1725   @{path NAME}   -- no file-system check
  1726   @{file NAME}   -- check for plain file
  1727   @{dir NAME}    -- check for directory
  1728 
  1729 Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may
  1730 have to be changed.
  1731 
  1732 
  1733 *** Document preparation ***
  1734 
  1735 * New symbol \<circle>, e.g. for temporal operator.
  1736 
  1737 * New document and ML antiquotation @{locale} for locales, similar to
  1738 existing antiquotation @{class}.
  1739 
  1740 * Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> --
  1741 this allows special forms of document output.
  1742 
  1743 * Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control
  1744 symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its
  1745 derivatives.
  1746 
  1747 * \<^raw:...> symbols are no longer supported.
  1748 
  1749 * Old 'header' command is no longer supported (legacy since
  1750 Isabelle2015).
  1751 
  1752 
  1753 *** Isar ***
  1754 
  1755 * Many specification elements support structured statements with 'if' /
  1756 'for' eigen-context, e.g. 'axiomatization', 'abbreviation',
  1757 'definition', 'inductive', 'function'.
  1758 
  1759 * Toplevel theorem statements support eigen-context notation with 'if' /
  1760 'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the
  1761 traditional long statement form (in prefix). Local premises are called
  1762 "that" or "assms", respectively. Empty premises are *not* bound in the
  1763 context: INCOMPATIBILITY.
  1764 
  1765 * Command 'define' introduces a local (non-polymorphic) definition, with
  1766 optional abstraction over local parameters. The syntax resembles
  1767 'definition' and 'obtain'. It fits better into the Isar language than
  1768 old 'def', which is now a legacy feature.
  1769 
  1770 * Command 'obtain' supports structured statements with 'if' / 'for'
  1771 context.
  1772 
  1773 * Command '\<proof>' is an alias for 'sorry', with different
  1774 typesetting. E.g. to produce proof holes in examples and documentation.
  1775 
  1776 * The defining position of a literal fact \<open>prop\<close> is maintained more
  1777 carefully, and made accessible as hyperlink in the Prover IDE.
  1778 
  1779 * Commands 'finally' and 'ultimately' used to expose the result as
  1780 literal fact: this accidental behaviour has been discontinued. Rare
  1781 INCOMPATIBILITY, use more explicit means to refer to facts in Isar.
  1782 
  1783 * Command 'axiomatization' has become more restrictive to correspond
  1784 better to internal axioms as singleton facts with mandatory name. Minor
  1785 INCOMPATIBILITY.
  1786 
  1787 * Proof methods may refer to the main facts via the dynamic fact
  1788 "method_facts". This is particularly useful for Eisbach method
  1789 definitions.
  1790 
  1791 * Proof method "use" allows to modify the main facts of a given method
  1792 expression, e.g.
  1793 
  1794   (use facts in simp)
  1795   (use facts in \<open>simp add: ...\<close>)
  1796 
  1797 * The old proof method "default" has been removed (legacy since
  1798 Isabelle2016). INCOMPATIBILITY, use "standard" instead.
  1799 
  1800 
  1801 *** Pure ***
  1802 
  1803 * Pure provides basic versions of proof methods "simp" and "simp_all"
  1804 that only know about meta-equality (==). Potential INCOMPATIBILITY in
  1805 theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
  1806 is relevant to avoid confusion of Pure.simp vs. HOL.simp.
  1807 
  1808 * The command 'unfolding' and proof method "unfold" include a second
  1809 stage where given equations are passed through the attribute "abs_def"
  1810 before rewriting. This ensures that definitions are fully expanded,
  1811 regardless of the actual parameters that are provided. Rare
  1812 INCOMPATIBILITY in some corner cases: use proof method (simp only:)
  1813 instead, or declare [[unfold_abs_def = false]] in the proof context.
  1814 
  1815 * Type-inference improves sorts of newly introduced type variables for
  1816 the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
  1817 Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
  1818 produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
  1819 INCOMPATIBILITY, need to provide explicit type constraints for Pure
  1820 types where this is really intended.
  1821 
  1822 
  1823 *** HOL ***
  1824 
  1825 * New proof method "argo" using the built-in Argo solver based on SMT
  1826 technology. The method can be used to prove goals of quantifier-free
  1827 propositional logic, goals based on a combination of quantifier-free
  1828 propositional logic with equality, and goals based on a combination of
  1829 quantifier-free propositional logic with linear real arithmetic
  1830 including min/max/abs. See HOL/ex/Argo_Examples.thy for examples.
  1831 
  1832 * The new "nunchaku" command integrates the Nunchaku model finder. The
  1833 tool is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details.
  1834 
  1835 * Metis: The problem encoding has changed very slightly. This might
  1836 break existing proofs. INCOMPATIBILITY.
  1837 
  1838 * Sledgehammer:
  1839   - The MaSh relevance filter is now faster than before.
  1840   - Produce syntactically correct Vampire 4.0 problem files.
  1841 
  1842 * (Co)datatype package:
  1843   - New commands for defining corecursive functions and reasoning about
  1844     them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
  1845     'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof
  1846     method. See 'isabelle doc corec'.
  1847   - The predicator :: ('a \<Rightarrow> bool) \<Rightarrow> 'a F \<Rightarrow> bool is now a first-class
  1848     citizen in bounded natural functors.
  1849   - 'primrec' now allows nested calls through the predicator in addition
  1850     to the map function.
  1851   - 'bnf' automatically discharges reflexive proof obligations.
  1852   - 'bnf' outputs a slightly modified proof obligation expressing rel in
  1853        terms of map and set
  1854        (not giving a specification for rel makes this one reflexive).
  1855   - 'bnf' outputs a new proof obligation expressing pred in terms of set
  1856        (not giving a specification for pred makes this one reflexive).
  1857     INCOMPATIBILITY: manual 'bnf' declarations may need adjustment.
  1858   - Renamed lemmas:
  1859       rel_prod_apply ~> rel_prod_inject
  1860       pred_prod_apply ~> pred_prod_inject
  1861     INCOMPATIBILITY.
  1862   - The "size" plugin has been made compatible again with locales.
  1863   - The theorems about "rel" and "set" may have a slightly different (but
  1864     equivalent) form.
  1865     INCOMPATIBILITY.
  1866 
  1867 * The 'coinductive' command produces a proper coinduction rule for
  1868 mutual coinductive predicates. This new rule replaces the old rule,
  1869 which exposed details of the internal fixpoint construction and was
  1870 hard to use. INCOMPATIBILITY.
  1871 
  1872 * New abbreviations for negated existence (but not bounded existence):
  1873 
  1874   \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)
  1875   \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)
  1876 
  1877 * The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
  1878 has been removed for output. It is retained for input only, until it is
  1879 eliminated altogether.
  1880 
  1881 * The unique existence quantifier no longer provides 'binder' syntax,
  1882 but uses syntax translations (as for bounded unique existence). Thus
  1883 iterated quantification \<exists>!x y. P x y with its slightly confusing
  1884 sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead,
  1885 pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y
  1886 (analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential
  1887 INCOMPATIBILITY in rare situations.
  1888 
  1889 * Conventional syntax "%(). t" for unit abstractions. Slight syntactic
  1890 INCOMPATIBILITY.
  1891 
  1892 * Renamed constants and corresponding theorems:
  1893 
  1894     setsum ~> sum
  1895     setprod ~> prod
  1896     listsum ~> sum_list
  1897     listprod ~> prod_list
  1898 
  1899 INCOMPATIBILITY.
  1900 
  1901 * Sligthly more standardized theorem names:
  1902     sgn_times ~> sgn_mult
  1903     sgn_mult' ~> Real_Vector_Spaces.sgn_mult
  1904     divide_zero_left ~> div_0
  1905     zero_mod_left ~> mod_0
  1906     divide_zero ~> div_by_0
  1907     divide_1 ~> div_by_1
  1908     nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left
  1909     div_mult_self1_is_id ~> nonzero_mult_div_cancel_left
  1910     nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right
  1911     div_mult_self2_is_id ~> nonzero_mult_div_cancel_right
  1912     is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left
  1913     is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right
  1914     mod_div_equality ~> div_mult_mod_eq
  1915     mod_div_equality2 ~> mult_div_mod_eq
  1916     mod_div_equality3 ~> mod_div_mult_eq
  1917     mod_div_equality4 ~> mod_mult_div_eq
  1918     minus_div_eq_mod ~> minus_div_mult_eq_mod
  1919     minus_div_eq_mod2 ~> minus_mult_div_eq_mod
  1920     minus_mod_eq_div ~> minus_mod_eq_div_mult
  1921     minus_mod_eq_div2 ~> minus_mod_eq_mult_div
  1922     div_mod_equality' ~> minus_mod_eq_div_mult [symmetric]
  1923     mod_div_equality' ~> minus_div_mult_eq_mod [symmetric]
  1924     zmod_zdiv_equality ~> mult_div_mod_eq [symmetric]
  1925     zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric]
  1926     Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
  1927     mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
  1928     zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
  1929     div_1 ~> div_by_Suc_0
  1930     mod_1 ~> mod_by_Suc_0
  1931 INCOMPATIBILITY.
  1932 
  1933 * New type class "idom_abs_sgn" specifies algebraic properties
  1934 of sign and absolute value functions.  Type class "sgn_if" has
  1935 disappeared.  Slight INCOMPATIBILITY.
  1936 
  1937 * Dedicated syntax LENGTH('a) for length of types.
  1938 
  1939 * Characters (type char) are modelled as finite algebraic type
  1940 corresponding to {0..255}.
  1941 
  1942   - Logical representation:
  1943     * 0 is instantiated to the ASCII zero character.
  1944     * All other characters are represented as "Char n"
  1945       with n being a raw numeral expression less than 256.
  1946     * Expressions of the form "Char n" with n greater than 255
  1947       are non-canonical.
  1948   - Printing and parsing:
  1949     * Printable characters are printed and parsed as "CHR ''\<dots>''"
  1950       (as before).
  1951     * The ASCII zero character is printed and parsed as "0".
  1952     * All other canonical characters are printed as "CHR 0xXX"
  1953       with XX being the hexadecimal character code.  "CHR n"
  1954       is parsable for every numeral expression n.
  1955     * Non-canonical characters have no special syntax and are
  1956       printed as their logical representation.
  1957   - Explicit conversions from and to the natural numbers are
  1958     provided as char_of_nat, nat_of_char (as before).
  1959   - The auxiliary nibble type has been discontinued.
  1960 
  1961 INCOMPATIBILITY.
  1962 
  1963 * Type class "div" with operation "mod" renamed to type class "modulo"
  1964 with operation "modulo", analogously to type class "divide". This
  1965 eliminates the need to qualify any of those names in the presence of
  1966 infix "mod" syntax. INCOMPATIBILITY.
  1967 
  1968 * Statements and proofs of Knaster-Tarski fixpoint combinators lfp/gfp
  1969 have been clarified. The fixpoint properties are lfp_fixpoint, its
  1970 symmetric lfp_unfold (as before), and the duals for gfp. Auxiliary items
  1971 for the proof (lfp_lemma2 etc.) are no longer exported, but can be
  1972 easily recovered by composition with eq_refl. Minor INCOMPATIBILITY.
  1973 
  1974 * Constant "surj" is a mere input abbreviation, to avoid hiding an
  1975 equation in term output. Minor INCOMPATIBILITY.
  1976 
  1977 * Command 'code_reflect' accepts empty constructor lists for datatypes,
  1978 which renders those abstract effectively.
  1979 
  1980 * Command 'export_code' checks given constants for abstraction
  1981 violations: a small guarantee that given constants specify a safe
  1982 interface for the generated code.
  1983 
  1984 * Code generation for Scala: ambiguous implicts in class diagrams are
  1985 spelt out explicitly.
  1986 
  1987 * Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on
  1988 explicitly provided auxiliary definitions for required type class
  1989 dictionaries rather than half-working magic. INCOMPATIBILITY, see the
  1990 tutorial on code generation for details.
  1991 
  1992 * Theory Set_Interval: substantial new theorems on indexed sums and
  1993 products.
  1994 
  1995 * Locale bijection establishes convenient default simp rules such as
  1996 "inv f (f a) = a" for total bijections.
  1997 
  1998 * Abstract locales semigroup, abel_semigroup, semilattice,
  1999 semilattice_neutr, ordering, ordering_top, semilattice_order,
  2000 semilattice_neutr_order, comm_monoid_set, semilattice_set,
  2001 semilattice_neutr_set, semilattice_order_set,
  2002 semilattice_order_neutr_set monoid_list, comm_monoid_list,
  2003 comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified
  2004 syntax uniformly that does not clash with corresponding global syntax.
  2005 INCOMPATIBILITY.
  2006 
  2007 * Former locale lifting_syntax is now a bundle, which is easier to
  2008 include in a local context or theorem statement, e.g. "context includes
  2009 lifting_syntax begin ... end". Minor INCOMPATIBILITY.
  2010 
  2011 * Some old / obsolete theorems have been renamed / removed, potential
  2012 INCOMPATIBILITY.
  2013 
  2014   nat_less_cases  --  removed, use linorder_cases instead
  2015   inv_image_comp  --  removed, use image_inv_f_f instead
  2016   image_surj_f_inv_f  ~>  image_f_inv_f
  2017 
  2018 * Some theorems about groups and orders have been generalised from
  2019   groups to semi-groups that are also monoids:
  2020     le_add_same_cancel1
  2021     le_add_same_cancel2
  2022     less_add_same_cancel1
  2023     less_add_same_cancel2
  2024     add_le_same_cancel1
  2025     add_le_same_cancel2
  2026     add_less_same_cancel1
  2027     add_less_same_cancel2
  2028 
  2029 * Some simplifications theorems about rings have been removed, since
  2030   superseeded by a more general version:
  2031     less_add_cancel_left_greater_zero ~> less_add_same_cancel1
  2032     less_add_cancel_right_greater_zero ~> less_add_same_cancel2
  2033     less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1
  2034     less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2
  2035     less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1
  2036     less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2
  2037     less_add_cancel_left_less_zero ~> add_less_same_cancel1
  2038     less_add_cancel_right_less_zero ~> add_less_same_cancel2
  2039 INCOMPATIBILITY.
  2040 
  2041 * Renamed split_if -> if_split and split_if_asm -> if_split_asm to
  2042 resemble the f.split naming convention, INCOMPATIBILITY.
  2043 
  2044 * Added class topological_monoid.
  2045 
  2046 * The following theorems have been renamed:
  2047 
  2048   setsum_left_distrib ~> sum_distrib_right
  2049   setsum_right_distrib ~> sum_distrib_left
  2050 
  2051 INCOMPATIBILITY.
  2052 
  2053 * Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
  2054 INCOMPATIBILITY.
  2055 
  2056 * "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional
  2057 comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f `
  2058 A)".
  2059 
  2060 * Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY.
  2061 
  2062 * The type class ordered_comm_monoid_add is now called
  2063 ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add
  2064 is introduced as the combination of ordered_ab_semigroup_add +
  2065 comm_monoid_add. INCOMPATIBILITY.
  2066 
  2067 * Introduced the type classes canonically_ordered_comm_monoid_add and
  2068 dioid.
  2069 
  2070 * Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When
  2071 instantiating linordered_semiring_strict and ordered_ab_group_add, an
  2072 explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might
  2073 be required. INCOMPATIBILITY.
  2074 
  2075 * Dropped various legacy fact bindings, whose replacements are often
  2076 of a more general type also:
  2077   lcm_left_commute_nat ~> lcm.left_commute
  2078   lcm_left_commute_int ~> lcm.left_commute
  2079   gcd_left_commute_nat ~> gcd.left_commute
  2080   gcd_left_commute_int ~> gcd.left_commute
  2081   gcd_greatest_iff_nat ~> gcd_greatest_iff
  2082   gcd_greatest_iff_int ~> gcd_greatest_iff
  2083   coprime_dvd_mult_nat ~> coprime_dvd_mult
  2084   coprime_dvd_mult_int ~> coprime_dvd_mult
  2085   zpower_numeral_even ~> power_numeral_even
  2086   gcd_mult_cancel_nat ~> gcd_mult_cancel
  2087   gcd_mult_cancel_int ~> gcd_mult_cancel
  2088   div_gcd_coprime_nat ~> div_gcd_coprime
  2089   div_gcd_coprime_int ~> div_gcd_coprime
  2090   zpower_numeral_odd ~> power_numeral_odd
  2091   zero_less_int_conv ~> of_nat_0_less_iff
  2092   gcd_greatest_nat ~> gcd_greatest
  2093   gcd_greatest_int ~> gcd_greatest
  2094   coprime_mult_nat ~> coprime_mult
  2095   coprime_mult_int ~> coprime_mult
  2096   lcm_commute_nat ~> lcm.commute
  2097   lcm_commute_int ~> lcm.commute
  2098   int_less_0_conv ~> of_nat_less_0_iff
  2099   gcd_commute_nat ~> gcd.commute
  2100   gcd_commute_int ~> gcd.commute
  2101   Gcd_insert_nat ~> Gcd_insert
  2102   Gcd_insert_int ~> Gcd_insert
  2103   of_int_int_eq ~> of_int_of_nat_eq
  2104   lcm_least_nat ~> lcm_least
  2105   lcm_least_int ~> lcm_least
  2106   lcm_assoc_nat ~> lcm.assoc
  2107   lcm_assoc_int ~> lcm.assoc
  2108   int_le_0_conv ~> of_nat_le_0_iff
  2109   int_eq_0_conv ~> of_nat_eq_0_iff
  2110   Gcd_empty_nat ~> Gcd_empty
  2111   Gcd_empty_int ~> Gcd_empty
  2112   gcd_assoc_nat ~> gcd.assoc
  2113   gcd_assoc_int ~> gcd.assoc
  2114   zero_zle_int ~> of_nat_0_le_iff
  2115   lcm_dvd2_nat ~> dvd_lcm2
  2116   lcm_dvd2_int ~> dvd_lcm2
  2117   lcm_dvd1_nat ~> dvd_lcm1
  2118   lcm_dvd1_int ~> dvd_lcm1
  2119   gcd_zero_nat ~> gcd_eq_0_iff
  2120   gcd_zero_int ~> gcd_eq_0_iff
  2121   gcd_dvd2_nat ~> gcd_dvd2
  2122   gcd_dvd2_int ~> gcd_dvd2
  2123   gcd_dvd1_nat ~> gcd_dvd1
  2124   gcd_dvd1_int ~> gcd_dvd1
  2125   int_numeral ~> of_nat_numeral
  2126   lcm_ac_nat ~> ac_simps
  2127   lcm_ac_int ~> ac_simps
  2128   gcd_ac_nat ~> ac_simps
  2129   gcd_ac_int ~> ac_simps
  2130   abs_int_eq ~> abs_of_nat
  2131   zless_int ~> of_nat_less_iff
  2132   zdiff_int ~> of_nat_diff
  2133   zadd_int ~> of_nat_add
  2134   int_mult ~> of_nat_mult
  2135   int_Suc ~> of_nat_Suc
  2136   inj_int ~> inj_of_nat
  2137   int_1 ~> of_nat_1
  2138   int_0 ~> of_nat_0
  2139   Lcm_empty_nat ~> Lcm_empty
  2140   Lcm_empty_int ~> Lcm_empty
  2141   Lcm_insert_nat ~> Lcm_insert
  2142   Lcm_insert_int ~> Lcm_insert
  2143   comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd
  2144   comp_fun_idem_gcd_int ~> comp_fun_idem_gcd
  2145   comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm
  2146   comp_fun_idem_lcm_int ~> comp_fun_idem_lcm
  2147   Lcm_eq_0 ~> Lcm_eq_0_I
  2148   Lcm0_iff ~> Lcm_0_iff
  2149   Lcm_dvd_int ~> Lcm_least
  2150   divides_mult_nat ~> divides_mult
  2151   divides_mult_int ~> divides_mult
  2152   lcm_0_nat ~> lcm_0_right
  2153   lcm_0_int ~> lcm_0_right
  2154   lcm_0_left_nat ~> lcm_0_left
  2155   lcm_0_left_int ~> lcm_0_left
  2156   dvd_gcd_D1_nat ~> dvd_gcdD1
  2157   dvd_gcd_D1_int ~> dvd_gcdD1
  2158   dvd_gcd_D2_nat ~> dvd_gcdD2
  2159   dvd_gcd_D2_int ~> dvd_gcdD2
  2160   coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff
  2161   coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff
  2162   realpow_minus_mult ~> power_minus_mult
  2163   realpow_Suc_le_self ~> power_Suc_le_self
  2164   dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest
  2165 INCOMPATIBILITY.
  2166 
  2167 * Renamed HOL/Quotient_Examples/FSet.thy to
  2168 HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY.
  2169 
  2170 * Session HOL-Library: theory FinFun bundles "finfun_syntax" and
  2171 "no_finfun_syntax" allow to control optional syntax in local contexts;
  2172 this supersedes former theory FinFun_Syntax. INCOMPATIBILITY, e.g. use
  2173 "unbundle finfun_syntax" to imitate import of
  2174 "~~/src/HOL/Library/FinFun_Syntax".
  2175 
  2176 * Session HOL-Library: theory Multiset_Permutations (executably) defines
  2177 the set of permutations of a given set or multiset, i.e. the set of all
  2178 lists that contain every element of the carrier (multi-)set exactly
  2179 once.
  2180 
  2181 * Session HOL-Library: multiset membership is now expressed using
  2182 set_mset rather than count.
  2183 
  2184   - Expressions "count M a > 0" and similar simplify to membership
  2185     by default.
  2186 
  2187   - Converting between "count M a = 0" and non-membership happens using
  2188     equations count_eq_zero_iff and not_in_iff.
  2189 
  2190   - Rules count_inI and in_countE obtain facts of the form
  2191     "count M a = n" from membership.
  2192 
  2193   - Rules count_in_diffI and in_diff_countE obtain facts of the form
  2194     "count M a = n + count N a" from membership on difference sets.
  2195 
  2196 INCOMPATIBILITY.
  2197 
  2198 * Session HOL-Library: theory LaTeXsugar uses new-style "dummy_pats" for
  2199 displaying equations in functional programming style --- variables
  2200 present on the left-hand but not on the righ-hand side are replaced by
  2201 underscores.
  2202 
  2203 * Session HOL-Library: theory Combinator_PER provides combinator to
  2204 build partial equivalence relations from a predicate and an equivalence
  2205 relation.
  2206 
  2207 * Session HOL-Library: theory Perm provides basic facts about almost
  2208 everywhere fix bijections.
  2209 
  2210 * Session HOL-Library: theory Normalized_Fraction allows viewing an
  2211 element of a field of fractions as a normalized fraction (i.e. a pair of
  2212 numerator and denominator such that the two are coprime and the
  2213 denominator is normalized wrt. unit factors).
  2214 
  2215 * Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis.
  2216 
  2217 * Session HOL-Multivariate_Analysis has been renamed to HOL-Analysis.
  2218 
  2219 * Session HOL-Analysis: measure theory has been moved here from
  2220 HOL-Probability. When importing HOL-Analysis some theorems need
  2221 additional name spaces prefixes due to name clashes. INCOMPATIBILITY.
  2222 
  2223 * Session HOL-Analysis: more complex analysis including Cauchy's
  2224 inequality, Liouville theorem, open mapping theorem, maximum modulus
  2225 principle, Residue theorem, Schwarz Lemma.
  2226 
  2227 * Session HOL-Analysis: Theory of polyhedra: faces, extreme points,
  2228 polytopes, and the Krein–Milman Minkowski theorem.
  2229 
  2230 * Session HOL-Analysis: Numerous results ported from the HOL Light
  2231 libraries: homeomorphisms, continuous function extensions, invariance of
  2232 domain.
  2233 
  2234 * Session HOL-Probability: the type of emeasure and nn_integral was
  2235 changed from ereal to ennreal, INCOMPATIBILITY.
  2236 
  2237   emeasure :: 'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal
  2238   nn_integral :: 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal
  2239 
  2240 * Session HOL-Probability: Code generation and QuickCheck for
  2241 Probability Mass Functions.
  2242 
  2243 * Session HOL-Probability: theory Random_Permutations contains some
  2244 theory about choosing a permutation of a set uniformly at random and
  2245 folding over a list in random order.
  2246 
  2247 * Session HOL-Probability: theory SPMF formalises discrete
  2248 subprobability distributions.
  2249 
  2250 * Session HOL-Library: the names of multiset theorems have been
  2251 normalised to distinguish which ordering the theorems are about
  2252 
  2253     mset_less_eqI ~> mset_subset_eqI
  2254     mset_less_insertD ~> mset_subset_insertD
  2255     mset_less_eq_count ~> mset_subset_eq_count
  2256     mset_less_diff_self ~> mset_subset_diff_self
  2257     mset_le_exists_conv ~> mset_subset_eq_exists_conv
  2258     mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel
  2259     mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel
  2260     mset_le_mono_add ~> mset_subset_eq_mono_add
  2261     mset_le_add_left ~> mset_subset_eq_add_left
  2262     mset_le_add_right ~> mset_subset_eq_add_right
  2263     mset_le_single ~> mset_subset_eq_single
  2264     mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute
  2265     diff_le_self ~> diff_subset_eq_self
  2266     mset_leD ~> mset_subset_eqD
  2267     mset_lessD ~> mset_subsetD
  2268     mset_le_insertD ~> mset_subset_eq_insertD
  2269     mset_less_of_empty ~> mset_subset_of_empty
  2270     mset_less_size ~> mset_subset_size
  2271     wf_less_mset_rel ~> wf_subset_mset_rel
  2272     count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq
  2273     mset_remdups_le ~> mset_remdups_subset_eq
  2274     ms_lesseq_impl ~> subset_eq_mset_impl
  2275 
  2276 Some functions have been renamed:
  2277     ms_lesseq_impl -> subset_eq_mset_impl
  2278 
  2279 * HOL-Library: multisets are now ordered with the multiset ordering
  2280     #\<subseteq># ~> \<le>
  2281     #\<subset># ~> <
  2282     le_multiset ~> less_eq_multiset
  2283     less_multiset ~> le_multiset
  2284 INCOMPATIBILITY.
  2285 
  2286 * Session HOL-Library: the prefix multiset_order has been discontinued:
  2287 the theorems can be directly accessed. As a consequence, the lemmas
  2288 "order_multiset" and "linorder_multiset" have been discontinued, and the
  2289 interpretations "multiset_linorder" and "multiset_wellorder" have been
  2290 replaced by instantiations. INCOMPATIBILITY.
  2291 
  2292 * Session HOL-Library: some theorems about the multiset ordering have
  2293 been renamed:
  2294 
  2295     le_multiset_def ~> less_eq_multiset_def
  2296     less_multiset_def ~> le_multiset_def
  2297     less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset
  2298     mult_less_not_refl ~> mset_le_not_refl
  2299     mult_less_trans ~> mset_le_trans
  2300     mult_less_not_sym ~> mset_le_not_sym
  2301     mult_less_asym ~> mset_le_asym
  2302     mult_less_irrefl ~> mset_le_irrefl
  2303     union_less_mono2{,1,2} ~> union_le_mono2{,1,2}
  2304 
  2305     le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O
  2306     le_multiset_total ~> less_eq_multiset_total
  2307     less_multiset_right_total ~> subset_eq_imp_le_multiset
  2308     le_multiset_empty_left ~> less_eq_multiset_empty_left
  2309     le_multiset_empty_right ~> less_eq_multiset_empty_right
  2310     less_multiset_empty_right ~> le_multiset_empty_left
  2311     less_multiset_empty_left ~> le_multiset_empty_right
  2312     union_less_diff_plus ~> union_le_diff_plus
  2313     ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset
  2314     less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty
  2315     le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty
  2316 INCOMPATIBILITY.
  2317 
  2318 * Session HOL-Library: the lemma mset_map has now the attribute [simp].
  2319 INCOMPATIBILITY.
  2320 
  2321 * Session HOL-Library: some theorems about multisets have been removed.
  2322 INCOMPATIBILITY, use the following replacements:
  2323 
  2324     le_multiset_plus_plus_left_iff ~> add_less_cancel_right
  2325     less_multiset_plus_plus_left_iff ~> add_less_cancel_right
  2326     le_multiset_plus_plus_right_iff ~> add_less_cancel_left
  2327     less_multiset_plus_plus_right_iff ~> add_less_cancel_left
  2328     add_eq_self_empty_iff ~> add_cancel_left_right
  2329     mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right
  2330     mset_less_add_bothsides ~> subset_mset.add_less_cancel_right
  2331     mset_le_add_bothsides ~> subset_mset.add_less_cancel_right
  2332     empty_inter ~> subset_mset.inf_bot_left
  2333     inter_empty ~> subset_mset.inf_bot_right
  2334     empty_sup ~> subset_mset.sup_bot_left
  2335     sup_empty ~> subset_mset.sup_bot_right
  2336     bdd_below_multiset ~> subset_mset.bdd_above_bot
  2337     subset_eq_empty ~> subset_mset.le_zero_eq
  2338     le_empty ~> subset_mset.le_zero_eq
  2339     mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero
  2340     mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero
  2341 
  2342 * Session HOL-Library: some typeclass constraints about multisets have
  2343 been reduced from ordered or linordered to preorder. Multisets have the
  2344 additional typeclasses order_bot, no_top,
  2345 ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,
  2346 linordered_cancel_ab_semigroup_add, and
  2347 ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY.
  2348 
  2349 * Session HOL-Library: there are some new simplification rules about
  2350 multisets, the multiset ordering, and the subset ordering on multisets.
  2351 INCOMPATIBILITY.
  2352 
  2353 * Session HOL-Library: the subset ordering on multisets has now the
  2354 interpretations ordered_ab_semigroup_monoid_add_imp_le and
  2355 bounded_lattice_bot. INCOMPATIBILITY.
  2356 
  2357 * Session HOL-Library, theory Multiset: single has been removed in favor
  2358 of add_mset that roughly corresponds to Set.insert. Some theorems have
  2359 removed or changed:
  2360 
  2361   single_not_empty ~> add_mset_not_empty or empty_not_add_mset
  2362   fold_mset_insert ~> fold_mset_add_mset
  2363   image_mset_insert ~> image_mset_add_mset
  2364   union_single_eq_diff
  2365   multi_self_add_other_not_self
  2366   diff_single_eq_union
  2367 INCOMPATIBILITY.
  2368 
  2369 * Session HOL-Library, theory Multiset: some theorems have been changed
  2370 to use add_mset instead of single:
  2371 
  2372   mset_add
  2373   multi_self_add_other_not_self
  2374   diff_single_eq_union
  2375   union_single_eq_diff
  2376   union_single_eq_member
  2377   add_eq_conv_diff
  2378   insert_noteq_member
  2379   add_eq_conv_ex
  2380   multi_member_split
  2381   multiset_add_sub_el_shuffle
  2382   mset_subset_eq_insertD
  2383   mset_subset_insertD
  2384   insert_subset_eq_iff
  2385   insert_union_subset_iff
  2386   multi_psub_of_add_self
  2387   inter_add_left1
  2388   inter_add_left2
  2389   inter_add_right1
  2390   inter_add_right2
  2391   sup_union_left1
  2392   sup_union_left2
  2393   sup_union_right1
  2394   sup_union_right2
  2395   size_eq_Suc_imp_eq_union
  2396   multi_nonempty_split
  2397   mset_insort
  2398   mset_update
  2399   mult1I
  2400   less_add
  2401   mset_zip_take_Cons_drop_twice
  2402   rel_mset_Zero
  2403   msed_map_invL
  2404   msed_map_invR
  2405   msed_rel_invL
  2406   msed_rel_invR
  2407   le_multiset_right_total
  2408   multiset_induct
  2409   multiset_induct2_size
  2410   multiset_induct2
  2411 INCOMPATIBILITY.
  2412 
  2413 * Session HOL-Library, theory Multiset: the definitions of some
  2414 constants have changed to use add_mset instead of adding a single
  2415 element:
  2416 
  2417   image_mset
  2418   mset
  2419   replicate_mset
  2420   mult1
  2421   pred_mset
  2422   rel_mset'
  2423   mset_insort
  2424 
  2425 INCOMPATIBILITY.
  2426 
  2427 * Session HOL-Library, theory Multiset: due to the above changes, the
  2428 attributes of some multiset theorems have been changed:
  2429 
  2430   insert_DiffM  [] ~> [simp]
  2431   insert_DiffM2 [simp] ~> []
  2432   diff_add_mset_swap [simp]
  2433   fold_mset_add_mset [simp]
  2434   diff_diff_add [simp] (for multisets only)
  2435   diff_cancel [simp] ~> []
  2436   count_single [simp] ~> []
  2437   set_mset_single [simp] ~> []
  2438   size_multiset_single [simp] ~> []
  2439   size_single [simp] ~> []
  2440   image_mset_single [simp] ~> []
  2441   mset_subset_eq_mono_add_right_cancel [simp] ~> []
  2442   mset_subset_eq_mono_add_left_cancel [simp] ~> []
  2443   fold_mset_single [simp] ~> []
  2444   subset_eq_empty [simp] ~> []
  2445   empty_sup [simp] ~> []
  2446   sup_empty [simp] ~> []
  2447   inter_empty [simp] ~> []
  2448   empty_inter [simp] ~> []
  2449 INCOMPATIBILITY.
  2450 
  2451 * Session HOL-Library, theory Multiset: the order of the variables in
  2452 the second cases of multiset_induct, multiset_induct2_size,
  2453 multiset_induct2 has been changed (e.g. Add A a ~> Add a A).
  2454 INCOMPATIBILITY.
  2455 
  2456 * Session HOL-Library, theory Multiset: there is now a simplification
  2457 procedure on multisets. It mimics the behavior of the procedure on
  2458 natural numbers. INCOMPATIBILITY.
  2459 
  2460 * Session HOL-Library, theory Multiset: renamed sums and products of
  2461 multisets:
  2462 
  2463   msetsum ~> sum_mset
  2464   msetprod ~> prod_mset
  2465 
  2466 * Session HOL-Library, theory Multiset: the notation for intersection
  2467 and union of multisets have been changed:
  2468 
  2469   #\<inter> ~> \<inter>#
  2470   #\<union> ~> \<union>#
  2471 
  2472 INCOMPATIBILITY.
  2473 
  2474 * Session HOL-Library, theory Multiset: the lemma
  2475 one_step_implies_mult_aux on multisets has been removed, use
  2476 one_step_implies_mult instead. INCOMPATIBILITY.
  2477 
  2478 * Session HOL-Library: theory Complete_Partial_Order2 provides reasoning
  2479 support for monotonicity and continuity in chain-complete partial orders
  2480 and about admissibility conditions for fixpoint inductions.
  2481 
  2482 * Session HOL-Library: theory Library/Polynomial contains also
  2483 derivation of polynomials (formerly in Library/Poly_Deriv) but not
  2484 gcd/lcm on polynomials over fields. This has been moved to a separate
  2485 theory Library/Polynomial_GCD_euclidean.thy, to pave way for a possible
  2486 future different type class instantiation for polynomials over factorial
  2487 rings. INCOMPATIBILITY.
  2488 
  2489 * Session HOL-Library: theory Sublist provides function "prefixes" with
  2490 the following renaming
  2491 
  2492   prefixeq -> prefix
  2493   prefix -> strict_prefix
  2494   suffixeq -> suffix
  2495   suffix -> strict_suffix
  2496 
  2497 Added theory of longest common prefixes.
  2498 
  2499 * Session HOL-Number_Theory: algebraic foundation for primes:
  2500 Generalisation of predicate "prime" and introduction of predicates
  2501 "prime_elem", "irreducible", a "prime_factorization" function, and the
  2502 "factorial_ring" typeclass with instance proofs for nat, int, poly. Some
  2503 theorems now have different names, most notably "prime_def" is now
  2504 "prime_nat_iff". INCOMPATIBILITY.
  2505 
  2506 * Session Old_Number_Theory has been removed, after porting remaining
  2507 theories.
  2508 
  2509 * Session HOL-Types_To_Sets provides an experimental extension of
  2510 Higher-Order Logic to allow translation of types to sets.
  2511 
  2512 
  2513 *** ML ***
  2514 
  2515 * Integer.gcd and Integer.lcm use efficient operations from the Poly/ML
  2516 library (notably for big integers). Subtle change of semantics:
  2517 Integer.gcd and Integer.lcm both normalize the sign, results are never
  2518 negative. This coincides with the definitions in HOL/GCD.thy.
  2519 INCOMPATIBILITY.
  2520 
  2521 * Structure Rat for rational numbers is now an integral part of
  2522 Isabelle/ML, with special notation @int/nat or @int for numerals (an
  2523 abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
  2524 printing. Standard operations on type Rat.rat are provided via ad-hoc
  2525 overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to
  2526 use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
  2527 superseded by General.Div.
  2528 
  2529 * ML antiquotation @{path} is superseded by @{file}, which ensures that
  2530 the argument is a plain file. Minor INCOMPATIBILITY.
  2531 
  2532 * Antiquotation @{make_string} is available during Pure bootstrap --
  2533 with approximative output quality.
  2534 
  2535 * Low-level ML system structures (like PolyML and RunCall) are no longer
  2536 exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY.
  2537 
  2538 * The ML function "ML" provides easy access to run-time compilation.
  2539 This is particularly useful for conditional compilation, without
  2540 requiring separate files.
  2541 
  2542 * Option ML_exception_debugger controls detailed exception trace via the
  2543 Poly/ML debugger. Relevant ML modules need to be compiled beforehand
  2544 with ML_file_debug, or with ML_file and option ML_debugger enabled. Note
  2545 debugger information requires consirable time and space: main
  2546 Isabelle/HOL with full debugger support may need ML_system_64.
  2547 
  2548 * Local_Theory.restore has been renamed to Local_Theory.reset to
  2549 emphasize its disruptive impact on the cumulative context, notably the
  2550 scope of 'private' or 'qualified' names. Note that Local_Theory.reset is
  2551 only appropriate when targets are managed, e.g. starting from a global
  2552 theory and returning to it. Regular definitional packages should use
  2553 balanced blocks of Local_Theory.open_target versus
  2554 Local_Theory.close_target instead. Rare INCOMPATIBILITY.
  2555 
  2556 * Structure TimeLimit (originally from the SML/NJ library) has been
  2557 replaced by structure Timeout, with slightly different signature.
  2558 INCOMPATIBILITY.
  2559 
  2560 * Discontinued cd and pwd operations, which are not well-defined in a
  2561 multi-threaded environment. Note that files are usually located
  2562 relatively to the master directory of a theory (see also
  2563 File.full_path). Potential INCOMPATIBILITY.
  2564 
  2565 * Binding.empty_atts supersedes Thm.empty_binding and
  2566 Attrib.empty_binding. Minor INCOMPATIBILITY.
  2567 
  2568 
  2569 *** System ***
  2570 
  2571 * SML/NJ and old versions of Poly/ML are no longer supported.
  2572 
  2573 * Poly/ML heaps now follow the hierarchy of sessions, and thus require
  2574 much less disk space.
  2575 
  2576 * The Isabelle ML process is now managed directly by Isabelle/Scala, and
  2577 shell scripts merely provide optional command-line access. In
  2578 particular:
  2579 
  2580   . Scala module ML_Process to connect to the raw ML process,
  2581     with interaction via stdin/stdout/stderr or in batch mode;
  2582   . command-line tool "isabelle console" as interactive wrapper;
  2583   . command-line tool "isabelle process" as batch mode wrapper.
  2584 
  2585 * The executable "isabelle_process" has been discontinued. Tools and
  2586 prover front-ends should use ML_Process or Isabelle_Process in
  2587 Isabelle/Scala. INCOMPATIBILITY.
  2588 
  2589 * New command-line tool "isabelle process" supports ML evaluation of
  2590 literal expressions (option -e) or files (option -f) in the context of a
  2591 given heap image. Errors lead to premature exit of the ML process with
  2592 return code 1.
  2593 
  2594 * The command-line tool "isabelle build" supports option -N for cyclic
  2595 shuffling of NUMA CPU nodes. This may help performance tuning on Linux
  2596 servers with separate CPU/memory modules.
  2597 
  2598 * System option "threads" (for the size of the Isabelle/ML thread farm)
  2599 is also passed to the underlying ML runtime system as --gcthreads,
  2600 unless there is already a default provided via ML_OPTIONS settings.
  2601 
  2602 * System option "checkpoint" helps to fine-tune the global heap space
  2603 management of isabelle build. This is relevant for big sessions that may
  2604 exhaust the small 32-bit address space of the ML process (which is used
  2605 by default).
  2606 
  2607 * System option "profiling" specifies the mode for global ML profiling
  2608 in "isabelle build". Possible values are "time", "allocations". The
  2609 command-line tool "isabelle profiling_report" helps to digest the
  2610 resulting log files.
  2611 
  2612 * System option "ML_process_policy" specifies an optional command prefix
  2613 for the underlying ML process, e.g. to control CPU affinity on
  2614 multiprocessor systems. The "isabelle jedit" tool allows to override the
  2615 implicit default via option -p.
  2616 
  2617 * Command-line tool "isabelle console" provides option -r to help to
  2618 bootstrapping Isabelle/Pure interactively.
  2619 
  2620 * Command-line tool "isabelle yxml" has been discontinued.
  2621 INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in
  2622 Isabelle/ML or Isabelle/Scala.
  2623 
  2624 * Many Isabelle tools that require a Java runtime system refer to the
  2625 settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64,
  2626 depending on the underlying platform. The settings for "isabelle build"
  2627 ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been
  2628 discontinued. Potential INCOMPATIBILITY.
  2629 
  2630 * The Isabelle system environment always ensures that the main
  2631 executables are found within the shell search $PATH: "isabelle" and
  2632 "isabelle_scala_script".
  2633 
  2634 * Isabelle tools may consist of .scala files: the Scala compiler is
  2635 invoked on the spot. The source needs to define some object that extends
  2636 Isabelle_Tool.Body.
  2637 
  2638 * File.bash_string, File.bash_path etc. represent Isabelle/ML and
  2639 Isabelle/Scala strings authentically within GNU bash. This is useful to
  2640 produce robust shell scripts under program control, without worrying
  2641 about spaces or special characters. Note that user output works via
  2642 Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and
  2643 less versatile) operations File.shell_quote, File.shell_path etc. have
  2644 been discontinued.
  2645 
  2646 * The isabelle_java executable allows to run a Java process within the
  2647 name space of Java and Scala components that are bundled with Isabelle,
  2648 but without the Isabelle settings environment.
  2649 
  2650 * Isabelle/Scala: the SSH module supports ssh and sftp connections, for
  2651 remote command-execution and file-system access. This resembles
  2652 operations from module File and Isabelle_System to some extent. Note
  2653 that Path specifications need to be resolved remotely via
  2654 ssh.remote_path instead of File.standard_path: the implicit process
  2655 environment is different, Isabelle settings are not available remotely.
  2656 
  2657 * Isabelle/Scala: the Mercurial module supports repositories via the
  2658 regular hg command-line interface. The repositroy clone and working
  2659 directory may reside on a local or remote file-system (via ssh
  2660 connection).
  2661 
  2662 
  2663 
  2664 New in Isabelle2016 (February 2016)
  2665 -----------------------------------
  2666 
  2667 *** General ***
  2668 
  2669 * Eisbach is now based on Pure instead of HOL. Objects-logics may import
  2670 either the theory ~~/src/HOL/Eisbach/Eisbach (for HOL etc.) or
  2671 ~~/src/HOL/Eisbach/Eisbach_Old_Appl_Syntax (for FOL, ZF etc.). Note that
  2672 the HOL-Eisbach session located in ~~/src/HOL/Eisbach/ contains further
  2673 examples that do require HOL.
  2674 
  2675 * Better resource usage on all platforms (Linux, Windows, Mac OS X) for
  2676 both Isabelle/ML and Isabelle/Scala.  Slightly reduced heap space usage.
  2677 
  2678 * Former "xsymbols" syntax with Isabelle symbols is used by default,
  2679 without any special print mode. Important ASCII replacement syntax
  2680 remains available under print mode "ASCII", but less important syntax
  2681 has been removed (see below).
  2682 
  2683 * Support for more arrow symbols, with rendering in LaTeX and Isabelle
  2684 fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>.
  2685 
  2686 * Special notation \<struct> for the first implicit 'structure' in the
  2687 context has been discontinued. Rare INCOMPATIBILITY, use explicit
  2688 structure name instead, notably in indexed notation with block-subscript
  2689 (e.g. \<odot>\<^bsub>A\<^esub>).
  2690 
  2691 * The glyph for \<diamond> in the IsabelleText font now corresponds better to its
  2692 counterpart \<box> as quantifier-like symbol. A small diamond is available as
  2693 \<diamondop>; the old symbol \<struct> loses this rendering and any special
  2694 meaning.
  2695 
  2696 * Syntax for formal comments "-- text" now also supports the symbolic
  2697 form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps
  2698 to update old sources.
  2699 
  2700 * Toplevel theorem statements have been simplified as follows:
  2701 
  2702   theorems             ~>  lemmas
  2703   schematic_lemma      ~>  schematic_goal
  2704   schematic_theorem    ~>  schematic_goal
  2705   schematic_corollary  ~>  schematic_goal
  2706 
  2707 Command-line tool "isabelle update_theorems" updates theory sources
  2708 accordingly.
  2709 
  2710 * Toplevel theorem statement 'proposition' is another alias for
  2711 'theorem'.
  2712 
  2713 * The old 'defs' command has been removed (legacy since Isabelle2014).
  2714 INCOMPATIBILITY, use regular 'definition' instead. Overloaded and/or
  2715 deferred definitions require a surrounding 'overloading' block.
  2716 
  2717 
  2718 *** Prover IDE -- Isabelle/Scala/jEdit ***
  2719 
  2720 * IDE support for the source-level debugger of Poly/ML, to work with
  2721 Isabelle/ML and official Standard ML. Option "ML_debugger" and commands
  2722 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',
  2723 'SML_file_no_debug' control compilation of sources with or without
  2724 debugging information. The Debugger panel allows to set breakpoints (via
  2725 context menu), step through stopped threads, evaluate local ML
  2726 expressions etc. At least one Debugger view needs to be active to have
  2727 any effect on the running ML program.
  2728 
  2729 * The State panel manages explicit proof state output, with dynamic
  2730 auto-update according to cursor movement. Alternatively, the jEdit
  2731 action "isabelle.update-state" (shortcut S+ENTER) triggers manual
  2732 update.
  2733 
  2734 * The Output panel no longer shows proof state output by default, to
  2735 avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or
  2736 enable option "editor_output_state".
  2737 
  2738 * The text overview column (status of errors, warnings etc.) is updated
  2739 asynchronously, leading to much better editor reactivity. Moreover, the
  2740 full document node content is taken into account. The width of the
  2741 column is scaled according to the main text area font, for improved
  2742 visibility.
  2743 
  2744 * The main text area no longer changes its color hue in outdated
  2745 situations. The text overview column takes over the role to indicate
  2746 unfinished edits in the PIDE pipeline. This avoids flashing text display
  2747 due to ad-hoc updates by auxiliary GUI components, such as the State
  2748 panel.
  2749 
  2750 * Slightly improved scheduling for urgent print tasks (e.g. command
  2751 state output, interactive queries) wrt. long-running background tasks.
  2752 
  2753 * Completion of symbols via prefix of \<name> or \<^name> or \name is
  2754 always possible, independently of the language context. It is never
  2755 implicit: a popup will show up unconditionally.
  2756 
  2757 * Additional abbreviations for syntactic completion may be specified in
  2758 $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with
  2759 support for simple templates using ASCII 007 (bell) as placeholder.
  2760 
  2761 * Symbols \<oplus>, \<Oplus>, \<otimes>, \<Otimes>, \<odot>, \<Odot>, \<ominus>, \<oslash> no longer provide abbreviations for
  2762 completion like "+o", "*o", ".o" etc. -- due to conflicts with other
  2763 ASCII syntax. INCOMPATIBILITY, use plain backslash-completion or define
  2764 suitable abbreviations in $ISABELLE_HOME_USER/etc/abbrevs.
  2765 
  2766 * Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls
  2767 emphasized text style; the effect is visible in document output, not in
  2768 the editor.
  2769 
  2770 * Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE,
  2771 instead of former C+e LEFT.
  2772 
  2773 * The command-line tool "isabelle jedit" and the isabelle.Main
  2774 application wrapper treat the default $USER_HOME/Scratch.thy more
  2775 uniformly, and allow the dummy file argument ":" to open an empty buffer
  2776 instead.
  2777 
  2778 * New command-line tool "isabelle jedit_client" allows to connect to an
  2779 already running Isabelle/jEdit process. This achieves the effect of
  2780 single-instance applications seen on common GUI desktops.
  2781 
  2782 * The default look-and-feel for Linux is the traditional "Metal", which
  2783 works better with GUI scaling for very high-resolution displays (e.g.
  2784 4K). Moreover, it is generally more robust than "Nimbus".
  2785 
  2786 * Update to jedit-5.3.0, with improved GUI scaling and support of
  2787 high-resolution displays (e.g. 4K).
  2788 
  2789 * The main Isabelle executable is managed as single-instance Desktop
  2790 application uniformly on all platforms: Linux, Windows, Mac OS X.
  2791 
  2792 
  2793 *** Document preparation ***
  2794 
  2795 * Commands 'paragraph' and 'subparagraph' provide additional section
  2796 headings. Thus there are 6 levels of standard headings, as in HTML.
  2797 
  2798 * Command 'text_raw' has been clarified: input text is processed as in
  2799 'text' (with antiquotations and control symbols). The key difference is
  2800 the lack of the surrounding isabelle markup environment in output.
  2801 
  2802 * Text is structured in paragraphs and nested lists, using notation that
  2803 is similar to Markdown. The control symbols for list items are as
  2804 follows:
  2805 
  2806   \<^item>  itemize
  2807   \<^enum>  enumerate
  2808   \<^descr>  description
  2809 
  2810 * There is a new short form for antiquotations with a single argument
  2811 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and
  2812 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}.
  2813 \<^name> without following cartouche is equivalent to @{name}. The
  2814 standard Isabelle fonts provide glyphs to render important control
  2815 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
  2816 
  2817 * Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with
  2818 corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using
  2819 standard LaTeX macros of the same names.
  2820 
  2821 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
  2822 Consequently, \<open>...\<close> without any decoration prints literal quasi-formal
  2823 text. Command-line tool "isabelle update_cartouches -t" helps to update
  2824 old sources, by approximative patching of the content of string and
  2825 cartouche tokens seen in theory sources.
  2826 
  2827 * The @{text} antiquotation now ignores the antiquotation option
  2828 "source". The given text content is output unconditionally, without any
  2829 surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the
  2830 argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial
  2831 or terminal spaces are ignored.
  2832 
  2833 * Antiquotations @{emph} and @{bold} output LaTeX source recursively,
  2834 adding appropriate text style markup. These may be used in the short
  2835 form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>.
  2836 
  2837 * Document antiquotation @{footnote} outputs LaTeX source recursively,
  2838 marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>.
  2839 
  2840 * Antiquotation @{verbatim [display]} supports option "indent".
  2841 
  2842 * Antiquotation @{theory_text} prints uninterpreted theory source text
  2843 (Isar outer syntax with command keywords etc.). This may be used in the
  2844 short form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent".
  2845 
  2846 * Antiquotation @{doc ENTRY} provides a reference to the given
  2847 documentation, with a hyperlink in the Prover IDE.
  2848 
  2849 * Antiquotations @{command}, @{method}, @{attribute} print checked
  2850 entities of the Isar language.
  2851 
  2852 * HTML presentation uses the standard IsabelleText font and Unicode
  2853 rendering of Isabelle symbols like Isabelle/Scala/jEdit.  The former
  2854 print mode "HTML" loses its special meaning.
  2855 
  2856 
  2857 *** Isar ***
  2858 
  2859 * Local goals ('have', 'show', 'hence', 'thus') allow structured rule
  2860 statements like fixes/assumes/shows in theorem specifications, but the
  2861 notation is postfix with keywords 'if' (or 'when') and 'for'. For
  2862 example:
  2863 
  2864   have result: "C x y"
  2865     if "A x" and "B y"
  2866     for x :: 'a and y :: 'a
  2867     <proof>
  2868 
  2869 The local assumptions are bound to the name "that". The result is
  2870 exported from context of the statement as usual. The above roughly
  2871 corresponds to a raw proof block like this:
  2872 
  2873   {
  2874     fix x :: 'a and y :: 'a
  2875     assume that: "A x" "B y"
  2876     have "C x y" <proof>
  2877   }
  2878   note result = this
  2879 
  2880 The keyword 'when' may be used instead of 'if', to indicate 'presume'
  2881 instead of 'assume' above.
  2882 
  2883 * Assumptions ('assume', 'presume') allow structured rule statements
  2884 using 'if' and 'for', similar to 'have' etc. above. For example:
  2885 
  2886   assume result: "C x y"
  2887     if "A x" and "B y"
  2888     for x :: 'a and y :: 'a
  2889 
  2890 This assumes "\<And>x y::'a. A x \<Longrightarrow> B y \<Longrightarrow> C x y" and produces a general
  2891 result as usual: "A ?x \<Longrightarrow> B ?y \<Longrightarrow> C ?x ?y".
  2892 
  2893 Vacuous quantification in assumptions is omitted, i.e. a for-context
  2894 only effects propositions according to actual use of variables. For
  2895 example:
  2896 
  2897   assume "A x" and "B y" for x and y
  2898 
  2899 is equivalent to:
  2900 
  2901   assume "\<And>x. A x" and "\<And>y. B y"
  2902 
  2903 * The meaning of 'show' with Pure rule statements has changed: premises
  2904 are treated in the sense of 'assume', instead of 'presume'. This means,
  2905 a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as
  2906 follows:
  2907 
  2908   show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
  2909 
  2910 or:
  2911 
  2912   show "C x" if "A x" "B x" for x
  2913 
  2914 Rare INCOMPATIBILITY, the old behaviour may be recovered as follows:
  2915 
  2916   show "C x" when "A x" "B x" for x
  2917 
  2918 * New command 'consider' states rules for generalized elimination and
  2919 case splitting. This is like a toplevel statement "theorem obtains" used
  2920 within a proof body; or like a multi-branch 'obtain' without activation
  2921 of the local context elements yet.
  2922 
  2923 * Proof method "cases" allows to specify the rule as first entry of
  2924 chained facts.  This is particularly useful with 'consider':
  2925 
  2926   consider (a) A | (b) B | (c) C <proof>
  2927   then have something
  2928   proof cases
  2929     case a
  2930     then show ?thesis <proof>
  2931   next
  2932     case b
  2933     then show ?thesis <proof>
  2934   next
  2935     case c
  2936     then show ?thesis <proof>
  2937   qed
  2938 
  2939 * Command 'case' allows fact name and attribute specification like this:
  2940 
  2941   case a: (c xs)
  2942   case a [attributes]: (c xs)
  2943 
  2944 Facts that are introduced by invoking the case context are uniformly
  2945 qualified by "a"; the same name is used for the cumulative fact. The old
  2946 form "case (c xs) [attributes]" is no longer supported. Rare
  2947 INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,
  2948 and always put attributes in front.
  2949 
  2950 * The standard proof method of commands 'proof' and '..' is now called
  2951 "standard" to make semantically clear what it is; the old name "default"
  2952 is still available as legacy for some time. Documentation now explains
  2953 '..' more accurately as "by standard" instead of "by rule".
  2954 
  2955 * Nesting of Isar goal structure has been clarified: the context after
  2956 the initial backwards refinement is retained for the whole proof, within
  2957 all its context sections (as indicated via 'next'). This is e.g.
  2958 relevant for 'using', 'including', 'supply':
  2959 
  2960   have "A \<and> A" if a: A for A
  2961     supply [simp] = a
  2962   proof
  2963     show A by simp
  2964   next
  2965     show A by simp
  2966   qed
  2967 
  2968 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the
  2969 proof body as well, abstracted over relevant parameters.
  2970 
  2971 * Improved type-inference for theorem statement 'obtains': separate
  2972 parameter scope for of each clause.
  2973 
  2974 * Term abbreviations via 'is' patterns also work for schematic
  2975 statements: result is abstracted over unknowns.
  2976 
  2977 * Command 'subgoal' allows to impose some structure on backward
  2978 refinements, to avoid proof scripts degenerating into long of 'apply'
  2979 sequences. Further explanations and examples are given in the isar-ref
  2980 manual.
  2981 
  2982 * Command 'supply' supports fact definitions during goal refinement
  2983 ('apply' scripts).
  2984 
  2985 * Proof method "goal_cases" turns the current subgoals into cases within
  2986 the context; the conclusion is bound to variable ?case in each case. For
  2987 example:
  2988 
  2989 lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
  2990   and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
  2991 proof goal_cases
  2992   case (1 x)
  2993   then show ?case using \<open>A x\<close> \<open>B x\<close> sorry
  2994 next
  2995   case (2 y z)
  2996   then show ?case using \<open>U y\<close> \<open>V z\<close> sorry
  2997 qed
  2998 
  2999 lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
  3000   and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
  3001 proof goal_cases
  3002   case prems: 1
  3003   then show ?case using prems sorry
  3004 next
  3005   case prems: 2
  3006   then show ?case using prems sorry
  3007 qed
  3008 
  3009 * The undocumented feature of implicit cases goal1, goal2, goal3, etc.
  3010 is marked as legacy, and will be removed eventually. The proof method
  3011 "goals" achieves a similar effect within regular Isar; often it can be
  3012 done more adequately by other means (e.g. 'consider').
  3013 
  3014 * The vacuous fact "TERM x" may be established "by fact" or as `TERM x`
  3015 as well, not just "by this" or "." as before.
  3016 
  3017 * Method "sleep" succeeds after a real-time delay (in seconds). This is
  3018 occasionally useful for demonstration and testing purposes.
  3019 
  3020 
  3021 *** Pure ***
  3022 
  3023 * Qualifiers in locale expressions default to mandatory ('!') regardless
  3024 of the command. Previously, for 'locale' and 'sublocale' the default was
  3025 optional ('?'). The old synatx '!' has been discontinued.
  3026 INCOMPATIBILITY, remove '!' and add '?' as required.
  3027 
  3028 * Keyword 'rewrites' identifies rewrite morphisms in interpretation
  3029 commands. Previously, the keyword was 'where'. INCOMPATIBILITY.
  3030 
  3031 * More gentle suppression of syntax along locale morphisms while
  3032 printing terms. Previously 'abbreviation' and 'notation' declarations
  3033 would be suppressed for morphisms except term identity. Now
  3034 'abbreviation' is also kept for morphims that only change the involved
  3035 parameters, and only 'notation' is suppressed. This can be of great help
  3036 when working with complex locale hierarchies, because proof states are
  3037 displayed much more succinctly. It also means that only notation needs
  3038 to be redeclared if desired, as illustrated by this example:
  3039 
  3040   locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65)
  3041   begin
  3042     definition derived (infixl "\<odot>" 65) where ...
  3043   end
  3044 
  3045   locale morphism =
  3046     left: struct composition + right: struct composition'
  3047     for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" 65)
  3048   begin
  3049     notation right.derived ("\<odot>''")
  3050   end
  3051 
  3052 * Command 'global_interpretation' issues interpretations into global
  3053 theories, with optional rewrite definitions following keyword 'defines'.
  3054 
  3055 * Command 'sublocale' accepts optional rewrite definitions after keyword
  3056 'defines'.
  3057 
  3058 * Command 'permanent_interpretation' has been discontinued. Use
  3059 'global_interpretation' or 'sublocale' instead. INCOMPATIBILITY.
  3060 
  3061 * Command 'print_definitions' prints dependencies of definitional
  3062 specifications. This functionality used to be part of 'print_theory'.
  3063 
  3064 * Configuration option rule_insts_schematic has been discontinued
  3065 (intermediate legacy feature in Isabelle2015). INCOMPATIBILITY.
  3066 
  3067 * Abbreviations in type classes now carry proper sort constraint. Rare
  3068 INCOMPATIBILITY in situations where the previous misbehaviour has been
  3069 exploited.
  3070 
  3071 * Refinement of user-space type system in type classes: pseudo-local
  3072 operations behave more similar to abbreviations. Potential
  3073 INCOMPATIBILITY in exotic situations.
  3074 
  3075 
  3076 *** HOL ***
  3077 
  3078 * The 'typedef' command has been upgraded from a partially checked
  3079 "axiomatization", to a full definitional specification that takes the
  3080 global collection of overloaded constant / type definitions into
  3081 account. Type definitions with open dependencies on overloaded
  3082 definitions need to be specified as "typedef (overloaded)". This
  3083 provides extra robustness in theory construction. Rare INCOMPATIBILITY.
  3084 
  3085 * Qualification of various formal entities in the libraries is done more
  3086 uniformly via "context begin qualified definition ... end" instead of
  3087 old-style "hide_const (open) ...". Consequently, both the defined
  3088 constant and its defining fact become qualified, e.g. Option.is_none and
  3089 Option.is_none_def. Occasional INCOMPATIBILITY in applications.
  3090 
  3091 * Some old and rarely used ASCII replacement syntax has been removed.
  3092 INCOMPATIBILITY, standard syntax with symbols should be used instead.
  3093 The subsequent commands help to reproduce the old forms, e.g. to
  3094 simplify porting old theories:
  3095 
  3096   notation iff  (infixr "<->" 25)
  3097 
  3098   notation Times  (infixr "<*>" 80)
  3099 
  3100   type_notation Map.map  (infixr "~=>" 0)
  3101   notation Map.map_comp  (infixl "o'_m" 55)
  3102 
  3103   type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21)
  3104 
  3105   notation FuncSet.funcset  (infixr "->" 60)
  3106   notation FuncSet.extensional_funcset  (infixr "->\<^sub>E" 60)
  3107 
  3108   notation Omega_Words_Fun.conc (infixr "conc" 65)
  3109 
  3110   notation Preorder.equiv ("op ~~")
  3111     and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50)
  3112 
  3113   notation (in topological_space) tendsto (infixr "--->" 55)
  3114   notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
  3115   notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
  3116 
  3117   notation NSA.approx (infixl "@=" 50)
  3118   notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)
  3119   notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
  3120 
  3121 * The alternative notation "\<Colon>" for type and sort constraints has been
  3122 removed: in LaTeX document output it looks the same as "::".
  3123 INCOMPATIBILITY, use plain "::" instead.
  3124 
  3125 * Commands 'inductive' and 'inductive_set' work better when names for
  3126 intro rules are omitted: the "cases" and "induct" rules no longer
  3127 declare empty case_names, but no case_names at all. This allows to use
  3128 numbered cases in proofs, without requiring method "goal_cases".
  3129 
  3130 * Inductive definitions ('inductive', 'coinductive', etc.) expose
  3131 low-level facts of the internal construction only if the option
  3132 "inductive_internals" is enabled. This refers to the internal predicate
  3133 definition and its monotonicity result. Rare INCOMPATIBILITY.
  3134 
  3135 * Recursive function definitions ('fun', 'function', 'partial_function')
  3136 expose low-level facts of the internal construction only if the option
  3137 "function_internals" is enabled. Its internal inductive definition is
  3138 also subject to "inductive_internals". Rare INCOMPATIBILITY.
  3139 
  3140 * BNF datatypes ('datatype', 'codatatype', etc.) expose low-level facts
  3141 of the internal construction only if the option "bnf_internals" is
  3142 enabled. This supersedes the former option "bnf_note_all". Rare
  3143 INCOMPATIBILITY.
  3144 
  3145 * Combinator to represent case distinction on products is named
  3146 "case_prod", uniformly, discontinuing any input aliasses. Very popular
  3147 theorem aliasses have been retained.
  3148 
  3149 Consolidated facts:
  3150   PairE ~> prod.exhaust
  3151   Pair_eq ~> prod.inject
  3152   pair_collapse ~> prod.collapse
  3153   Pair_fst_snd_eq ~> prod_eq_iff
  3154   split_twice ~> prod.case_distrib
  3155   split_weak_cong ~> prod.case_cong_weak
  3156   split_split ~> prod.split
  3157   split_split_asm ~> prod.split_asm
  3158   splitI ~> case_prodI
  3159   splitD ~> case_prodD
  3160   splitI2 ~> case_prodI2
  3161   splitI2' ~> case_prodI2'
  3162   splitE ~> case_prodE
  3163   splitE' ~> case_prodE'
  3164   split_pair ~> case_prod_Pair
  3165   split_eta ~> case_prod_eta
  3166   split_comp ~> case_prod_comp
  3167   mem_splitI ~> mem_case_prodI
  3168   mem_splitI2 ~> mem_case_prodI2
  3169   mem_splitE ~> mem_case_prodE
  3170   The_split ~> The_case_prod
  3171   cond_split_eta ~> cond_case_prod_eta
  3172   Collect_split_in_rel_leE ~> Collect_case_prod_in_rel_leE
  3173   Collect_split_in_rel_leI ~> Collect_case_prod_in_rel_leI
  3174   in_rel_Collect_split_eq ~> in_rel_Collect_case_prod_eq
  3175   Collect_split_Grp_eqD ~> Collect_case_prod_Grp_eqD
  3176   Collect_split_Grp_inD ~> Collect_case_prod_Grp_in
  3177   Domain_Collect_split ~> Domain_Collect_case_prod
  3178   Image_Collect_split ~> Image_Collect_case_prod
  3179   Range_Collect_split ~> Range_Collect_case_prod
  3180   Eps_split ~> Eps_case_prod
  3181   Eps_split_eq ~> Eps_case_prod_eq
  3182   split_rsp ~> case_prod_rsp
  3183   curry_split ~> curry_case_prod
  3184   split_curry ~> case_prod_curry
  3185 
  3186 Changes in structure HOLogic:
  3187   split_const ~> case_prod_const
  3188   mk_split ~> mk_case_prod
  3189   mk_psplits ~> mk_ptupleabs
  3190   strip_psplits ~> strip_ptupleabs
  3191 
  3192 INCOMPATIBILITY.
  3193 
  3194 * The coercions to type 'real' have been reorganised. The function
  3195 'real' is no longer overloaded, but has type 'nat => real' and
  3196 abbreviates of_nat for that type. Also 'real_of_int :: int => real'
  3197 abbreviates of_int for that type. Other overloaded instances of 'real'
  3198 have been replaced by 'real_of_ereal' and 'real_of_float'.
  3199 
  3200 Consolidated facts (among others):
  3201   real_of_nat_le_iff -> of_nat_le_iff
  3202   real_of_nat_numeral of_nat_numeral
  3203   real_of_int_zero of_int_0
  3204   real_of_nat_zero of_nat_0
  3205   real_of_one of_int_1
  3206   real_of_int_add of_int_add
  3207   real_of_nat_add of_nat_add
  3208   real_of_int_diff of_int_diff
  3209   real_of_nat_diff of_nat_diff
  3210   floor_subtract floor_diff_of_int
  3211   real_of_int_inject of_int_eq_iff
  3212   real_of_int_gt_zero_cancel_iff of_int_0_less_iff
  3213   real_of_int_ge_zero_cancel_iff of_int_0_le_iff
  3214   real_of_nat_ge_zero of_nat_0_le_iff
  3215   real_of_int_ceiling_ge le_of_int_ceiling
  3216   ceiling_less_eq ceiling_less_iff
  3217   ceiling_le_eq ceiling_le_iff
  3218   less_floor_eq less_floor_iff
  3219   floor_less_eq floor_less_iff
  3220   floor_divide_eq_div floor_divide_of_int_eq
  3221   real_of_int_zero_cancel of_nat_eq_0_iff
  3222   ceiling_real_of_int ceiling_of_int
  3223 
  3224 INCOMPATIBILITY.
  3225 
  3226 * Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has
  3227 been removed. INCOMPATIBILITY.
  3228 
  3229 * Quickcheck setup for finite sets.
  3230 
  3231 * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
  3232 
  3233 * Sledgehammer:
  3234   - The MaSh relevance filter has been sped up.
  3235   - Proof reconstruction has been improved, to minimize the incidence of
  3236     cases where Sledgehammer gives a proof that does not work.
  3237   - Auto Sledgehammer now minimizes and preplays the results.
  3238   - Handle Vampire 4.0 proof output without raising exception.
  3239   - Eliminated "MASH" environment variable. Use the "MaSh" option in
  3240     Isabelle/jEdit instead. INCOMPATIBILITY.
  3241   - Eliminated obsolete "blocking" option and related subcommands.
  3242 
  3243 * Nitpick:
  3244   - Fixed soundness bug in translation of "finite" predicate.
  3245   - Fixed soundness bug in "destroy_constrs" optimization.
  3246   - Fixed soundness bug in translation of "rat" type.
  3247   - Removed "check_potential" and "check_genuine" options.
  3248   - Eliminated obsolete "blocking" option.
  3249 
  3250 * (Co)datatype package:
  3251   - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
  3252     structure on the raw type to an abstract type defined using typedef.
  3253   - Always generate "case_transfer" theorem.
  3254   - For mutual types, generate slightly stronger "rel_induct",
  3255     "rel_coinduct", and "coinduct" theorems. INCOMPATIBILITY.
  3256   - Allow discriminators and selectors with the same name as the type
  3257     being defined.
  3258   - Avoid various internal name clashes (e.g., 'datatype f = f').
  3259 
  3260 * Transfer: new methods for interactive debugging of 'transfer' and
  3261 'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',
  3262 'transfer_prover_start' and 'transfer_prover_end'.
  3263 
  3264 * New diagnostic command print_record for displaying record definitions.
  3265 
  3266 * Division on integers is bootstrapped directly from division on
  3267 naturals and uses generic numeral algorithm for computations. Slight
  3268 INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes former
  3269 simprocs binary_int_div and binary_int_mod
  3270 
  3271 * Tightened specification of class semiring_no_zero_divisors. Minor
  3272 INCOMPATIBILITY.
  3273 
  3274 * Class algebraic_semidom introduces common algebraic notions of
  3275 integral (semi)domains, particularly units. Although logically subsumed
  3276 by fields, is is not a super class of these in order not to burden
  3277 fields with notions that are trivial there.
  3278 
  3279 * Class normalization_semidom specifies canonical representants for
  3280 equivalence classes of associated elements in an integral (semi)domain.
  3281 This formalizes associated elements as well.
  3282 
  3283 * Abstract specification of gcd/lcm operations in classes semiring_gcd,
  3284 semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute
  3285 and gcd_int.commute are subsumed by gcd.commute, as well as
  3286 gcd_nat.assoc and gcd_int.assoc by gcd.assoc.
  3287 
  3288 * Former constants Fields.divide (_ / _) and Divides.div (_ div _) are
  3289 logically unified to Rings.divide in syntactic type class Rings.divide,
  3290 with infix syntax (_ div _). Infix syntax (_ / _) for field division is
  3291 added later as abbreviation in class Fields.inverse. INCOMPATIBILITY,
  3292 instantiations must refer to Rings.divide rather than the former
  3293 separate constants, hence infix syntax (_ / _) is usually not available
  3294 during instantiation.
  3295 
  3296 * New cancellation simprocs for boolean algebras to cancel complementary
  3297 terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to
  3298 "top". INCOMPATIBILITY.
  3299 
  3300 * Class uniform_space introduces uniform spaces btw topological spaces
  3301 and metric spaces. Minor INCOMPATIBILITY: open_<type>_def needs to be
  3302 introduced in the form of an uniformity. Some constants are more general
  3303 now, it may be necessary to add type class constraints.
  3304 
  3305   open_real_def \<leadsto> open_dist
  3306   open_complex_def \<leadsto> open_dist
  3307 
  3308 * Library/Monad_Syntax: notation uses symbols \<bind> and \<then>. INCOMPATIBILITY.
  3309 
  3310 * Library/Multiset:
  3311   - Renamed multiset inclusion operators:
  3312       < ~> <#
  3313       > ~> >#
  3314       <= ~> <=#
  3315       >= ~> >=#
  3316       \<le> ~> \<le>#
  3317       \<ge> ~> \<ge>#
  3318     INCOMPATIBILITY.
  3319   - Added multiset inclusion operator syntax:
  3320       \<subset>#
  3321       \<subseteq>#
  3322       \<supset>#
  3323       \<supseteq>#
  3324   - "'a multiset" is no longer an instance of the "order",
  3325     "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",
  3326     "semilattice_inf", and "semilattice_sup" type classes. The theorems
  3327     previously provided by these type classes (directly or indirectly)
  3328     are now available through the "subset_mset" interpretation
  3329     (e.g. add_mono ~> subset_mset.add_mono).
  3330     INCOMPATIBILITY.
  3331   - Renamed conversions:
  3332       multiset_of ~> mset
  3333       multiset_of_set ~> mset_set
  3334       set_of ~> set_mset
  3335     INCOMPATIBILITY
  3336   - Renamed lemmas:
  3337       mset_le_def ~> subseteq_mset_def
  3338       mset_less_def ~> subset_mset_def
  3339       less_eq_multiset.rep_eq ~> subseteq_mset_def
  3340     INCOMPATIBILITY
  3341   - Removed lemmas generated by lift_definition:
  3342     less_eq_multiset.abs_eq, less_eq_multiset.rsp,
  3343     less_eq_multiset.transfer, less_eq_multiset_def
  3344     INCOMPATIBILITY
  3345 
  3346 * Library/Omega_Words_Fun: Infinite words modeled as functions nat \<Rightarrow> 'a.
  3347 
  3348 * Library/Bourbaki_Witt_Fixpoint: Added formalisation of the
  3349 Bourbaki-Witt fixpoint theorem for increasing functions in
  3350 chain-complete partial orders.
  3351 
  3352 * Library/Old_Recdef: discontinued obsolete 'defer_recdef' command.
  3353 Minor INCOMPATIBILITY, use 'function' instead.
  3354 
  3355 * Library/Periodic_Fun: a locale that provides convenient lemmas for
  3356 periodic functions.
  3357 
  3358 * Library/Formal_Power_Series: proper definition of division (with
  3359 remainder) for formal power series; instances for Euclidean Ring and
  3360 GCD.
  3361 
  3362 * HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
  3363 
  3364 * HOL-Statespace: command 'statespace' uses mandatory qualifier for
  3365 import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
  3366 remove '!' and add '?' as required.
  3367 
  3368 * HOL-Decision_Procs: The "approximation" method works with "powr"
  3369 (exponentiation on real numbers) again.
  3370 
  3371 * HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm with Contour
  3372 integrals (= complex path integrals), Cauchy's integral theorem, winding
  3373 numbers and Cauchy's integral formula, Liouville theorem, Fundamental
  3374 Theorem of Algebra. Ported from HOL Light.
  3375 
  3376 * HOL-Multivariate_Analysis: topological concepts such as connected
  3377 components, homotopic paths and the inside or outside of a set.
  3378 
  3379 * HOL-Multivariate_Analysis: radius of convergence of power series and
  3380 various summability tests; Harmonic numbers and the Euler–Mascheroni
  3381 constant; the Generalised Binomial Theorem; the complex and real
  3382 Gamma/log-Gamma/Digamma/ Polygamma functions and their most important
  3383 properties.
  3384 
  3385 * HOL-Probability: The central limit theorem based on Levy's uniqueness
  3386 and continuity theorems, weak convergence, and characterisitc functions.
  3387 
  3388 * HOL-Data_Structures: new and growing session of standard data
  3389 structures.
  3390 
  3391 
  3392 *** ML ***
  3393 
  3394 * The following combinators for low-level profiling of the ML runtime
  3395 system are available:
  3396 
  3397   profile_time          (*CPU time*)
  3398   profile_time_thread   (*CPU time on this thread*)
  3399   profile_allocations   (*overall heap allocations*)
  3400 
  3401 * Antiquotation @{undefined} or \<^undefined> inlines (raise Match).
  3402 
  3403 * Antiquotation @{method NAME} inlines the (checked) name of the given
  3404 Isar proof method.
  3405 
  3406 * Pretty printing of Poly/ML compiler output in Isabelle has been
  3407 improved: proper treatment of break offsets and blocks with consistent
  3408 breaks.
  3409 
  3410 * The auxiliary module Pure/display.ML has been eliminated. Its
  3411 elementary thm print operations are now in Pure/more_thm.ML and thus
  3412 called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.
  3413 
  3414 * Simproc programming interfaces have been simplified:
  3415 Simplifier.make_simproc and Simplifier.define_simproc supersede various
  3416 forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that
  3417 term patterns for the left-hand sides are specified with implicitly
  3418 fixed variables, like top-level theorem statements. INCOMPATIBILITY.
  3419 
  3420 * Instantiation rules have been re-organized as follows:
  3421 
  3422   Thm.instantiate  (*low-level instantiation with named arguments*)
  3423   Thm.instantiate' (*version with positional arguments*)
  3424 
  3425   Drule.infer_instantiate  (*instantiation with type inference*)
  3426   Drule.infer_instantiate'  (*version with positional arguments*)
  3427 
  3428 The LHS only requires variable specifications, instead of full terms.
  3429 Old cterm_instantiate is superseded by infer_instantiate.
  3430 INCOMPATIBILITY, need to re-adjust some ML names and types accordingly.
  3431 
  3432 * Old tactic shorthands atac, rtac, etac, dtac, ftac have been
  3433 discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
  3434 instead (with proper context).
  3435 
  3436 * Thm.instantiate (and derivatives) no longer require the LHS of the
  3437 instantiation to be certified: plain variables are given directly.
  3438 
  3439 * Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous
  3440 quasi-bound variables (like the Simplifier), instead of accidentally
  3441 named local fixes. This has the potential to improve stability of proof
  3442 tools, but can also cause INCOMPATIBILITY for tools that don't observe
  3443 the proof context discipline.
  3444 
  3445 * Isar proof methods are based on a slightly more general type
  3446 context_tactic, which allows to change the proof context dynamically
  3447 (e.g. to update cases) and indicate explicit Seq.Error results. Former
  3448 METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are
  3449 provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY.
  3450 
  3451 
  3452 *** System ***
  3453 
  3454 * Command-line tool "isabelle console" enables print mode "ASCII".
  3455 
  3456 * Command-line tool "isabelle update_then" expands old Isar command
  3457 conflations:
  3458 
  3459     hence  ~>  then have
  3460     thus   ~>  then show
  3461 
  3462 This syntax is more orthogonal and improves readability and
  3463 maintainability of proofs.
  3464 
  3465 * Global session timeout is multiplied by timeout_scale factor. This
  3466 allows to adjust large-scale tests (e.g. AFP) to overall hardware
  3467 performance.
  3468 
  3469 * Property values in etc/symbols may contain spaces, if written with the
  3470 replacement character "␣" (Unicode point 0x2324). For example:
  3471 
  3472     \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono
  3473 
  3474 * Java runtime environment for x86_64-windows allows to use larger heap
  3475 space.
  3476 
  3477 * Java runtime options are determined separately for 32bit vs. 64bit
  3478 platforms as follows.
  3479 
  3480   - Isabelle desktop application: platform-specific files that are
  3481     associated with the main app bundle
  3482 
  3483   - isabelle jedit: settings
  3484     JEDIT_JAVA_SYSTEM_OPTIONS
  3485     JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64
  3486 
  3487   - isabelle build: settings
  3488     ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64
  3489 
  3490 * Bash shell function "jvmpath" has been renamed to "platform_path": it
  3491 is relevant both for Poly/ML and JVM processes.
  3492 
  3493 * Poly/ML default platform architecture may be changed from 32bit to
  3494 64bit via system option ML_system_64. A system restart (and rebuild) is
  3495 required after change.
  3496 
  3497 * Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which
  3498 both allow larger heap space than former x86-cygwin.
  3499 
  3500 * Heap images are 10-15% smaller due to less wasteful persistent theory
  3501 content (using ML type theory_id instead of theory);
  3502 
  3503 
  3504 
  3505 New in Isabelle2015 (May 2015)
  3506 ------------------------------
  3507 
  3508 *** General ***
  3509 
  3510 * Local theory specification commands may have a 'private' or
  3511 'qualified' modifier to restrict name space accesses to the local scope,
  3512 as provided by some "context begin ... end" block. For example:
  3513 
  3514   context
  3515   begin
  3516 
  3517   private definition ...
  3518   private lemma ...
  3519 
  3520   qualified definition ...
  3521   qualified lemma ...
  3522 
  3523   lemma ...
  3524   theorem ...
  3525 
  3526   end
  3527 
  3528 * Command 'experiment' opens an anonymous locale context with private
  3529 naming policy.
  3530 
  3531 * Command 'notepad' requires proper nesting of begin/end and its proof
  3532 structure in the body: 'oops' is no longer supported here. Minor
  3533 INCOMPATIBILITY, use 'sorry' instead.
  3534 
  3535 * Command 'named_theorems' declares a dynamic fact within the context,
  3536 together with an attribute to maintain the content incrementally. This
  3537 supersedes functor Named_Thms in Isabelle/ML, but with a subtle change
  3538 of semantics due to external visual order vs. internal reverse order.
  3539 
  3540 * 'find_theorems': search patterns which are abstractions are
  3541 schematically expanded before search. Search results match the naive
  3542 expectation more closely, particularly wrt. abbreviations.
  3543 INCOMPATIBILITY.
  3544 
  3545 * Commands 'method_setup' and 'attribute_setup' now work within a local
  3546 theory context.
  3547 
  3548 * Outer syntax commands are managed authentically within the theory
  3549 context, without implicit global state. Potential for accidental
  3550 INCOMPATIBILITY, make sure that required theories are really imported.
  3551 
  3552 * Historical command-line terminator ";" is no longer accepted (and
  3553 already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle
  3554 update_semicolons" to remove obsolete semicolons from old theory
  3555 sources.
  3556 
  3557 * Structural composition of proof methods (meth1; meth2) in Isar
  3558 corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
  3559 
  3560 * The Eisbach proof method language allows to define new proof methods
  3561 by combining existing ones with their usual syntax. The "match" proof
  3562 method provides basic fact/term matching in addition to
  3563 premise/conclusion matching through Subgoal.focus, and binds fact names
  3564 from matches as well as term patterns within matches. The Isabelle
  3565 documentation provides an entry "eisbach" for the Eisbach User Manual.
  3566 Sources and various examples are in ~~/src/HOL/Eisbach/.
  3567 
  3568 
  3569 *** Prover IDE -- Isabelle/Scala/jEdit ***
  3570 
  3571 * Improved folding mode "isabelle" based on Isar syntax. Alternatively,
  3572 the "sidekick" mode may be used for document structure.
  3573 
  3574 * Extended bracket matching based on Isar language structure. System
  3575 option jedit_structure_limit determines maximum number of lines to scan
  3576 in the buffer.
  3577 
  3578 * Support for BibTeX files: context menu, context-sensitive token
  3579 marker, SideKick parser.
  3580 
  3581 * Document antiquotation @{cite} provides formal markup, which is
  3582 interpreted semi-formally based on .bib files that happen to be open in
  3583 the editor (hyperlinks, completion etc.).
  3584 
  3585 * Less waste of vertical space via negative line spacing (see Global
  3586 Options / Text Area).
  3587 
  3588 * Improved graphview panel with optional output of PNG or PDF, for
  3589 display of 'thy_deps', 'class_deps' etc.
  3590 
  3591 * The commands 'thy_deps' and 'class_deps' allow optional bounds to
  3592 restrict the visualized hierarchy.
  3593 
  3594 * Improved scheduling for asynchronous print commands (e.g. provers
  3595 managed by the Sledgehammer panel) wrt. ongoing document processing.
  3596 
  3597 
  3598 *** Document preparation ***
  3599 
  3600 * Document markup commands 'chapter', 'section', 'subsection',
  3601 'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any
  3602 context, even before the initial 'theory' command. Obsolete proof
  3603 commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been
  3604 discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw'
  3605 instead. The old 'header' command is still retained for some time, but
  3606 should be replaced by 'chapter', 'section' etc. (using "isabelle
  3607 update_header"). Minor INCOMPATIBILITY.
  3608 
  3609 * Official support for "tt" style variants, via \isatt{...} or
  3610 \begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
  3611 verbatim environment of LaTeX is no longer used. This allows @{ML} etc.
  3612 as argument to other macros (such as footnotes).
  3613 
  3614 * Document antiquotation @{verbatim} prints ASCII text literally in "tt"
  3615 style.
  3616 
  3617 * Discontinued obsolete option "document_graph": session_graph.pdf is
  3618 produced unconditionally for HTML browser_info and PDF-LaTeX document.
  3619 
  3620 * Diagnostic commands and document markup commands within a proof do not
  3621 affect the command tag for output. Thus commands like 'thm' are subject
  3622 to proof document structure, and no longer "stick out" accidentally.
  3623 Commands 'text' and 'txt' merely differ in the LaTeX style, not their
  3624 tags. Potential INCOMPATIBILITY in exotic situations.
  3625 
  3626 * System option "pretty_margin" is superseded by "thy_output_margin",
  3627 which is also accessible via document antiquotation option "margin".
  3628 Only the margin for document output may be changed, but not the global
  3629 pretty printing: that is 76 for plain console output, and adapted
  3630 dynamically in GUI front-ends. Implementations of document
  3631 antiquotations need to observe the margin explicitly according to
  3632 Thy_Output.string_of_margin. Minor INCOMPATIBILITY.
  3633 
  3634 * Specification of 'document_files' in the session ROOT file is
  3635 mandatory for document preparation. The legacy mode with implicit
  3636 copying of the document/ directory is no longer supported. Minor
  3637 INCOMPATIBILITY.
  3638 
  3639 
  3640 *** Pure ***
  3641 
  3642 * Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
  3643 etc.) allow an optional context of local variables ('for' declaration):
  3644 these variables become schematic in the instantiated theorem; this
  3645 behaviour is analogous to 'for' in attributes "where" and "of".
  3646 Configuration option rule_insts_schematic (default false) controls use
  3647 of schematic variables outside the context. Minor INCOMPATIBILITY,
  3648 declare rule_insts_schematic = true temporarily and update to use local
  3649 variable declarations or dummy patterns instead.
  3650 
  3651 * Explicit instantiation via attributes "where", "of", and proof methods
  3652 "rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
  3653 ("_") that stand for anonymous local variables.
  3654 
  3655 * Generated schematic variables in standard format of exported facts are
  3656 incremented to avoid material in the proof context. Rare
  3657 INCOMPATIBILITY, explicit instantiation sometimes needs to refer to
  3658 different index.
  3659 
  3660 * Lexical separation of signed and unsigned numerals: categories "num"
  3661 and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence
  3662 of numeral signs, particularly in expressions involving infix syntax
  3663 like "(- 1) ^ n".
  3664 
  3665 * Old inner token category "xnum" has been discontinued.  Potential
  3666 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num"
  3667 token category instead.
  3668 
  3669 
  3670 *** HOL ***
  3671 
  3672 * New (co)datatype package:
  3673   - The 'datatype_new' command has been renamed 'datatype'. The old
  3674     command of that name is now called 'old_datatype' and is provided
  3675     by "~~/src/HOL/Library/Old_Datatype.thy". See
  3676     'isabelle doc datatypes' for information on porting.
  3677     INCOMPATIBILITY.
  3678   - Renamed theorems:
  3679       disc_corec ~> corec_disc
  3680       disc_corec_iff ~> corec_disc_iff
  3681       disc_exclude ~> distinct_disc
  3682       disc_exhaust ~> exhaust_disc
  3683       disc_map_iff ~> map_disc_iff
  3684       sel_corec ~> corec_sel
  3685       sel_exhaust ~> exhaust_sel
  3686       sel_map ~> map_sel
  3687       sel_set ~> set_sel
  3688       sel_split ~> split_sel
  3689       sel_split_asm ~> split_sel_asm
  3690       strong_coinduct ~> coinduct_strong
  3691       weak_case_cong ~> case_cong_weak
  3692     INCOMPATIBILITY.
  3693   - The "no_code" option to "free_constructors", "datatype_new", and
  3694     "codatatype" has been renamed "plugins del: code".
  3695     INCOMPATIBILITY.
  3696   - The rules "set_empty" have been removed. They are easy
  3697     consequences of other set rules "by auto".
  3698     INCOMPATIBILITY.
  3699   - The rule "set_cases" is now registered with the "[cases set]"
  3700     attribute. This can influence the behavior of the "cases" proof
  3701     method when more than one case rule is applicable (e.g., an
  3702     assumption is of the form "w : set ws" and the method "cases w"
  3703     is invoked). The solution is to specify the case rule explicitly
  3704     (e.g. "cases w rule: widget.exhaust").
  3705     INCOMPATIBILITY.
  3706   - Renamed theories:
  3707       BNF_Comp ~> BNF_Composition
  3708       BNF_FP_Base ~> BNF_Fixpoint_Base
  3709       BNF_GFP ~> BNF_Greatest_Fixpoint
  3710       BNF_LFP ~> BNF_Least_Fixpoint
  3711       BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions
  3712       Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions
  3713     INCOMPATIBILITY.
  3714   - Lifting and Transfer setup for basic HOL types sum and prod (also
  3715     option) is now performed by the BNF package. Theories Lifting_Sum,
  3716     Lifting_Product and Lifting_Option from Main became obsolete and
  3717     were removed. Changed definitions of the relators rel_prod and
  3718     rel_sum (using inductive).
  3719     INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead
  3720     of rel_prod_def and rel_sum_def.
  3721     Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names
  3722     changed (e.g. map_prod_transfer ~> prod.map_transfer).
  3723   - Parametricity theorems for map functions, relators, set functions,
  3724     constructors, case combinators, discriminators, selectors and
  3725     (co)recursors are automatically proved and registered as transfer
  3726     rules.
  3727 
  3728 * Old datatype package:
  3729   - The old 'datatype' command has been renamed 'old_datatype', and
  3730     'rep_datatype' has been renamed 'old_rep_datatype'. They are
  3731     provided by "~~/src/HOL/Library/Old_Datatype.thy". See
  3732     'isabelle doc datatypes' for information on porting.
  3733     INCOMPATIBILITY.
  3734   - Renamed theorems:
  3735       weak_case_cong ~> case_cong_weak
  3736     INCOMPATIBILITY.
  3737   - Renamed theory:
  3738       ~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy
  3739     INCOMPATIBILITY.
  3740 
  3741 * Nitpick:
  3742   - Fixed soundness bug related to the strict and non-strict subset
  3743     operations.
  3744 
  3745 * Sledgehammer:
  3746   - CVC4 is now included with Isabelle instead of CVC3 and run by
  3747     default.
  3748   - Z3 is now always enabled by default, now that it is fully open
  3749     source. The "z3_non_commercial" option is discontinued.
  3750   - Minimization is now always enabled by default.
  3751     Removed sub-command:
  3752       min
  3753   - Proof reconstruction, both one-liners and Isar, has been
  3754     dramatically improved.
  3755   - Improved support for CVC4 and veriT.
  3756 
  3757 * Old and new SMT modules:
  3758   - The old 'smt' method has been renamed 'old_smt' and moved to
  3759     'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility,
  3760     until applications have been ported to use the new 'smt' method. For
  3761     the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must
  3762     be installed, and the environment variable "OLD_Z3_SOLVER" must
  3763     point to it.
  3764     INCOMPATIBILITY.
  3765   - The 'smt2' method has been renamed 'smt'.
  3766     INCOMPATIBILITY.
  3767   - New option 'smt_reconstruction_step_timeout' to limit the
  3768     reconstruction time of Z3 proof steps in the new 'smt' method.
  3769   - New option 'smt_statistics' to display statistics of the new 'smt'
  3770     method, especially runtime statistics of Z3 proof reconstruction.
  3771 
  3772 * Lifting: command 'lift_definition' allows to execute lifted constants
  3773 that have as a return type a datatype containing a subtype. This
  3774 overcomes long-time limitations in the area of code generation and
  3775 lifting, and avoids tedious workarounds.
  3776 
  3777 * Command and antiquotation "value" provide different evaluation slots
  3778 (again), where the previous strategy (NBE after ML) serves as default.
  3779 Minor INCOMPATIBILITY.
  3780 
  3781 * Add NO_MATCH-simproc, allows to check for syntactic non-equality.
  3782 
  3783 * field_simps: Use NO_MATCH-simproc for distribution rules, to avoid
  3784 non-termination in case of distributing a division. With this change
  3785 field_simps is in some cases slightly less powerful, if it fails try to
  3786 add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY.
  3787 
  3788 * Separate class no_zero_divisors has been given up in favour of fully
  3789 algebraic semiring_no_zero_divisors. INCOMPATIBILITY.
  3790 
  3791 * Class linordered_semidom really requires no zero divisors.
  3792 INCOMPATIBILITY.
  3793 
  3794 * Classes division_ring, field and linordered_field always demand
  3795 "inverse 0 = 0". Given up separate classes division_ring_inverse_zero,
  3796 field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY.
  3797 
  3798 * Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit
  3799 additive inverse operation. INCOMPATIBILITY.
  3800 
  3801 * Complex powers and square roots. The functions "ln" and "powr" are now
  3802 overloaded for types real and complex, and 0 powr y = 0 by definition.
  3803 INCOMPATIBILITY: type constraints may be necessary.
  3804 
  3805 * The functions "sin" and "cos" are now defined for any type of sort
  3806 "{real_normed_algebra_1,banach}" type, so in particular on "real" and
  3807 "complex" uniformly. Minor INCOMPATIBILITY: type constraints may be
  3808 needed.
  3809 
  3810 * New library of properties of the complex transcendental functions sin,
  3811 cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light.
  3812 
  3813 * The factorial function, "fact", now has type "nat => 'a" (of a sort
  3814 that admits numeric types including nat, int, real and complex.
  3815 INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type
  3816 constraint, and the combination "real (fact k)" is likely to be
  3817 unsatisfactory. If a type conversion is still necessary, then use
  3818 "of_nat (fact k)" or "real_of_nat (fact k)".
  3819 
  3820 * Removed functions "natfloor" and "natceiling", use "nat o floor" and
  3821 "nat o ceiling" instead. A few of the lemmas have been retained and
  3822 adapted: in their names "natfloor"/"natceiling" has been replaced by
  3823 "nat_floor"/"nat_ceiling".
  3824 
  3825 * Qualified some duplicated fact names required for boostrapping the
  3826 type class hierarchy:
  3827   ab_add_uminus_conv_diff ~> diff_conv_add_uminus
  3828   field_inverse_zero ~> inverse_zero
  3829   field_divide_inverse ~> divide_inverse
  3830   field_inverse ~> left_inverse
  3831 Minor INCOMPATIBILITY.
  3832 
  3833 * Eliminated fact duplicates:
  3834   mult_less_imp_less_right ~> mult_right_less_imp_less
  3835   mult_less_imp_less_left ~> mult_left_less_imp_less
  3836 Minor INCOMPATIBILITY.
  3837 
  3838 * Fact consolidation: even_less_0_iff is subsumed by
  3839 double_add_less_zero_iff_single_add_less_zero (simp by default anyway).
  3840 
  3841 * Generalized and consolidated some theorems concerning divsibility:
  3842   dvd_reduce ~> dvd_add_triv_right_iff
  3843   dvd_plus_eq_right ~> dvd_add_right_iff
  3844   dvd_plus_eq_left ~> dvd_add_left_iff
  3845 Minor INCOMPATIBILITY.
  3846 
  3847 * "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _"
  3848 and part of theory Main.
  3849   even_def ~> even_iff_mod_2_eq_zero
  3850 INCOMPATIBILITY.
  3851 
  3852 * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor
  3853 INCOMPATIBILITY.
  3854 
  3855 * Bootstrap of listsum as special case of abstract product over lists.
  3856 Fact rename:
  3857     listsum_def ~> listsum.eq_foldr
  3858 INCOMPATIBILITY.
  3859 
  3860 * Product over lists via constant "listprod".
  3861 
  3862 * Theory List: renamed drop_Suc_conv_tl and nth_drop' to
  3863 Cons_nth_drop_Suc.
  3864 
  3865 * New infrastructure for compiling, running, evaluating and testing
  3866 generated code in target languages in HOL/Library/Code_Test. See
  3867 HOL/Codegenerator_Test/Code_Test* for examples.
  3868 
  3869 * Library/Multiset:
  3870   - Introduced "replicate_mset" operation.
  3871   - Introduced alternative characterizations of the multiset ordering in
  3872     "Library/Multiset_Order".
  3873   - Renamed multiset ordering:
  3874       <# ~> #<#
  3875       <=# ~> #<=#
  3876       \<subset># ~> #\<subset>#
  3877       \<subseteq># ~> #\<subseteq>#
  3878     INCOMPATIBILITY.
  3879   - Introduced abbreviations for ill-named multiset operations:
  3880       <#, \<subset># abbreviate < (strict subset)
  3881       <=#, \<le>#, \<subseteq># abbreviate <= (subset or equal)
  3882     INCOMPATIBILITY.
  3883   - Renamed
  3884       in_multiset_of ~> in_multiset_in_set
  3885       Multiset.fold ~> fold_mset
  3886       Multiset.filter ~> filter_mset
  3887     INCOMPATIBILITY.
  3888   - Removed mcard, is equal to size.
  3889   - Added attributes:
  3890       image_mset.id [simp]
  3891       image_mset_id [simp]
  3892       elem_multiset_of_set [simp, intro]
  3893       comp_fun_commute_plus_mset [simp]
  3894       comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp]
  3895       in_mset_fold_plus_iff [iff]
  3896       set_of_Union_mset [simp]
  3897       in_Union_mset_iff [iff]
  3898     INCOMPATIBILITY.
  3899 
  3900 * Library/Sum_of_Squares: simplified and improved "sos" method. Always
  3901 use local CSDP executable, which is much faster than the NEOS server.
  3902 The "sos_cert" functionality is invoked as "sos" with additional
  3903 argument. Minor INCOMPATIBILITY.
  3904 
  3905 * HOL-Decision_Procs: New counterexample generator quickcheck
  3906 [approximation] for inequalities of transcendental functions. Uses
  3907 hardware floating point arithmetic to randomly discover potential
  3908 counterexamples. Counterexamples are certified with the "approximation"
  3909 method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
  3910 examples.
  3911 
  3912 * HOL-Probability: Reworked measurability prover
  3913   - applies destructor rules repeatedly
  3914   - removed application splitting (replaced by destructor rule)
  3915   - added congruence rules to rewrite measure spaces under the sets
  3916     projection
  3917 
  3918 * New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for
  3919 single-step rewriting with subterm selection based on patterns.
  3920 
  3921 
  3922 *** ML ***
  3923 
  3924 * Subtle change of name space policy: undeclared entries are now
  3925 considered inaccessible, instead of accessible via the fully-qualified
  3926 internal name. This mainly affects Name_Space.intern (and derivatives),
  3927 which may produce an unexpected Long_Name.hidden prefix. Note that
  3928 contemporary applications use the strict Name_Space.check (and
  3929 derivatives) instead, which is not affected by the change. Potential
  3930 INCOMPATIBILITY in rare applications of Name_Space.intern.
  3931 
  3932 * Subtle change of error semantics of Toplevel.proof_of: regular user
  3933 ERROR instead of internal Toplevel.UNDEF.
  3934 
  3935 * Basic combinators map, fold, fold_map, split_list, apply are available
  3936 as parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
  3937 
  3938 * Renamed "pairself" to "apply2", in accordance to @{apply 2}.
  3939 INCOMPATIBILITY.
  3940 
  3941 * Former combinators NAMED_CRITICAL and CRITICAL for central critical
  3942 sections have been discontinued, in favour of the more elementary
  3943 Multithreading.synchronized and its high-level derivative
  3944 Synchronized.var (which is usually sufficient in applications). Subtle
  3945 INCOMPATIBILITY: synchronized access needs to be atomic and cannot be
  3946 nested.
  3947 
  3948 * Synchronized.value (ML) is actually synchronized (as in Scala): subtle
  3949 change of semantics with minimal potential for INCOMPATIBILITY.
  3950 
  3951 * The main operations to certify logical entities are Thm.ctyp_of and
  3952 Thm.cterm_of with a local context; old-style global theory variants are
  3953 available as Thm.global_ctyp_of and Thm.global_cterm_of.
  3954 INCOMPATIBILITY.
  3955 
  3956 * Elementary operations in module Thm are no longer pervasive.
  3957 INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of,
  3958 Thm.term_of etc.
  3959 
  3960 * Proper context for various elementary tactics: assume_tac,
  3961 resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac,
  3962 compose_tac, Splitter.split_tac etc. INCOMPATIBILITY.
  3963 
  3964 * Tactical PARALLEL_ALLGOALS is the most common way to refer to
  3965 PARALLEL_GOALS.
  3966 
  3967 * Goal.prove_multi is superseded by the fully general Goal.prove_common,
  3968 which also allows to specify a fork priority.
  3969 
  3970 * Antiquotation @{command_spec "COMMAND"} is superseded by
  3971 @{command_keyword COMMAND} (usually without quotes and with PIDE
  3972 markup). Minor INCOMPATIBILITY.
  3973 
  3974 * Cartouches within ML sources are turned into values of type
  3975 Input.source (with formal position information).
  3976 
  3977 
  3978 *** System ***
  3979 
  3980 * The Isabelle tool "update_cartouches" changes theory files to use
  3981 cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
  3982 
  3983 * The Isabelle tool "build" provides new options -X, -k, -x.
  3984 
  3985 * Discontinued old-fashioned "codegen" tool. Code generation can always
  3986 be externally triggered using an appropriate ROOT file plus a
  3987 corresponding theory. Parametrization is possible using environment
  3988 variables, or ML snippets in the most extreme cases. Minor
  3989 INCOMPATIBILITY.
  3990 
  3991 * JVM system property "isabelle.threads" determines size of Scala thread
  3992 pool, like Isabelle system option "threads" for ML.
  3993 
  3994 * JVM system property "isabelle.laf" determines the default Swing
  3995 look-and-feel, via internal class name or symbolic name as in the jEdit
  3996 menu Global Options / Appearance.
  3997 
  3998 * Support for Proof General and Isar TTY loop has been discontinued.
  3999 Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.
  4000 
  4001 
  4002 
  4003 New in Isabelle2014 (August 2014)
  4004 ---------------------------------
  4005 
  4006 *** General ***
  4007 
  4008 * Support for official Standard ML within the Isabelle context.
  4009 Command 'SML_file' reads and evaluates the given Standard ML file.
  4010 Toplevel bindings are stored within the theory context; the initial
  4011 environment is restricted to the Standard ML implementation of
  4012 Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'
  4013 and 'SML_export' allow to exchange toplevel bindings between the two
  4014 separate environments.  See also ~~/src/Tools/SML/Examples.thy for
  4015 some examples.
  4016 
  4017 * Standard tactics and proof methods such as "clarsimp", "auto" and
  4018 "safe" now preserve equality hypotheses "x = expr" where x is a free
  4019 variable.  Locale assumptions and chained facts containing "x"
  4020 continue to be useful.  The new method "hypsubst_thin" and the
  4021 configuration option "hypsubst_thin" (within the attribute name space)
  4022 restore the previous behavior.  INCOMPATIBILITY, especially where
  4023 induction is done after these methods or when the names of free and
  4024 bound variables clash.  As first approximation, old proofs may be
  4025 repaired by "using [[hypsubst_thin = true]]" in the critical spot.
  4026 
  4027 * More static checking of proof methods, which allows the system to
  4028 form a closure over the concrete syntax.  Method arguments should be
  4029 processed in the original proof context as far as possible, before
  4030 operating on the goal state.  In any case, the standard discipline for
  4031 subgoal-addressing needs to be observed: no subgoals or a subgoal
  4032 number that is out of range produces an empty result sequence, not an
  4033 exception.  Potential INCOMPATIBILITY for non-conformant tactical
  4034 proof tools.
  4035 
  4036 * Lexical syntax (inner and outer) supports text cartouches with
  4037 arbitrary nesting, and without escapes of quotes etc.  The Prover IDE
  4038 supports input via ` (backquote).
  4039 
  4040 * The outer syntax categories "text" (for formal comments and document
  4041 markup commands) and "altstring" (for literal fact references) allow
  4042 cartouches as well, in addition to the traditional mix of quotations.
  4043 
  4044 * Syntax of document antiquotation @{rail} now uses \<newline> instead
  4045 of "\\", to avoid the optical illusion of escaped backslash within
  4046 string token.  General renovation of its syntax using text cartouches.
  4047 Minor INCOMPATIBILITY.
  4048 
  4049 * Discontinued legacy_isub_isup, which was a temporary workaround for
  4050 Isabelle/ML in Isabelle2013-1.  The prover process no longer accepts
  4051 old identifier syntax with \<^isub> or \<^isup>.  Potential
  4052 INCOMPATIBILITY.
  4053 
  4054 * Document antiquotation @{url} produces markup for the given URL,
  4055 which results in an active hyperlink within the text.
  4056 
  4057 * Document antiquotation @{file_unchecked} is like @{file}, but does
  4058 not check existence within the file-system.
  4059 
  4060 * Updated and extended manuals: codegen, datatypes, implementation,
  4061 isar-ref, jedit, system.
  4062 
  4063 
  4064 *** Prover IDE -- Isabelle/Scala/jEdit ***
  4065 
  4066 * Improved Document panel: simplified interaction where every single
  4067 mouse click (re)opens document via desktop environment or as jEdit
  4068 buffer.
  4069 
  4070 * Support for Navigator plugin (with toolbar buttons), with connection
  4071 to PIDE hyperlinks.
  4072 
  4073 * Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
  4074 Open text buffers take precedence over copies within the file-system.
  4075 
  4076 * Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
  4077 auxiliary ML files.
  4078 
  4079 * Improved syntactic and semantic completion mechanism, with simple
  4080 templates, completion language context, name-space completion,
  4081 file-name completion, spell-checker completion.
  4082 
  4083 * Refined GUI popup for completion: more robust key/mouse event
  4084 handling and propagation to enclosing text area -- avoid loosing
  4085 keystrokes with slow / remote graphics displays.
  4086 
  4087 * Completion popup supports both ENTER and TAB (default) to select an
  4088 item, depending on Isabelle options.
  4089 
  4090 * Refined insertion of completion items wrt. jEdit text: multiple
  4091 selections, rectangular selections, rectangular selection as "tall
  4092 caret".
  4093 
  4094 * Integrated spell-checker for document text, comments etc. with
  4095 completion popup and context-menu.
  4096 
  4097 * More general "Query" panel supersedes "Find" panel, with GUI access
  4098 to commands 'find_theorems' and 'find_consts', as well as print
  4099 operations for the context.  Minor incompatibility in keyboard
  4100 shortcuts etc.: replace action isabelle-find by isabelle-query.
  4101 
  4102 * Search field for all output panels ("Output", "Query", "Info" etc.)
  4103 to highlight text via regular expression.
  4104 
  4105 * Option "jedit_print_mode" (see also "Plugin Options / Isabelle /
  4106 General") allows to specify additional print modes for the prover
  4107 process, without requiring old-fashioned command-line invocation of
  4108 "isabelle jedit -m MODE".
  4109 
  4110 * More support for remote files (e.g. http) using standard Java
  4111 networking operations instead of jEdit virtual file-systems.
  4112 
  4113 * Empty editors buffers that are no longer required (e.g.\ via theory
  4114 imports) are automatically removed from the document model.
  4115 
  4116 * Improved monitor panel.
  4117 
  4118 * Improved Console/Scala plugin: more uniform scala.Console output,
  4119 more robust treatment of threads and interrupts.
  4120 
  4121 * Improved management of dockable windows: clarified keyboard focus
  4122 and window placement wrt. main editor view; optional menu item to
  4123 "Detach" a copy where this makes sense.
  4124 
  4125 * New Simplifier Trace panel provides an interactive view of the
  4126 simplification process, enabled by the "simp_trace_new" attribute
  4127 within the context.
  4128 
  4129 
  4130 *** Pure ***
  4131 
  4132 * Low-level type-class commands 'classes', 'classrel', 'arities' have
  4133 been discontinued to avoid the danger of non-trivial axiomatization
  4134 that is not immediately visible.  INCOMPATIBILITY, use regular
  4135 'instance' command with proof.  The required OFCLASS(...) theorem
  4136 might be postulated via 'axiomatization' beforehand, or the proof
  4137 finished trivially if the underlying class definition is made vacuous
  4138 (without any assumptions).  See also Isabelle/ML operations
  4139 Axclass.class_axiomatization, Axclass.classrel_axiomatization,
  4140 Axclass.arity_axiomatization.
  4141 
  4142 * Basic constants of Pure use more conventional names and are always
  4143 qualified.  Rare INCOMPATIBILITY, but with potentially serious
  4144 consequences, notably for tools in Isabelle/ML.  The following
  4145 renaming needs to be applied:
  4146 
  4147   ==             ~>  Pure.eq
  4148   ==>            ~>  Pure.imp
  4149   all            ~>  Pure.all
  4150   TYPE           ~>  Pure.type
  4151   dummy_pattern  ~>  Pure.dummy_pattern
  4152 
  4153 Systematic porting works by using the following theory setup on a
  4154 *previous* Isabelle version to introduce the new name accesses for the
  4155 old constants:
  4156 
  4157 setup {*
  4158   fn thy => thy
  4159     |> Sign.root_path
  4160     |> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="
  4161     |> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"
  4162     |> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"
  4163     |> Sign.restore_naming thy
  4164 *}
  4165 
  4166 Thus ML antiquotations like @{const_name Pure.eq} may be used already.
  4167 Later the application is moved to the current Isabelle version, and
  4168 the auxiliary aliases are deleted.
  4169 
  4170 * Attributes "where" and "of" allow an optional context of local
  4171 variables ('for' declaration): these variables become schematic in the
  4172 instantiated theorem.
  4173 
  4174 * Obsolete attribute "standard" has been discontinued (legacy since
  4175 Isabelle2012).  Potential INCOMPATIBILITY, use explicit 'for' context
  4176 where instantiations with schematic variables are intended (for
  4177 declaration commands like 'lemmas' or attributes like "of").  The
  4178 following temporary definition may help to port old applications:
  4179 
  4180   attribute_setup standard =
  4181     "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
  4182 
  4183 * More thorough check of proof context for goal statements and
  4184 attributed fact expressions (concerning background theory, declared
  4185 hyps).  Potential INCOMPATIBILITY, tools need to observe standard
  4186 context discipline.  See also Assumption.add_assumes and the more
  4187 primitive Thm.assume_hyps.
  4188 
  4189 * Inner syntax token language allows regular quoted strings "..."
  4190 (only makes sense in practice, if outer syntax is delimited
  4191 differently, e.g. via cartouches).
  4192 
  4193 * Command 'print_term_bindings' supersedes 'print_binds' for clarity,
  4194 but the latter is retained some time as Proof General legacy.
  4195 
  4196 * Code generator preprocessor: explicit control of simp tracing on a
  4197 per-constant basis.  See attribute "code_preproc".
  4198 
  4199 
  4200 *** HOL ***
  4201 
  4202 * Code generator: enforce case of identifiers only for strict target
  4203 language requirements.  INCOMPATIBILITY.
  4204 
  4205 * Code generator: explicit proof contexts in many ML interfaces.
  4206 INCOMPATIBILITY.
  4207 
  4208 * Code generator: minimize exported identifiers by default.  Minor
  4209 INCOMPATIBILITY.
  4210 
  4211 * Code generation for SML and OCaml: dropped arcane "no_signatures"
  4212 option.  Minor INCOMPATIBILITY.
  4213 
  4214 * "declare [[code abort: ...]]" replaces "code_abort ...".
  4215 INCOMPATIBILITY.
  4216 
  4217 * "declare [[code drop: ...]]" drops all code equations associated
  4218 with the given constants.
  4219 
  4220 * Code generations are provided for make, fields, extend and truncate
  4221 operations on records.
  4222 
  4223 * Command and antiquotation "value" are now hardcoded against nbe and
  4224 ML.  Minor INCOMPATIBILITY.
  4225 
  4226 * Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY.
  4227 
  4228 * The symbol "\<newline>" may be used within char or string literals
  4229 to represent (Char Nibble0 NibbleA), i.e. ASCII newline.
  4230 
  4231 * Qualified String.implode and String.explode.  INCOMPATIBILITY.
  4232 
  4233 * Simplifier: Enhanced solver of preconditions of rewrite rules can
  4234 now deal with conjunctions.  For help with converting proofs, the old
  4235 behaviour of the simplifier can be restored like this: declare/using
  4236 [[simp_legacy_precond]].  This configuration option will disappear
  4237 again in the future.  INCOMPATIBILITY.
  4238 
  4239 * Simproc "finite_Collect" is no longer enabled by default, due to
  4240 spurious crashes and other surprises.  Potential INCOMPATIBILITY.
  4241 
  4242 * Moved new (co)datatype package and its dependencies from session
  4243   "HOL-BNF" to "HOL".  The commands 'bnf', 'wrap_free_constructors',
  4244   'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now
  4245   part of theory "Main".
  4246 
  4247   Theory renamings:
  4248     FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
  4249     Library/Wfrec.thy ~> Wfrec.thy
  4250     Library/Zorn.thy ~> Zorn.thy
  4251     Cardinals/Order_Relation.thy ~> Order_Relation.thy
  4252     Library/Order_Union.thy ~> Cardinals/Order_Union.thy
  4253     Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy
  4254     Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy
  4255     Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy
  4256     Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy
  4257     Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy
  4258     BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy
  4259     BNF/Basic_BNFs.thy ~> Basic_BNFs.thy
  4260     BNF/BNF_Comp.thy ~> BNF_Comp.thy
  4261     BNF/BNF_Def.thy ~> BNF_Def.thy
  4262     BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy
  4263     BNF/BNF_GFP.thy ~> BNF_GFP.thy
  4264     BNF/BNF_LFP.thy ~> BNF_LFP.thy
  4265     BNF/BNF_Util.thy ~> BNF_Util.thy
  4266     BNF/Coinduction.thy ~> Coinduction.thy
  4267     BNF/More_BNFs.thy ~> Library/More_BNFs.thy
  4268     BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy
  4269     BNF/Examples/* ~> BNF_Examples/*
  4270 
  4271   New theories:
  4272     Wellorder_Extension.thy (split from Zorn.thy)
  4273     Library/Cardinal_Notations.thy
  4274     Library/BNF_Axomatization.thy
  4275     BNF_Examples/Misc_Primcorec.thy
  4276     BNF_Examples/Stream_Processor.thy
  4277 
  4278   Discontinued theories:
  4279     BNF/BNF.thy
  4280     BNF/Equiv_Relations_More.thy
  4281 
  4282 INCOMPATIBILITY.
  4283 
  4284 * New (co)datatype package:
  4285   - Command 'primcorec' is fully implemented.
  4286   - Command 'datatype_new' generates size functions ("size_xxx" and
  4287     "size") as required by 'fun'.
  4288   - BNFs are integrated with the Lifting tool and new-style
  4289     (co)datatypes with Transfer.
  4290   - Renamed commands:
  4291       datatype_new_compat ~> datatype_compat
  4292       primrec_new ~> primrec
  4293       wrap_free_constructors ~> free_constructors
  4294     INCOMPATIBILITY.
  4295   - The generated constants "xxx_case" and "xxx_rec" have been renamed
  4296     "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
  4297     INCOMPATIBILITY.
  4298   - The constant "xxx_(un)fold" and related theorems are no longer
  4299     generated.  Use "xxx_(co)rec" or define "xxx_(un)fold" manually
  4300     using "prim(co)rec".
  4301     INCOMPATIBILITY.
  4302   - No discriminators are generated for nullary constructors by
  4303     default, eliminating the need for the odd "=:" syntax.
  4304     INCOMPATIBILITY.
  4305   - No discriminators or selectors are generated by default by
  4306     "datatype_new", unless custom names are specified or the new
  4307     "discs_sels" option is passed.
  4308     INCOMPATIBILITY.
  4309 
  4310 * Old datatype package:
  4311   - The generated theorems "xxx.cases" and "xxx.recs" have been
  4312     renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" ->
  4313     "sum.case").  INCOMPATIBILITY.
  4314   - The generated constants "xxx_case", "xxx_rec", and "xxx_size" have
  4315     been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g.,
  4316     "prod_case" ~> "case_prod").  INCOMPATIBILITY.
  4317 
  4318 * The types "'a list" and "'a option", their set and map functions,
  4319   their relators, and their selectors are now produced using the new
  4320   BNF-based datatype package.
  4321 
  4322   Renamed constants:
  4323     Option.set ~> set_option
  4324     Option.map ~> map_option
  4325     option_rel ~> rel_option
  4326 
  4327   Renamed theorems:
  4328     set_def ~> set_rec[abs_def]
  4329     map_def ~> map_rec[abs_def]
  4330     Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
  4331     option.recs ~> option.rec
  4332     list_all2_def ~> list_all2_iff
  4333     set.simps ~> set_simps (or the slightly different "list.set")
  4334     map.simps ~> list.map
  4335     hd.simps ~> list.sel(1)
  4336     tl.simps ~> list.sel(2-3)
  4337     the.simps ~> option.sel
  4338 
  4339 INCOMPATIBILITY.
  4340 
  4341 * The following map functions and relators have been renamed:
  4342     sum_map ~> map_sum
  4343     map_pair ~> map_prod
  4344     prod_rel ~> rel_prod
  4345     sum_rel ~> rel_sum
  4346     fun_rel ~> rel_fun
  4347     set_rel ~> rel_set
  4348     filter_rel ~> rel_filter
  4349     fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy")
  4350     cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy")
  4351     vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy")
  4352 
  4353 INCOMPATIBILITY.
  4354 
  4355 * Lifting and Transfer:
  4356   - a type variable as a raw type is supported
  4357   - stronger reflexivity prover
  4358   - rep_eq is always generated by lift_definition
  4359   - setup for Lifting/Transfer is now automated for BNFs
  4360     + holds for BNFs that do not contain a dead variable
  4361     + relator_eq, relator_mono, relator_distr, relator_domain,
  4362       relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total,
  4363       right_unique, right_total, left_unique, left_total are proved
  4364       automatically
  4365     + definition of a predicator is generated automatically
  4366     + simplification rules for a predicator definition are proved
  4367       automatically for datatypes
  4368   - consolidation of the setup of Lifting/Transfer
  4369     + property that a relator preservers reflexivity is not needed any
  4370       more
  4371       Minor INCOMPATIBILITY.
  4372     + left_total and left_unique rules are now transfer rules
  4373       (reflexivity_rule attribute not needed anymore)
  4374       INCOMPATIBILITY.
  4375     + Domainp does not have to be a separate assumption in
  4376       relator_domain theorems (=> more natural statement)
  4377       INCOMPATIBILITY.
  4378   - registration of code equations is more robust
  4379     Potential INCOMPATIBILITY.
  4380   - respectfulness proof obligation is preprocessed to a more readable
  4381     form
  4382     Potential INCOMPATIBILITY.
  4383   - eq_onp is always unfolded in respectfulness proof obligation
  4384     Potential INCOMPATIBILITY.
  4385   - unregister lifting setup for Code_Numeral.integer and
  4386     Code_Numeral.natural
  4387     Potential INCOMPATIBILITY.
  4388   - Lifting.invariant -> eq_onp
  4389     INCOMPATIBILITY.
  4390 
  4391 * New internal SAT solver "cdclite" that produces models and proof
  4392 traces.  This solver replaces the internal SAT solvers "enumerate" and
  4393 "dpll".  Applications that explicitly used one of these two SAT
  4394 solvers should use "cdclite" instead. In addition, "cdclite" is now
  4395 the default SAT solver for the "sat" and "satx" proof methods and
  4396 corresponding tactics; the old default can be restored using "declare
  4397 [[sat_solver = zchaff_with_proofs]]".  Minor INCOMPATIBILITY.
  4398 
  4399 * SMT module: A new version of the SMT module, temporarily called
  4400 "SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g.,
  4401 4.3). The new proof method is called "smt2". CVC3 and CVC4 are also
  4402 supported as oracles. Yices is no longer supported, because no version
  4403 of the solver can handle both SMT-LIB 2 and quantifiers.
  4404 
  4405 * Activation of Z3 now works via "z3_non_commercial" system option
  4406 (without requiring restart), instead of former settings variable
  4407 "Z3_NON_COMMERCIAL".  The option can be edited in Isabelle/jEdit menu
  4408 Plugin Options / Isabelle / General.
  4409 
  4410 * Sledgehammer:
  4411   - Z3 can now produce Isar proofs.
  4412   - MaSh overhaul:
  4413     . New SML-based learning algorithms eliminate the dependency on
  4414       Python and increase performance and reliability.
  4415     . MaSh and MeSh are now used by default together with the
  4416       traditional MePo (Meng-Paulson) relevance filter. To disable
  4417       MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin
  4418       Options / Isabelle / General to "none".
  4419   - New option:
  4420       smt_proofs
  4421   - Renamed options:
  4422       isar_compress ~> compress
  4423       isar_try0 ~> try0
  4424 
  4425 INCOMPATIBILITY.
  4426 
  4427 * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
  4428 
  4429 * Nitpick:
  4430   - Fixed soundness bug whereby mutually recursive datatypes could
  4431     take infinite values.
  4432   - Fixed soundness bug with low-level number functions such as
  4433     "Abs_Integ" and "Rep_Integ".
  4434   - Removed "std" option.
  4435   - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to
  4436     "hide_types".
  4437 
  4438 * Metis: Removed legacy proof method 'metisFT'. Use 'metis
  4439 (full_types)' instead. INCOMPATIBILITY.
  4440 
  4441 * Try0: Added 'algebra' and 'meson' to the set of proof methods.
  4442 
  4443 * Adjustion of INF and SUP operations:
  4444   - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
  4445   - Consolidated theorem names containing INFI and SUPR: have INF and
  4446     SUP instead uniformly.
  4447   - More aggressive normalization of expressions involving INF and Inf
  4448     or SUP and Sup.
  4449   - INF_image and SUP_image do not unfold composition.
  4450   - Dropped facts INF_comp, SUP_comp.
  4451   - Default congruence rules strong_INF_cong and strong_SUP_cong, with
  4452     simplifier implication in premises.  Generalize and replace former
  4453     INT_cong, SUP_cong
  4454 
  4455 INCOMPATIBILITY.
  4456 
  4457 * SUP and INF generalized to conditionally_complete_lattice.
  4458 
  4459 * Swapped orientation of facts image_comp and vimage_comp:
  4460 
  4461   image_compose ~> image_comp [symmetric]
  4462   image_comp ~> image_comp [symmetric]
  4463   vimage_compose ~> vimage_comp [symmetric]
  4464   vimage_comp ~> vimage_comp [symmetric]
  4465 
  4466 INCOMPATIBILITY.
  4467 
  4468 * Theory reorganization: split of Big_Operators.thy into
  4469 Groups_Big.thy and Lattices_Big.thy.
  4470 
  4471 * Consolidated some facts about big group operators:
  4472 
  4473     setsum_0' ~> setsum.neutral
  4474     setsum_0 ~> setsum.neutral_const
  4475     setsum_addf ~> setsum.distrib
  4476     setsum_cartesian_product ~> setsum.cartesian_product
  4477     setsum_cases ~> setsum.If_cases
  4478     setsum_commute ~> setsum.commute
  4479     setsum_cong ~> setsum.cong
  4480     setsum_delta ~> setsum.delta
  4481     setsum_delta' ~> setsum.delta'
  4482     setsum_diff1' ~> setsum.remove
  4483     setsum_empty ~> setsum.empty
  4484     setsum_infinite ~> setsum.infinite
  4485     setsum_insert ~> setsum.insert
  4486     setsum_inter_restrict'' ~> setsum.inter_filter
  4487     setsum_mono_zero_cong_left ~> setsum.mono_neutral_cong_left
  4488     setsum_mono_zero_cong_right ~> setsum.mono_neutral_cong_right
  4489     setsum_mono_zero_left ~> setsum.mono_neutral_left
  4490     setsum_mono_zero_right ~> setsum.mono_neutral_right
  4491     setsum_reindex ~> setsum.reindex
  4492     setsum_reindex_cong ~> setsum.reindex_cong
  4493     setsum_reindex_nonzero ~> setsum.reindex_nontrivial
  4494     setsum_restrict_set ~> setsum.inter_restrict
  4495     setsum_Plus ~> setsum.Plus
  4496     setsum_setsum_restrict ~> setsum.commute_restrict
  4497     setsum_Sigma ~> setsum.Sigma
  4498     setsum_subset_diff ~> setsum.subset_diff
  4499     setsum_Un_disjoint ~> setsum.union_disjoint
  4500     setsum_UN_disjoint ~> setsum.UNION_disjoint
  4501     setsum_Un_Int ~> setsum.union_inter
  4502     setsum_Union_disjoint ~> setsum.Union_disjoint
  4503     setsum_UNION_zero ~> setsum.Union_comp
  4504     setsum_Un_zero ~> setsum.union_inter_neutral
  4505     strong_setprod_cong ~> setprod.strong_cong
  4506     strong_setsum_cong ~> setsum.strong_cong
  4507     setprod_1' ~> setprod.neutral
  4508     setprod_1 ~> setprod.neutral_const
  4509     setprod_cartesian_product ~> setprod.cartesian_product
  4510     setprod_cong ~> setprod.cong
  4511     setprod_delta ~> setprod.delta
  4512     setprod_delta' ~> setprod.delta'
  4513     setprod_empty ~> setprod.empty
  4514     setprod_infinite ~> setprod.infinite
  4515     setprod_insert ~> setprod.insert
  4516     setprod_mono_one_cong_left ~> setprod.mono_neutral_cong_left
  4517     setprod_mono_one_cong_right ~> setprod.mono_neutral_cong_right
  4518     setprod_mono_one_left ~> setprod.mono_neutral_left
  4519     setprod_mono_one_right ~> setprod.mono_neutral_right
  4520     setprod_reindex ~> setprod.reindex
  4521     setprod_reindex_cong ~> setprod.reindex_cong
  4522     setprod_reindex_nonzero ~> setprod.reindex_nontrivial
  4523     setprod_Sigma ~> setprod.Sigma
  4524     setprod_subset_diff ~> setprod.subset_diff
  4525     setprod_timesf ~> setprod.distrib
  4526     setprod_Un2 ~> setprod.union_diff2
  4527     setprod_Un_disjoint ~> setprod.union_disjoint
  4528     setprod_UN_disjoint ~> setprod.UNION_disjoint
  4529     setprod_Un_Int ~> setprod.union_inter
  4530     setprod_Union_disjoint ~> setprod.Union_disjoint
  4531     setprod_Un_one ~> setprod.union_inter_neutral
  4532 
  4533   Dropped setsum_cong2 (simple variant of setsum.cong).
  4534   Dropped setsum_inter_restrict' (simple variant of setsum.inter_restrict)
  4535   Dropped setsum_reindex_id, setprod_reindex_id
  4536     (simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]).
  4537 
  4538 INCOMPATIBILITY.
  4539 
  4540 * Abolished slightly odd global lattice interpretation for min/max.
  4541 
  4542   Fact consolidations:
  4543     min_max.inf_assoc ~> min.assoc
  4544     min_max.inf_commute ~> min.commute
  4545     min_max.inf_left_commute ~> min.left_commute
  4546     min_max.inf_idem ~> min.idem
  4547     min_max.inf_left_idem ~> min.left_idem
  4548     min_max.inf_right_idem ~> min.right_idem
  4549     min_max.sup_assoc ~> max.assoc
  4550     min_max.sup_commute ~> max.commute
  4551     min_max.sup_left_commute ~> max.left_commute
  4552     min_max.sup_idem ~> max.idem
  4553     min_max.sup_left_idem ~> max.left_idem
  4554     min_max.sup_inf_distrib1 ~> max_min_distrib2
  4555     min_max.sup_inf_distrib2 ~> max_min_distrib1
  4556     min_max.inf_sup_distrib1 ~> min_max_distrib2
  4557     min_max.inf_sup_distrib2 ~> min_max_distrib1
  4558     min_max.distrib ~> min_max_distribs
  4559     min_max.inf_absorb1 ~> min.absorb1
  4560     min_max.inf_absorb2 ~> min.absorb2
  4561     min_max.sup_absorb1 ~> max.absorb1
  4562     min_max.sup_absorb2 ~> max.absorb2
  4563     min_max.le_iff_inf ~> min.absorb_iff1
  4564     min_max.le_iff_sup ~> max.absorb_iff2
  4565     min_max.inf_le1 ~> min.cobounded1
  4566     min_max.inf_le2 ~> min.cobounded2
  4567     le_maxI1, min_max.sup_ge1 ~> max.cobounded1
  4568     le_maxI2, min_max.sup_ge2 ~> max.cobounded2
  4569     min_max.le_infI1 ~> min.coboundedI1
  4570     min_max.le_infI2 ~> min.coboundedI2
  4571     min_max.le_supI1 ~> max.coboundedI1
  4572     min_max.le_supI2 ~> max.coboundedI2
  4573     min_max.less_infI1 ~> min.strict_coboundedI1
  4574     min_max.less_infI2 ~> min.strict_coboundedI2
  4575     min_max.less_supI1 ~> max.strict_coboundedI1
  4576     min_max.less_supI2 ~> max.strict_coboundedI2
  4577     min_max.inf_mono ~> min.mono
  4578     min_max.sup_mono ~> max.mono
  4579     min_max.le_infI, min_max.inf_greatest ~> min.boundedI
  4580     min_max.le_supI, min_max.sup_least ~> max.boundedI
  4581     min_max.le_inf_iff ~> min.bounded_iff
  4582     min_max.le_sup_iff ~> max.bounded_iff
  4583 
  4584 For min_max.inf_sup_aci, prefer (one of) min.commute, min.assoc,
  4585 min.left_commute, min.left_idem, max.commute, max.assoc,
  4586 max.left_commute, max.left_idem directly.
  4587 
  4588 For min_max.inf_sup_ord, prefer (one of) min.cobounded1,
  4589 min.cobounded2, max.cobounded1m max.cobounded2 directly.
  4590 
  4591 For min_ac or max_ac, prefer more general collection ac_simps.
  4592 
  4593 INCOMPATIBILITY.
  4594 
  4595 * Theorem disambiguation Inf_le_Sup (on finite sets) ~>
  4596 Inf_fin_le_Sup_fin.  INCOMPATIBILITY.
  4597 
  4598 * Qualified constant names Wellfounded.acc, Wellfounded.accp.
  4599 INCOMPATIBILITY.
  4600 
  4601 * Fact generalization and consolidation:
  4602     neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
  4603 
  4604 INCOMPATIBILITY.
  4605 
  4606 * Purely algebraic definition of even.  Fact generalization and
  4607   consolidation:
  4608     nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd
  4609     even_zero_(nat|int) ~> even_zero
  4610 
  4611 INCOMPATIBILITY.
  4612 
  4613 * Abolished neg_numeral.
  4614   - Canonical representation for minus one is "- 1".
  4615   - Canonical representation for other negative numbers is "- (numeral _)".
  4616   - When devising rule sets for number calculation, consider the
  4617     following canonical cases: 0, 1, numeral _, - 1, - numeral _.
  4618   - HOLogic.dest_number also recognizes numerals in non-canonical forms
  4619     like "numeral One", "- numeral One", "- 0" and even "- ... - _".
  4620   - Syntax for negative numerals is mere input syntax.
  4621 
  4622 INCOMPATIBILITY.
  4623 
  4624 * Reduced name variants for rules on associativity and commutativity:
  4625 
  4626     add_assoc ~> add.assoc
  4627     add_commute ~> add.commute
  4628     add_left_commute ~> add.left_commute
  4629     mult_assoc ~> mult.assoc
  4630     mult_commute ~> mult.commute
  4631     mult_left_commute ~> mult.left_commute
  4632     nat_add_assoc ~> add.assoc
  4633     nat_add_commute ~> add.commute
  4634     nat_add_left_commute ~> add.left_commute
  4635     nat_mult_assoc ~> mult.assoc
  4636     nat_mult_commute ~> mult.commute
  4637     eq_assoc ~> iff_assoc
  4638     eq_left_commute ~> iff_left_commute
  4639 
  4640 INCOMPATIBILITY.
  4641 
  4642 * Fact collections add_ac and mult_ac are considered old-fashioned.
  4643 Prefer ac_simps instead, or specify rules
  4644 (add|mult).(assoc|commute|left_commute) individually.
  4645 
  4646 * Elimination of fact duplicates:
  4647     equals_zero_I ~> minus_unique
  4648     diff_eq_0_iff_eq ~> right_minus_eq
  4649     nat_infinite ~> infinite_UNIV_nat
  4650     int_infinite ~> infinite_UNIV_int
  4651 
  4652 INCOMPATIBILITY.
  4653 
  4654 * Fact name consolidation:
  4655     diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus
  4656     minus_le_self_iff ~> neg_less_eq_nonneg
  4657     le_minus_self_iff ~> less_eq_neg_nonpos
  4658     neg_less_nonneg ~> neg_less_pos
  4659     less_minus_self_iff ~> less_neg_neg [simp]
  4660 
  4661 INCOMPATIBILITY.
  4662 
  4663 * More simplification rules on unary and binary minus:
  4664 add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,
  4665 add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,
  4666 add_minus_cancel, diff_add_cancel, le_add_same_cancel1,
  4667 le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,
  4668 minus_add_cancel, uminus_add_conv_diff.  These correspondingly have
  4669 been taken away from fact collections algebra_simps and field_simps.
  4670 INCOMPATIBILITY.
  4671 
  4672 To restore proofs, the following patterns are helpful:
  4673 
  4674 a) Arbitrary failing proof not involving "diff_def":
  4675 Consider simplification with algebra_simps or field_simps.
  4676 
  4677 b) Lifting rules from addition to subtraction:
  4678 Try with "using <rule for addition> of [... "- _" ...]" by simp".
  4679 
  4680 c) Simplification with "diff_def": just drop "diff_def".
  4681 Consider simplification with algebra_simps or field_simps;
  4682 or the brute way with
  4683 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
  4684 
  4685 * Introduce bdd_above and bdd_below in theory
  4686 Conditionally_Complete_Lattices, use them instead of explicitly
  4687 stating boundedness of sets.
  4688 
  4689 * ccpo.admissible quantifies only over non-empty chains to allow more
  4690 syntax-directed proof rules; the case of the empty chain shows up as
  4691 additional case in fixpoint induction proofs.  INCOMPATIBILITY.
  4692 
  4693 * Removed and renamed theorems in Series:
  4694   summable_le         ~>  suminf_le
  4695   suminf_le           ~>  suminf_le_const
  4696   series_pos_le       ~>  setsum_le_suminf
  4697   series_pos_less     ~>  setsum_less_suminf
  4698   suminf_ge_zero      ~>  suminf_nonneg
  4699   suminf_gt_zero      ~>  suminf_pos
  4700   suminf_gt_zero_iff  ~>  suminf_pos_iff
  4701   summable_sumr_LIMSEQ_suminf  ~>  summable_LIMSEQ
  4702   suminf_0_le         ~>  suminf_nonneg [rotate]
  4703   pos_summable        ~>  summableI_nonneg_bounded
  4704   ratio_test          ~>  summable_ratio_test
  4705 
  4706   removed series_zero, replaced by sums_finite
  4707 
  4708   removed auxiliary lemmas:
  4709 
  4710     sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group,
  4711     half, le_Suc_ex_iff, lemma_realpow_diff_sumr,
  4712     real_setsum_nat_ivl_bounded, summable_le2, ratio_test_lemma2,
  4713     sumr_minus_one_realpow_zerom, sumr_one_lb_realpow_zero,
  4714     summable_convergent_sumr_iff, sumr_diff_mult_const
  4715 
  4716 INCOMPATIBILITY.
  4717 
  4718 * Replace (F)DERIV syntax by has_derivative:
  4719   - "(f has_derivative f') (at x within s)" replaces "FDERIV f x : s : f'"
  4720 
  4721   - "(f has_field_derivative f') (at x within s)" replaces "DERIV f x : s : f'"
  4722 
  4723   - "f differentiable at x within s" replaces "_ differentiable _ in _" syntax
  4724 
  4725   - removed constant isDiff
  4726 
  4727   - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as
  4728     input syntax.
  4729 
  4730   - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed.
  4731 
  4732   - Renamed FDERIV_... lemmas to has_derivative_...
  4733 
  4734   - renamed deriv (the syntax constant used for "DERIV _ _ :> _") to DERIV
  4735 
  4736   - removed DERIV_intros, has_derivative_eq_intros
  4737 
  4738   - introduced derivative_intros and deriative_eq_intros which
  4739     includes now rules for DERIV, has_derivative and
  4740     has_vector_derivative.
  4741 
  4742   - Other renamings:
  4743     differentiable_def        ~>  real_differentiable_def
  4744     differentiableE           ~>  real_differentiableE
  4745     fderiv_def                ~>  has_derivative_at
  4746     field_fderiv_def          ~>  field_has_derivative_at
  4747     isDiff_der                ~>  differentiable_def
  4748     deriv_fderiv              ~>  has_field_derivative_def
  4749     deriv_def                 ~>  DERIV_def
  4750 
  4751 INCOMPATIBILITY.
  4752 
  4753 * Include more theorems in continuous_intros. Remove the
  4754 continuous_on_intros, isCont_intros collections, these facts are now
  4755 in continuous_intros.
  4756 
  4757 * Theorems about complex numbers are now stated only using Re and Im,
  4758 the Complex constructor is not used anymore. It is possible to use
  4759 primcorec to defined the behaviour of a complex-valued function.
  4760 
  4761 Removed theorems about the Complex constructor from the simpset, they
  4762 are available as the lemma collection legacy_Complex_simps. This
  4763 especially removes
  4764 
  4765     i_complex_of_real: "ii * complex_of_real r = Complex 0 r".
  4766 
  4767 Instead the reverse direction is supported with
  4768     Complex_eq: "Complex a b = a + \<i> * b"
  4769 
  4770 Moved csqrt from Fundamental_Algebra_Theorem to Complex.
  4771 
  4772   Renamings:
  4773     Re/Im                  ~>  complex.sel
  4774     complex_Re/Im_zero     ~>  zero_complex.sel
  4775     complex_Re/Im_add      ~>  plus_complex.sel
  4776     complex_Re/Im_minus    ~>  uminus_complex.sel
  4777     complex_Re/Im_diff     ~>  minus_complex.sel
  4778     complex_Re/Im_one      ~>  one_complex.sel
  4779     complex_Re/Im_mult     ~>  times_complex.sel
  4780     complex_Re/Im_inverse  ~>  inverse_complex.sel
  4781     complex_Re/Im_scaleR   ~>  scaleR_complex.sel
  4782     complex_Re/Im_i        ~>  ii.sel
  4783     complex_Re/Im_cnj      ~>  cnj.sel
  4784     Re/Im_cis              ~>  cis.sel
  4785 
  4786     complex_divide_def   ~>  divide_complex_def
  4787     complex_norm_def     ~>  norm_complex_def
  4788     cmod_def             ~>  norm_complex_de
  4789 
  4790   Removed theorems:
  4791     complex_zero_def
  4792     complex_add_def
  4793     complex_minus_def
  4794     complex_diff_def
  4795     complex_one_def
  4796     complex_mult_def
  4797     complex_inverse_def
  4798     complex_scaleR_def
  4799 
  4800 INCOMPATIBILITY.
  4801 
  4802 * Theory Lubs moved HOL image to HOL-Library. It is replaced by
  4803 Conditionally_Complete_Lattices.  INCOMPATIBILITY.
  4804 
  4805 * HOL-Library: new theory src/HOL/Library/Tree.thy.
  4806 
  4807 * HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it
  4808 is subsumed by session Kleene_Algebra in AFP.
  4809 
  4810 * HOL-Library / theory RBT: various constants and facts are hidden;
  4811 lifting setup is unregistered.  INCOMPATIBILITY.
  4812 
  4813 * HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
  4814 
  4815 * HOL-Word: bit representations prefer type bool over type bit.
  4816 INCOMPATIBILITY.
  4817 
  4818 * HOL-Word:
  4819   - Abandoned fact collection "word_arith_alts", which is a duplicate
  4820     of "word_arith_wis".
  4821   - Dropped first (duplicated) element in fact collections
  4822     "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
  4823     "uint_word_arith_bintrs".
  4824 
  4825 * HOL-Number_Theory:
  4826   - consolidated the proofs of the binomial theorem
  4827   - the function fib is again of type nat => nat and not overloaded
  4828   - no more references to Old_Number_Theory in the HOL libraries
  4829     (except the AFP)
  4830 
  4831 INCOMPATIBILITY.
  4832 
  4833 * HOL-Multivariate_Analysis:
  4834   - Type class ordered_real_vector for ordered vector spaces.
  4835   - New theory Complex_Basic_Analysis defining complex derivatives,
  4836     holomorphic functions, etc., ported from HOL Light's canal.ml.
  4837   - Changed order of ordered_euclidean_space to be compatible with
  4838     pointwise ordering on products. Therefore instance of
  4839     conditionally_complete_lattice and ordered_real_vector.
  4840     INCOMPATIBILITY: use box instead of greaterThanLessThan or
  4841     explicit set-comprehensions with eucl_less for other (half-)open
  4842     intervals.
  4843   - removed dependencies on type class ordered_euclidean_space with
  4844     introduction of "cbox" on euclidean_space
  4845     - renamed theorems:
  4846         interval ~> box
  4847         mem_interval ~> mem_box
  4848         interval_eq_empty ~> box_eq_empty
  4849         interval_ne_empty ~> box_ne_empty
  4850         interval_sing(1) ~> cbox_sing
  4851         interval_sing(2) ~> box_sing
  4852         subset_interval_imp ~> subset_box_imp
  4853         subset_interval ~> subset_box
  4854         open_interval ~> open_box
  4855         closed_interval ~> closed_cbox
  4856         interior_closed_interval ~> interior_cbox
  4857         bounded_closed_interval ~> bounded_cbox
  4858         compact_interval ~> compact_cbox
  4859         bounded_subset_closed_interval_symmetric ~> bounded_subset_cbox_symmetric
  4860         bounded_subset_closed_interval ~> bounded_subset_cbox
  4861         mem_interval_componentwiseI ~> mem_box_componentwiseI
  4862         convex_box ~> convex_prod
  4863         rel_interior_real_interval ~> rel_interior_real_box
  4864         convex_interval ~> convex_box
  4865         convex_hull_eq_real_interval ~> convex_hull_eq_real_cbox
  4866         frechet_derivative_within_closed_interval ~> frechet_derivative_within_cbox
  4867         content_closed_interval' ~> content_cbox'
  4868         elementary_subset_interval ~> elementary_subset_box
  4869         diameter_closed_interval ~> diameter_cbox
  4870         frontier_closed_interval ~> frontier_cbox
  4871         frontier_open_interval ~> frontier_box
  4872         bounded_subset_open_interval_symmetric ~> bounded_subset_box_symmetric
  4873         closure_open_interval ~> closure_box
  4874         open_closed_interval_convex ~> open_cbox_convex
  4875         open_interval_midpoint ~> box_midpoint
  4876         content_image_affinity_interval ~> content_image_affinity_cbox
  4877         is_interval_interval ~> is_interval_cbox + is_interval_box + is_interval_closed_interval
  4878         bounded_interval ~> bounded_closed_interval + bounded_boxes
  4879 
  4880     - respective theorems for intervals over the reals:
  4881         content_closed_interval + content_cbox
  4882         has_integral + has_integral_real
  4883         fine_division_exists + fine_division_exists_real
  4884         has_integral_null + has_integral_null_real
  4885         tagged_division_union_interval + tagged_division_union_interval_real
  4886         has_integral_const + has_integral_const_real
  4887         integral_const + integral_const_real
  4888         has_integral_bound + has_integral_bound_real
  4889         integrable_continuous + integrable_continuous_real
  4890         integrable_subinterval + integrable_subinterval_real
  4891         has_integral_reflect_lemma + has_integral_reflect_lemma_real
  4892         integrable_reflect + integrable_reflect_real
  4893         integral_reflect + integral_reflect_real
  4894         image_affinity_interval + image_affinity_cbox
  4895         image_smult_interval + image_smult_cbox
  4896         integrable_const + integrable_const_ivl
  4897         integrable_on_subinterval + integrable_on_subcbox
  4898 
  4899   - renamed theorems:
  4900     derivative_linear         ~>  has_derivative_bounded_linear
  4901     derivative_is_linear      ~>  has_derivative_linear
  4902     bounded_linear_imp_linear ~>  bounded_linear.linear
  4903 
  4904 * HOL-Probability:
  4905   - Renamed positive_integral to nn_integral:
  4906 
  4907     . Renamed all lemmas "*positive_integral*" to *nn_integral*"
  4908       positive_integral_positive ~> nn_integral_nonneg
  4909 
  4910     . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
  4911 
  4912   - replaced the Lebesgue integral on real numbers by the more general
  4913     Bochner integral for functions into a real-normed vector space.
  4914 
  4915     integral_zero               ~>  integral_zero / integrable_zero
  4916     integral_minus              ~>  integral_minus / integrable_minus
  4917     integral_add                ~>  integral_add / integrable_add
  4918     integral_diff               ~>  integral_diff / integrable_diff
  4919     integral_setsum             ~>  integral_setsum / integrable_setsum
  4920     integral_multc              ~>  integral_mult_left / integrable_mult_left
  4921     integral_cmult              ~>  integral_mult_right / integrable_mult_right
  4922     integral_triangle_inequality~>  integral_norm_bound
  4923     integrable_nonneg           ~>  integrableI_nonneg
  4924     integral_positive           ~>  integral_nonneg_AE
  4925     integrable_abs_iff          ~>  integrable_abs_cancel
  4926     positive_integral_lim_INF   ~>  nn_integral_liminf
  4927     lebesgue_real_affine        ~>  lborel_real_affine
  4928     borel_integral_has_integral ~>  has_integral_lebesgue_integral
  4929     integral_indicator          ~>
  4930          integral_real_indicator / integrable_real_indicator
  4931     positive_integral_fst       ~>  nn_integral_fst'
  4932     positive_integral_fst_measurable ~> nn_integral_fst
  4933     positive_integral_snd_measurable ~> nn_integral_snd
  4934 
  4935     integrable_fst_measurable   ~>
  4936          integral_fst / integrable_fst / AE_integrable_fst
  4937 
  4938     integrable_snd_measurable   ~>
  4939          integral_snd / integrable_snd / AE_integrable_snd
  4940 
  4941     integral_monotone_convergence  ~>
  4942          integral_monotone_convergence / integrable_monotone_convergence
  4943 
  4944     integral_monotone_convergence_at_top  ~>
  4945          integral_monotone_convergence_at_top /
  4946          integrable_monotone_convergence_at_top
  4947 
  4948     has_integral_iff_positive_integral_lebesgue  ~>
  4949          has_integral_iff_has_bochner_integral_lebesgue_nonneg
  4950 
  4951     lebesgue_integral_has_integral  ~>
  4952          has_integral_integrable_lebesgue_nonneg
  4953 
  4954     positive_integral_lebesgue_has_integral  ~>
  4955          integral_has_integral_lebesgue_nonneg /
  4956          integrable_has_integral_lebesgue_nonneg
  4957 
  4958     lebesgue_integral_real_affine  ~>
  4959          nn_integral_real_affine
  4960 
  4961     has_integral_iff_positive_integral_lborel  ~>
  4962          integral_has_integral_nonneg / integrable_has_integral_nonneg
  4963 
  4964     The following theorems where removed:
  4965 
  4966     lebesgue_integral_nonneg
  4967     lebesgue_integral_uminus
  4968     lebesgue_integral_cmult
  4969     lebesgue_integral_multc
  4970     lebesgue_integral_cmult_nonneg
  4971     integral_cmul_indicator
  4972     integral_real
  4973 
  4974   - Formalized properties about exponentially, Erlang, and normal
  4975     distributed random variables.
  4976 
  4977 * HOL-Decision_Procs: Separate command 'approximate' for approximative
  4978 computation in src/HOL/Decision_Procs/Approximation.  Minor
  4979 INCOMPATIBILITY.
  4980 
  4981 
  4982 *** Scala ***
  4983 
  4984 * The signature and semantics of Document.Snapshot.cumulate_markup /
  4985 select_markup have been clarified.  Markup is now traversed in the
  4986 order of reports given by the prover: later markup is usually more
  4987 specific and may override results accumulated so far.  The elements
  4988 guard is mandatory and checked precisely.  Subtle INCOMPATIBILITY.
  4989 
  4990 * Substantial reworking of internal PIDE protocol communication
  4991 channels.  INCOMPATIBILITY.
  4992 
  4993 
  4994 *** ML ***
  4995 
  4996 * Subtle change of semantics of Thm.eq_thm: theory stamps are not
  4997 compared (according to Thm.thm_ord), but assumed to be covered by the
  4998 current background theory.  Thus equivalent data produced in different
  4999 branches of the theory graph usually coincides (e.g. relevant for
  5000 theory merge).  Note that the softer Thm.eq_thm_prop is often more
  5001 appropriate than Thm.eq_thm.
  5002 
  5003 * Proper context for basic Simplifier operations: rewrite_rule,
  5004 rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to
  5005 pass runtime Proof.context (and ensure that the simplified entity
  5006 actually belongs to it).
  5007 
  5008 * Proper context discipline for read_instantiate and instantiate_tac:
  5009 variables that are meant to become schematic need to be given as
  5010 fixed, and are generalized by the explicit context of local variables.
  5011 This corresponds to Isar attributes "where" and "of" with 'for'
  5012 declaration.  INCOMPATIBILITY, also due to potential change of indices
  5013 of schematic variables.
  5014 
  5015 * Moved ML_Compiler.exn_trace and other operations on exceptions to
  5016 structure Runtime.  Minor INCOMPATIBILITY.
  5017 
  5018 * Discontinued old Toplevel.debug in favour of system option
  5019 "ML_exception_trace", which may be also declared within the context
  5020 via "declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
  5021 
  5022 * Renamed configuration option "ML_trace" to "ML_source_trace". Minor
  5023 INCOMPATIBILITY.
  5024 
  5025 * Configuration option "ML_print_depth" controls the pretty-printing
  5026 depth of the ML compiler within the context.  The old print_depth in
  5027 ML is still available as default_print_depth, but rarely used.  Minor
  5028 INCOMPATIBILITY.
  5029 
  5030 * Toplevel function "use" refers to raw ML bootstrap environment,
  5031 without Isar context nor antiquotations.  Potential INCOMPATIBILITY.
  5032 Note that 'ML_file' is the canonical command to load ML files into the
  5033 formal context.
  5034 
  5035 * Simplified programming interface to define ML antiquotations, see
  5036 structure ML_Antiquotation.  Minor INCOMPATIBILITY.
  5037 
  5038 * ML antiquotation @{here} refers to its source position, which is
  5039 occasionally useful for experimentation and diagnostic purposes.
  5040 
  5041 * ML antiquotation @{path} produces a Path.T value, similarly to
  5042 Path.explode, but with compile-time check against the file-system and
  5043 some PIDE markup.  Note that unlike theory source, ML does not have a
  5044 well-defined master directory, so an absolute symbolic path
  5045 specification is usually required, e.g. "~~/src/HOL".
  5046 
  5047 * ML antiquotation @{print} inlines a function to print an arbitrary
  5048 ML value, which is occasionally useful for diagnostic or demonstration
  5049 purposes.
  5050 
  5051 
  5052 *** System ***
  5053 
  5054 * Proof General with its traditional helper scripts is now an optional
  5055 Isabelle component, e.g. see ProofGeneral-4.2-2 from the Isabelle
  5056 component repository http://isabelle.in.tum.de/components/.  Note that
  5057 the "system" manual provides general explanations about add-on
  5058 components, especially those that are not bundled with the release.
  5059 
  5060 * The raw Isabelle process executable has been renamed from
  5061 "isabelle-process" to "isabelle_process", which conforms to common
  5062 shell naming conventions, and allows to define a shell function within
  5063 the Isabelle environment to avoid dynamic path lookup.  Rare
  5064 incompatibility for old tools that do not use the ISABELLE_PROCESS
  5065 settings variable.
  5066 
  5067 * Former "isabelle tty" has been superseded by "isabelle console",
  5068 with implicit build like "isabelle jedit", and without the mostly
  5069 obsolete Isar TTY loop.
  5070 
  5071 * Simplified "isabelle display" tool.  Settings variables DVI_VIEWER
  5072 and PDF_VIEWER now refer to the actual programs, not shell
  5073 command-lines.  Discontinued option -c: invocation may be asynchronous
  5074 via desktop environment, without any special precautions.  Potential
  5075 INCOMPATIBILITY with ambitious private settings.
  5076 
  5077 * Removed obsolete "isabelle unsymbolize".  Note that the usual format
  5078 for email communication is the Unicode rendering of Isabelle symbols,
  5079 as produced by Isabelle/jEdit, for example.
  5080 
  5081 * Removed obsolete tool "wwwfind". Similar functionality may be
  5082 integrated into Isabelle/jEdit eventually.
  5083 
  5084 * Improved 'display_drafts' concerning desktop integration and
  5085 repeated invocation in PIDE front-end: re-use single file
  5086 $ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.
  5087 
  5088 * Session ROOT specifications require explicit 'document_files' for
  5089 robust dependencies on LaTeX sources.  Only these explicitly given
  5090 files are copied to the document output directory, before document
  5091 processing is started.
  5092 
  5093 * Windows: support for regular TeX installation (e.g. MiKTeX) instead
  5094 of TeX Live from Cygwin.
  5095 
  5096 
  5097 
  5098 New in Isabelle2013-2 (December 2013)
  5099 -------------------------------------
  5100 
  5101 *** Prover IDE -- Isabelle/Scala/jEdit ***
  5102 
  5103 * More robust editing of running commands with internal forks,
  5104 e.g. non-terminating 'by' steps.
  5105 
  5106 * More relaxed Sledgehammer panel: avoid repeated application of query
  5107 after edits surrounding the command location.
  5108 
  5109 * More status information about commands that are interrupted
  5110 accidentally (via physical event or Poly/ML runtime system signal,
  5111 e.g. out-of-memory).
  5112 
  5113 
  5114 *** System ***
  5115 
  5116 * More robust termination of external processes managed by
  5117 Isabelle/ML: support cancellation of tasks within the range of
  5118 milliseconds, as required for PIDE document editing with automatically
  5119 tried tools (e.g. Sledgehammer).
  5120 
  5121 * Reactivated Isabelle/Scala kill command for external processes on
  5122 Mac OS X, which was accidentally broken in Isabelle2013-1 due to a
  5123 workaround for some Debian/Ubuntu Linux versions from 2013.
  5124 
  5125 
  5126 
  5127 New in Isabelle2013-1 (November 2013)
  5128 -------------------------------------
  5129 
  5130 *** General ***
  5131 
  5132 * Discontinued obsolete 'uses' within theory header.  Note that
  5133 commands like 'ML_file' work without separate declaration of file
  5134 dependencies.  Minor INCOMPATIBILITY.
  5135 
  5136 * Discontinued redundant 'use' command, which was superseded by
  5137 'ML_file' in Isabelle2013.  Minor INCOMPATIBILITY.
  5138 
  5139 * Simplified subscripts within identifiers, using plain \<^sub>
  5140 instead of the second copy \<^isub> and \<^isup>.  Superscripts are
  5141 only for literal tokens within notation; explicit mixfix annotations
  5142 for consts or fixed variables may be used as fall-back for unusual
  5143 names.  Obsolete \<twosuperior> has been expanded to \<^sup>2 in
  5144 Isabelle/HOL.  INCOMPATIBILITY, use "isabelle update_sub_sup" to
  5145 standardize symbols as a starting point for further manual cleanup.
  5146 The ML reference variable "legacy_isub_isup" may be set as temporary
  5147 workaround, to make the prover accept a subset of the old identifier
  5148 syntax.
  5149 
  5150 * Document antiquotations: term style "isub" has been renamed to
  5151 "sub".  Minor INCOMPATIBILITY.
  5152 
  5153 * Uniform management of "quick_and_dirty" as system option (see also
  5154 "isabelle options"), configuration option within the context (see also
  5155 Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor
  5156 INCOMPATIBILITY, need to use more official Isabelle means to access
  5157 quick_and_dirty, instead of historical poking into mutable reference.
  5158 
  5159 * Renamed command 'print_configs' to 'print_options'.  Minor
  5160 INCOMPATIBILITY.
  5161 
  5162 * Proper diagnostic command 'print_state'.  Old 'pr' (with its
  5163 implicit change of some global references) is retained for now as
  5164 control command, e.g. for ProofGeneral 3.7.x.
  5165 
  5166 * Discontinued 'print_drafts' command with its old-fashioned PS output
  5167 and Unix command-line print spooling.  Minor INCOMPATIBILITY: use
  5168 'display_drafts' instead and print via the regular document viewer.
  5169 
  5170 * Updated and extended "isar-ref" and "implementation" manual,
  5171 eliminated old "ref" manual.
  5172 
  5173 
  5174 *** Prover IDE -- Isabelle/Scala/jEdit ***
  5175 
  5176 * New manual "jedit" for Isabelle/jEdit, see isabelle doc or
  5177 Documentation panel.
  5178 
  5179 * Dockable window "Documentation" provides access to Isabelle
  5180 documentation.
  5181 
  5182 * Dockable window "Find" provides query operations for formal entities
  5183 (GUI front-end to 'find_theorems' command).
  5184 
  5185 * Dockable window "Sledgehammer" manages asynchronous / parallel
  5186 sledgehammer runs over existing document sources, independently of
  5187 normal editing and checking process.
  5188 
  5189 * Dockable window "Timing" provides an overview of relevant command
  5190 timing information, depending on option jedit_timing_threshold.  The
  5191 same timing information is shown in the extended tooltip of the
  5192 command keyword, when hovering the mouse over it while the CONTROL or
  5193 COMMAND modifier is pressed.
  5194 
  5195 * Improved dockable window "Theories": Continuous checking of proof
  5196 document (visible and required parts) may be controlled explicitly,
  5197 using check box or shortcut "C+e ENTER".  Individual theory nodes may
  5198 be marked explicitly as required and checked in full, using check box
  5199 or shortcut "C+e SPACE".
  5200 
  5201 * Improved completion mechanism, which is now managed by the
  5202 Isabelle/jEdit plugin instead of SideKick.  Refined table of Isabelle
  5203 symbol abbreviations (see $ISABELLE_HOME/etc/symbols).
  5204 
  5205 * Standard jEdit keyboard shortcut C+b complete-word is remapped to
  5206 isabelle.complete for explicit completion in Isabelle sources.
  5207 INCOMPATIBILITY wrt. jEdit defaults, may have to invent new shortcuts
  5208 to resolve conflict.
  5209 
  5210 * Improved support of various "minor modes" for Isabelle NEWS,
  5211 options, session ROOT etc., with completion and SideKick tree view.
  5212 
  5213 * Strictly monotonic document update, without premature cancellation of
  5214 running transactions that are still needed: avoid reset/restart of
  5215 such command executions while editing.
  5216 
  5217 * Support for asynchronous print functions, as overlay to existing
  5218 document content.
  5219 
  5220 * Support for automatic tools in HOL, which try to prove or disprove
  5221 toplevel theorem statements.
  5222 
  5223 * Action isabelle.reset-font-size resets main text area font size
  5224 according to Isabelle/Scala plugin option "jedit_font_reset_size" (see
  5225 also "Plugin Options / Isabelle / General").  It can be bound to some
  5226 keyboard shortcut by the user (e.g. C+0 and/or C+NUMPAD0).
  5227 
  5228 * File specifications in jEdit (e.g. file browser) may refer to
  5229 $ISABELLE_HOME and $ISABELLE_HOME_USER on all platforms.  Discontinued
  5230 obsolete $ISABELLE_HOME_WINDOWS variable.
  5231 
  5232 * Improved support for Linux look-and-feel "GTK+", see also "Utilities
  5233 / Global Options / Appearance".
  5234 
  5235 * Improved support of native Mac OS X functionality via "MacOSX"
  5236 plugin, which is now enabled by default.
  5237 
  5238 
  5239 *** Pure ***
  5240 
  5241 * Commands 'interpretation' and 'sublocale' are now target-sensitive.
  5242 In particular, 'interpretation' allows for non-persistent
  5243 interpretation within "context ... begin ... end" blocks offering a
  5244 light-weight alternative to 'sublocale'.  See "isar-ref" manual for
  5245 details.
  5246 
  5247 * Improved locales diagnostic command 'print_dependencies'.
  5248 
  5249 * Discontinued obsolete 'axioms' command, which has been marked as
  5250 legacy since Isabelle2009-2.  INCOMPATIBILITY, use 'axiomatization'
  5251 instead, while observing its uniform scope for polymorphism.
  5252 
  5253 * Discontinued empty name bindings in 'axiomatization'.
  5254 INCOMPATIBILITY.
  5255 
  5256 * System option "proofs" has been discontinued.  Instead the global
  5257 state of Proofterm.proofs is persistently compiled into logic images
  5258 as required, notably HOL-Proofs.  Users no longer need to change
  5259 Proofterm.proofs dynamically.  Minor INCOMPATIBILITY.
  5260 
  5261 * Syntax translation functions (print_translation etc.) always depend
  5262 on Proof.context.  Discontinued former "(advanced)" option -- this is
  5263 now the default.  Minor INCOMPATIBILITY.
  5264 
  5265 * Former global reference trace_unify_fail is now available as
  5266 configuration option "unify_trace_failure" (global context only).
  5267 
  5268 * SELECT_GOAL now retains the syntactic context of the overall goal
  5269 state (schematic variables etc.).  Potential INCOMPATIBILITY in rare
  5270 situations.
  5271 
  5272 
  5273 *** HOL ***
  5274 
  5275 * Stronger precedence of syntax for big intersection and union on
  5276 sets, in accordance with corresponding lattice operations.
  5277 INCOMPATIBILITY.
  5278 
  5279 * Notation "{p:A. P}" now allows tuple patterns as well.
  5280 
  5281 * Nested case expressions are now translated in a separate check phase
  5282 rather than during parsing. The data for case combinators is separated
  5283 from the datatype package. The declaration attribute
  5284 "case_translation" can be used to register new case combinators:
  5285 
  5286   declare [[case_translation case_combinator constructor1 ... constructorN]]
  5287 
  5288 * Code generator:
  5289   - 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' /
  5290     'code_instance'.
  5291   - 'code_identifier' declares name hints for arbitrary identifiers in
  5292     generated code, subsuming 'code_modulename'.
  5293 
  5294 See the isar-ref manual for syntax diagrams, and the HOL theories for
  5295 examples.
  5296 
  5297 * Attibute 'code': 'code' now declares concrete and abstract code
  5298 equations uniformly.  Use explicit 'code equation' and 'code abstract'
  5299 to distinguish both when desired.
  5300 
  5301 * Discontinued theories Code_Integer and Efficient_Nat by a more
  5302 fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,
  5303 Code_Target_Nat and Code_Target_Numeral.  See the tutorial on code
  5304 generation for details.  INCOMPATIBILITY.
  5305 
  5306 * Numeric types are mapped by default to target language numerals:
  5307 natural (replaces former code_numeral) and integer (replaces former
  5308 code_int).  Conversions are available as integer_of_natural /
  5309 natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and
  5310 Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in
  5311 ML).  INCOMPATIBILITY.
  5312 
  5313 * Function package: For mutually recursive functions f and g, separate
  5314 cases rules f.cases and g.cases are generated instead of unusable
  5315 f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY,
  5316 in the case that the unusable rule was used nevertheless.
  5317 
  5318 * Function package: For each function f, new rules f.elims are
  5319 generated, which eliminate equalities of the form "f x = t".
  5320 
  5321 * New command 'fun_cases' derives ad-hoc elimination rules for
  5322 function equations as simplified instances of f.elims, analogous to
  5323 inductive_cases.  See ~~/src/HOL/ex/Fundefs.thy for some examples.
  5324 
  5325 * Lifting:
  5326   - parametrized correspondence relations are now supported:
  5327     + parametricity theorems for the raw term can be specified in
  5328       the command lift_definition, which allow us to generate stronger
  5329       transfer rules
  5330     + setup_lifting generates stronger transfer rules if parametric
  5331       correspondence relation can be generated
  5332     + various new properties of the relator must be specified to support
  5333       parametricity
  5334     + parametricity theorem for the Quotient relation can be specified
  5335   - setup_lifting generates domain rules for the Transfer package
  5336   - stronger reflexivity prover of respectfulness theorems for type
  5337     copies
  5338   - ===> and --> are now local. The symbols can be introduced
  5339     by interpreting the locale lifting_syntax (typically in an
  5340     anonymous context)
  5341   - Lifting/Transfer relevant parts of Library/Quotient_* are now in
  5342     Main. Potential INCOMPATIBILITY
  5343   - new commands for restoring and deleting Lifting/Transfer context:
  5344     lifting_forget, lifting_update
  5345   - the command print_quotmaps was renamed to print_quot_maps.
  5346     INCOMPATIBILITY
  5347 
  5348 * Transfer:
  5349   - better support for domains in Transfer: replace Domainp T
  5350     by the actual invariant in a transferred goal
  5351   - transfer rules can have as assumptions other transfer rules
  5352   - Experimental support for transferring from the raw level to the
  5353     abstract level: Transfer.transferred attribute
  5354   - Attribute version of the transfer method: untransferred attribute
  5355 
  5356 * Reification and reflection:
  5357   - Reification is now directly available in HOL-Main in structure
  5358     "Reification".
  5359   - Reflection now handles multiple lists with variables also.
  5360   - The whole reflection stack has been decomposed into conversions.
  5361 INCOMPATIBILITY.
  5362 
  5363 * Revised devices for recursive definitions over finite sets:
  5364   - Only one fundamental fold combinator on finite set remains:
  5365     Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b
  5366     This is now identity on infinite sets.
  5367   - Locales ("mini packages") for fundamental definitions with
  5368     Finite_Set.fold: folding, folding_idem.
  5369   - Locales comm_monoid_set, semilattice_order_set and
  5370     semilattice_neutr_order_set for big operators on sets.
  5371     See theory Big_Operators for canonical examples.
  5372     Note that foundational constants comm_monoid_set.F and
  5373     semilattice_set.F correspond to former combinators fold_image
  5374     and fold1 respectively.  These are now gone.  You may use
  5375     those foundational constants as substitutes, but it is
  5376     preferable to interpret the above locales accordingly.
  5377   - Dropped class ab_semigroup_idem_mult (special case of lattice,
  5378     no longer needed in connection with Finite_Set.fold etc.)
  5379   - Fact renames:
  5380       card.union_inter ~> card_Un_Int [symmetric]
  5381       card.union_disjoint ~> card_Un_disjoint
  5382 INCOMPATIBILITY.
  5383 
  5384 * Locale hierarchy for abstract orderings and (semi)lattices.
  5385 
  5386 * Complete_Partial_Order.admissible is defined outside the type class
  5387 ccpo, but with mandatory prefix ccpo. Admissibility theorems lose the
  5388 class predicate assumption or sort constraint when possible.
  5389 INCOMPATIBILITY.
  5390 
  5391 * Introduce type class "conditionally_complete_lattice": Like a
  5392 complete lattice but does not assume the existence of the top and
  5393 bottom elements.  Allows to generalize some lemmas about reals and
  5394 extended reals.  Removed SupInf and replaced it by the instantiation
  5395 of conditionally_complete_lattice for real. Renamed lemmas about
  5396 conditionally-complete lattice from Sup_... to cSup_... and from
  5397 Inf_...  to cInf_... to avoid hidding of similar complete lattice
  5398 lemmas.
  5399 
  5400 * Introduce type class linear_continuum as combination of
  5401 conditionally-complete lattices and inner dense linorders which have
  5402 more than one element.  INCOMPATIBILITY.
  5403 
  5404 * Introduced type classes order_top and order_bot. The old classes top
  5405 and bot only contain the syntax without assumptions.  INCOMPATIBILITY:
  5406 Rename bot -> order_bot, top -> order_top
  5407 
  5408 * Introduce type classes "no_top" and "no_bot" for orderings without
  5409 top and bottom elements.
  5410 
  5411 * Split dense_linorder into inner_dense_order and no_top, no_bot.
  5412 
  5413 * Complex_Main: Unify and move various concepts from
  5414 HOL-Multivariate_Analysis to HOL-Complex_Main.
  5415 
  5416  - Introduce type class (lin)order_topology and
  5417    linear_continuum_topology.  Allows to generalize theorems about
  5418    limits and order.  Instances are reals and extended reals.
  5419 
  5420  - continuous and continuos_on from Multivariate_Analysis:
  5421    "continuous" is the continuity of a function at a filter.  "isCont"
  5422    is now an abbrevitation: "isCont x f == continuous (at _) f".
  5423 
  5424    Generalized continuity lemmas from isCont to continuous on an
  5425    arbitrary filter.
  5426 
  5427  - compact from Multivariate_Analysis. Use Bolzano's lemma to prove
  5428    compactness of closed intervals on reals. Continuous functions
  5429    attain infimum and supremum on compact sets. The inverse of a
  5430    continuous function is continuous, when the function is continuous
  5431    on a compact set.
  5432 
  5433  - connected from Multivariate_Analysis. Use it to prove the
  5434    intermediate value theorem. Show connectedness of intervals on
  5435    linear_continuum_topology).
  5436 
  5437  - first_countable_topology from Multivariate_Analysis. Is used to
  5438    show equivalence of properties on the neighbourhood filter of x and
  5439    on all sequences converging to x.
  5440 
  5441  - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved
  5442    theorems from Library/FDERIV.thy to Deriv.thy and base the
  5443    definition of DERIV on FDERIV. Add variants of DERIV and FDERIV
  5444    which are restricted to sets, i.e. to represent derivatives from
  5445    left or right.
  5446 
  5447  - Removed the within-filter. It is replaced by the principal filter:
  5448 
  5449      F within X = inf F (principal X)
  5450 
  5451  - Introduce "at x within U" as a single constant, "at x" is now an
  5452    abbreviation for "at x within UNIV"
  5453 
  5454  - Introduce named theorem collections tendsto_intros,
  5455    continuous_intros, continuous_on_intros and FDERIV_intros. Theorems
  5456    in tendsto_intros (or FDERIV_intros) are also available as
  5457    tendsto_eq_intros (or FDERIV_eq_intros) where the right-hand side
  5458    is replaced by a congruence rule. This allows to apply them as
  5459    intro rules and then proving equivalence by the simplifier.
  5460 
  5461  - Restructured theories in HOL-Complex_Main:
  5462 
  5463    + Moved RealDef and RComplete into Real
  5464 
  5465    + Introduced Topological_Spaces and moved theorems about
  5466      topological spaces, filters, limits and continuity to it
  5467 
  5468    + Renamed RealVector to Real_Vector_Spaces
  5469 
  5470    + Split Lim, SEQ, Series into Topological_Spaces,
  5471      Real_Vector_Spaces, and Limits
  5472 
  5473    + Moved Ln and Log to Transcendental
  5474 
  5475    + Moved theorems about continuity from Deriv to Topological_Spaces
  5476 
  5477  - Remove various auxiliary lemmas.
  5478 
  5479 INCOMPATIBILITY.
  5480 
  5481 * Nitpick:
  5482   - Added option "spy".
  5483   - Reduce incidence of "too high arity" errors.
  5484 
  5485 * Sledgehammer:
  5486   - Renamed option:
  5487       isar_shrink ~> isar_compress
  5488     INCOMPATIBILITY.
  5489   - Added options "isar_try0", "spy".
  5490   - Better support for "isar_proofs".
  5491   - MaSh has been fined-tuned and now runs as a local server.
  5492 
  5493 * Improved support for ad hoc overloading of constants (see also
  5494 isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).
  5495 
  5496 * Library/Polynomial.thy:
  5497   - Use lifting for primitive definitions.
  5498   - Explicit conversions from and to lists of coefficients, used for
  5499     generated code.
  5500   - Replaced recursion operator poly_rec by fold_coeffs.
  5501   - Prefer pre-existing gcd operation for gcd.
  5502   - Fact renames:
  5503     poly_eq_iff ~> poly_eq_poly_eq_iff
  5504     poly_ext ~> poly_eqI
  5505     expand_poly_eq ~> poly_eq_iff
  5506 IMCOMPATIBILITY.
  5507 
  5508 * New Library/Simps_Case_Conv.thy: Provides commands simps_of_case and
  5509 case_of_simps to convert function definitions between a list of
  5510 equations with patterns on the lhs and a single equation with case
  5511 expressions on the rhs. See also Ex/Simps_Case_Conv_Examples.thy.
  5512 
  5513 * New Library/FSet.thy: type of finite sets defined as a subtype of
  5514 sets defined by Lifting/Transfer.
  5515 
  5516 * Discontinued theory src/HOL/Library/Eval_Witness.  INCOMPATIBILITY.
  5517 
  5518 * Consolidation of library theories on product orders:
  5519 
  5520     Product_Lattice ~> Product_Order -- pointwise order on products
  5521     Product_ord ~> Product_Lexorder -- lexicographic order on products
  5522 
  5523 INCOMPATIBILITY.
  5524 
  5525 * Imperative-HOL: The MREC combinator is considered legacy and no
  5526 longer included by default. INCOMPATIBILITY, use partial_function
  5527 instead, or import theory Legacy_Mrec as a fallback.
  5528 
  5529 * HOL-Algebra: Discontinued theories ~~/src/HOL/Algebra/abstract and
  5530 ~~/src/HOL/Algebra/poly.  Existing theories should be based on
  5531 ~~/src/HOL/Library/Polynomial instead.  The latter provides
  5532 integration with HOL's type classes for rings.  INCOMPATIBILITY.
  5533 
  5534 * HOL-BNF:
  5535   - Various improvements to BNF-based (co)datatype package, including
  5536     new commands "primrec_new", "primcorec", and
  5537     "datatype_new_compat", as well as documentation. See
  5538     "datatypes.pdf" for details.
  5539   - New "coinduction" method to avoid some boilerplate (compared to
  5540     coinduct).
  5541   - Renamed keywords:
  5542     data ~> datatype_new
  5543     codata ~> codatatype
  5544     bnf_def ~> bnf
  5545   - Renamed many generated theorems, including
  5546     discs ~> disc
  5547     map_comp' ~> map_comp
  5548     map_id' ~> map_id
  5549     sels ~> sel
  5550     set_map' ~> set_map
  5551     sets ~> set
  5552 IMCOMPATIBILITY.
  5553 
  5554 
  5555 *** ML ***
  5556 
  5557 * Spec_Check is a Quickcheck tool for Isabelle/ML.  The ML function
  5558 "check_property" allows to check specifications of the form "ALL x y
  5559 z. prop x y z".  See also ~~/src/Tools/Spec_Check/ with its
  5560 Examples.thy in particular.
  5561 
  5562 * Improved printing of exception trace in Poly/ML 5.5.1, with regular
  5563 tracing output in the command transaction context instead of physical
  5564 stdout.  See also Toplevel.debug, Toplevel.debugging and
  5565 ML_Compiler.exn_trace.
  5566 
  5567 * ML type "theory" is now immutable, without any special treatment of
  5568 drafts or linear updates (which could lead to "stale theory" errors in
  5569 the past).  Discontinued obsolete operations like Theory.copy,
  5570 Theory.checkpoint, and the auxiliary type theory_ref.  Minor
  5571 INCOMPATIBILITY.
  5572 
  5573 * More uniform naming of goal functions for skipped proofs:
  5574 
  5575     Skip_Proof.prove  ~>  Goal.prove_sorry
  5576     Skip_Proof.prove_global  ~>  Goal.prove_sorry_global
  5577 
  5578 Minor INCOMPATIBILITY.
  5579 
  5580 * Simplifier tactics and tools use proper Proof.context instead of
  5581 historic type simpset.  Old-style declarations like addsimps,
  5582 addsimprocs etc. operate directly on Proof.context.  Raw type simpset
  5583 retains its use as snapshot of the main Simplifier context, using
  5584 simpset_of and put_simpset on Proof.context.  INCOMPATIBILITY -- port
  5585 old tools by making them depend on (ctxt : Proof.context) instead of
  5586 (ss : simpset), then turn (simpset_of ctxt) into ctxt.
  5587 
  5588 * Modifiers for classical wrappers (e.g. addWrapper, delWrapper)
  5589 operate on Proof.context instead of claset, for uniformity with addIs,
  5590 addEs, addDs etc. Note that claset_of and put_claset allow to manage
  5591 clasets separately from the context.
  5592 
  5593 * Discontinued obsolete ML antiquotations @{claset} and @{simpset}.
  5594 INCOMPATIBILITY, use @{context} instead.
  5595 
  5596 * Antiquotation @{theory_context A} is similar to @{theory A}, but
  5597 presents the result as initial Proof.context.
  5598 
  5599 
  5600 *** System ***
  5601 
  5602 * Discontinued obsolete isabelle usedir, mkdir, make -- superseded by
  5603 "isabelle build" in Isabelle2013.  INCOMPATIBILITY.
  5604 
  5605 * Discontinued obsolete isabelle-process options -f and -u (former
  5606 administrative aliases of option -e).  Minor INCOMPATIBILITY.
  5607 
  5608 * Discontinued obsolete isabelle print tool, and PRINT_COMMAND
  5609 settings variable.
  5610 
  5611 * Discontinued ISABELLE_DOC_FORMAT settings variable and historic
  5612 document formats: dvi.gz, ps, ps.gz -- the default document format is
  5613 always pdf.
  5614 
  5615 * Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to
  5616 specify global resources of the JVM process run by isabelle build.
  5617 
  5618 * Toplevel executable $ISABELLE_HOME/bin/isabelle_scala_script allows
  5619 to run Isabelle/Scala source files as standalone programs.
  5620 
  5621 * Improved "isabelle keywords" tool (for old-style ProofGeneral
  5622 keyword tables): use Isabelle/Scala operations, which inspect outer
  5623 syntax without requiring to build sessions first.
  5624 
  5625 * Sessions may be organized via 'chapter' specifications in the ROOT
  5626 file, which determines a two-level hierarchy of browser info.  The old
  5627 tree-like organization via implicit sub-session relation (with its
  5628 tendency towards erratic fluctuation of URLs) has been discontinued.
  5629 The default chapter is called "Unsorted".  Potential INCOMPATIBILITY
  5630 for HTML presentation of theories.
  5631 
  5632 
  5633 
  5634 New in Isabelle2013 (February 2013)
  5635 -----------------------------------
  5636 
  5637 *** General ***
  5638 
  5639 * Theorem status about oracles and unfinished/failed future proofs is
  5640 no longer printed by default, since it is incompatible with
  5641 incremental / parallel checking of the persistent document model.  ML
  5642 function Thm.peek_status may be used to inspect a snapshot of the
  5643 ongoing evaluation process.  Note that in batch mode --- notably
  5644 isabelle build --- the system ensures that future proofs of all
  5645 accessible theorems in the theory context are finished (as before).
  5646 
  5647 * Configuration option show_markup controls direct inlining of markup
  5648 into the printed representation of formal entities --- notably type
  5649 and sort constraints.  This enables Prover IDE users to retrieve that
  5650 information via tooltips in the output window, for example.
  5651 
  5652 * Command 'ML_file' evaluates ML text from a file directly within the
  5653 theory, without any predeclaration via 'uses' in the theory header.
  5654 
  5655 * Old command 'use' command and corresponding keyword 'uses' in the
  5656 theory header are legacy features and will be discontinued soon.
  5657 Tools that load their additional source files may imitate the
  5658 'ML_file' implementation, such that the system can take care of
  5659 dependencies properly.
  5660 
  5661 * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which
  5662 is called fastforce / fast_force_tac already since Isabelle2011-1.
  5663 
  5664 * Updated and extended "isar-ref" and "implementation" manual, reduced
  5665 remaining material in old "ref" manual.
  5666 
  5667 * Improved support for auxiliary contexts that indicate block structure
  5668 for specifications.  Nesting of "context fixes ... context assumes ..."
  5669 and "class ... context ...".
  5670 
  5671 * Attribute "consumes" allows a negative value as well, which is
  5672 interpreted relatively to the total number of premises of the rule in
  5673 the target context.  This form of declaration is stable when exported
  5674 from a nested 'context' with additional assumptions.  It is the
  5675 preferred form for definitional packages, notably cases/rules produced
  5676 in HOL/inductive and HOL/function.
  5677 
  5678 * More informative error messages for Isar proof commands involving
  5679 lazy enumerations (method applications etc.).
  5680 
  5681 * Refined 'help' command to retrieve outer syntax commands according
  5682 to name patterns (with clickable results).
  5683 
  5684 
  5685 *** Prover IDE -- Isabelle/Scala/jEdit ***
  5686 
  5687 * Parallel terminal proofs ('by') are enabled by default, likewise
  5688 proofs that are built into packages like 'datatype', 'function'.  This
  5689 allows to "run ahead" checking the theory specifications on the
  5690 surface, while the prover is still crunching on internal
  5691 justifications.  Unfinished / cancelled proofs are restarted as
  5692 required to complete full proof checking eventually.
  5693 
  5694 * Improved output panel with tooltips, hyperlinks etc. based on the
  5695 same Rich_Text_Area as regular Isabelle/jEdit buffers.  Activation of
  5696 tooltips leads to some window that supports the same recursively,
  5697 which can lead to stacks of tooltips as the semantic document content
  5698 is explored.  ESCAPE closes the whole stack, individual windows may be
  5699 closed separately, or detached to become independent jEdit dockables.
  5700 
  5701 * Improved support for commands that produce graph output: the text
  5702 message contains a clickable area to open a new instance of the graph
  5703 browser on demand.
  5704 
  5705 * More robust incremental parsing of outer syntax (partial comments,
  5706 malformed symbols).  Changing the balance of open/close quotes and
  5707 comment delimiters works more conveniently with unfinished situations
  5708 that frequently occur in user interaction.
  5709 
  5710 * More efficient painting and improved reactivity when editing large
  5711 files.  More scalable management of formal document content.
  5712 
  5713 * Smarter handling of tracing messages: prover process pauses after
  5714 certain number of messages per command transaction, with some user
  5715 dialog to stop or continue.  This avoids swamping the front-end with
  5716 potentially infinite message streams.
  5717 
  5718 * More plugin options and preferences, based on Isabelle/Scala.  The
  5719 jEdit plugin option panel provides access to some Isabelle/Scala
  5720 options, including tuning parameters for editor reactivity and color
  5721 schemes.
  5722 
  5723 * Dockable window "Symbols" provides some editing support for Isabelle
  5724 symbols.
  5725 
  5726 * Dockable window "Monitor" shows ML runtime statistics.  Note that
  5727 continuous display of the chart slows down the system.
  5728 
  5729 * Improved editing support for control styles: subscript, superscript,
  5730 bold, reset of style -- operating on single symbols or text
  5731 selections.  Cf. keyboard shortcuts C+e DOWN/UP/RIGHT/LEFT.
  5732 
  5733 * Actions isabelle.increase-font-size and isabelle.decrease-font-size
  5734 adjust the main text area font size, and its derivatives for output,
  5735 tooltips etc.  Cf. keyboard shortcuts C-PLUS and C-MINUS, which often
  5736 need to be adapted to local keyboard layouts.
  5737 
  5738 * More reactive completion popup by default: use \t (TAB) instead of
  5739 \n (NEWLINE) to minimize intrusion into regular flow of editing.  See
  5740 also "Plugin Options / SideKick / General / Code Completion Options".
  5741 
  5742 * Implicit check and build dialog of the specified logic session
  5743 image.  For example, HOL, HOLCF, HOL-Nominal can be produced on
  5744 demand, without bundling big platform-dependent heap images in the
  5745 Isabelle distribution.
  5746 
  5747 * Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates
  5748 from Oracle provide better multi-platform experience.  This version is
  5749 now bundled exclusively with Isabelle.
  5750 
  5751 
  5752 *** Pure ***
  5753 
  5754 * Code generation for Haskell: restrict unqualified imports from
  5755 Haskell Prelude to a small set of fundamental operations.
  5756 
  5757 * Command 'export_code': relative file names are interpreted
  5758 relatively to master directory of current theory rather than the
  5759 rather arbitrary current working directory.  INCOMPATIBILITY.
  5760 
  5761 * Discontinued obsolete attribute "COMP".  Potential INCOMPATIBILITY,
  5762 use regular rule composition via "OF" / "THEN", or explicit proof
  5763 structure instead.  Note that Isabelle/ML provides a variety of
  5764 operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
  5765 with some care where this is really required.
  5766 
  5767 * Command 'typ' supports an additional variant with explicit sort
  5768 constraint, to infer and check the most general type conforming to a
  5769 given sort.  Example (in HOL):
  5770 
  5771   typ "_ * _ * bool * unit" :: finite
  5772 
  5773 * Command 'locale_deps' visualizes all locales and their relations as
  5774 a Hasse diagram.
  5775 
  5776 
  5777 *** HOL ***
  5778 
  5779 * Sledgehammer:
  5780 
  5781   - Added MaSh relevance filter based on machine-learning; see the
  5782     Sledgehammer manual for details.
  5783   - Polished Isar proofs generated with "isar_proofs" option.
  5784   - Rationalized type encodings ("type_enc" option).
  5785   - Renamed "kill_provers" subcommand to "kill_all".
  5786   - Renamed options:
  5787       isar_proof ~> isar_proofs
  5788       isar_shrink_factor ~> isar_shrink
  5789       max_relevant ~> max_facts
  5790       relevance_thresholds ~> fact_thresholds
  5791 
  5792 * Quickcheck: added an optimisation for equality premises.  It is
  5793 switched on by default, and can be switched off by setting the
  5794 configuration quickcheck_optimise_equality to false.
  5795 
  5796 * Quotient: only one quotient can be defined by quotient_type
  5797 INCOMPATIBILITY.
  5798 
  5799 * Lifting:
  5800   - generation of an abstraction function equation in lift_definition
  5801   - quot_del attribute
  5802   - renamed no_abs_code -> no_code (INCOMPATIBILITY.)
  5803 
  5804 * Simproc "finite_Collect" rewrites set comprehensions into pointfree
  5805 expressions.
  5806 
  5807 * Preprocessing of the code generator rewrites set comprehensions into
  5808 pointfree expressions.
  5809 
  5810 * The SMT solver Z3 has now by default a restricted set of directly
  5811 supported features. For the full set of features (div/mod, nonlinear
  5812 arithmetic, datatypes/records) with potential proof reconstruction
  5813 failures, enable the configuration option "z3_with_extensions".  Minor
  5814 INCOMPATIBILITY.
  5815 
  5816 * Simplified 'typedef' specifications: historical options for implicit
  5817 set definition and alternative name have been discontinued.  The
  5818 former behavior of "typedef (open) t = A" is now the default, but
  5819 written just "typedef t = A".  INCOMPATIBILITY, need to adapt theories
  5820 accordingly.
  5821 
  5822 * Removed constant "chars"; prefer "Enum.enum" on type "char"
  5823 directly.  INCOMPATIBILITY.
  5824 
  5825 * Moved operation product, sublists and n_lists from theory Enum to
  5826 List.  INCOMPATIBILITY.
  5827 
  5828 * Theorem UN_o generalized to SUP_comp.  INCOMPATIBILITY.
  5829 
  5830 * Class "comm_monoid_diff" formalises properties of bounded
  5831 subtraction, with natural numbers and multisets as typical instances.
  5832 
  5833 * Added combinator "Option.these" with type "'a option set => 'a set".
  5834 
  5835 * Theory "Transitive_Closure": renamed lemmas
  5836 
  5837   reflcl_tranclp -> reflclp_tranclp
  5838   rtranclp_reflcl -> rtranclp_reflclp
  5839 
  5840 INCOMPATIBILITY.
  5841 
  5842 * Theory "Rings": renamed lemmas (in class semiring)
  5843 
  5844   left_distrib ~> distrib_right
  5845   right_distrib ~> distrib_left
  5846 
  5847 INCOMPATIBILITY.
  5848 
  5849 * Generalized the definition of limits:
  5850 
  5851   - Introduced the predicate filterlim (LIM x F. f x :> G) which
  5852     expresses that when the input values x converge to F then the
  5853     output f x converges to G.
  5854 
  5855   - Added filters for convergence to positive (at_top) and negative
  5856     infinity (at_bot).
  5857 
  5858   - Moved infinity in the norm (at_infinity) from
  5859     Multivariate_Analysis to Complex_Main.
  5860 
  5861   - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :>
  5862     at_top".
  5863 
  5864 INCOMPATIBILITY.
  5865 
  5866 * Theory "Library/Option_ord" provides instantiation of option type to
  5867 lattice type classes.
  5868 
  5869 * Theory "Library/Multiset": renamed
  5870 
  5871     constant fold_mset ~> Multiset.fold
  5872     fact fold_mset_commute ~> fold_mset_comm
  5873 
  5874 INCOMPATIBILITY.
  5875 
  5876 * Renamed theory Library/List_Prefix to Library/Sublist, with related
  5877 changes as follows.
  5878 
  5879   - Renamed constants (and related lemmas)
  5880 
  5881       prefix ~> prefixeq
  5882       strict_prefix ~> prefix
  5883 
  5884   - Replaced constant "postfix" by "suffixeq" with swapped argument
  5885     order (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped
  5886     old infix syntax "xs >>= ys"; use "suffixeq ys xs" instead.
  5887     Renamed lemmas accordingly.
  5888 
  5889   - Added constant "list_hembeq" for homeomorphic embedding on
  5890     lists. Added abbreviation "sublisteq" for special case
  5891     "list_hembeq (op =)".
  5892 
  5893   - Theory Library/Sublist no longer provides "order" and "bot" type
  5894     class instances for the prefix order (merely corresponding locale
  5895     interpretations). The type class instances are now in theory
  5896     Library/Prefix_Order.
  5897 
  5898   - The sublist relation of theory Library/Sublist_Order is now based
  5899     on "Sublist.sublisteq".  Renamed lemmas accordingly:
  5900 
  5901       le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff
  5902       le_list_append_mono ~> Sublist.list_hembeq_append_mono
  5903       le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2
  5904       le_list_Cons_EX ~> Sublist.list_hembeq_ConsD
  5905       le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2'
  5906       le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq
  5907       le_list_drop_Cons ~> Sublist.sublisteq_Cons'
  5908       le_list_drop_many ~> Sublist.sublisteq_drop_many
  5909       le_list_filter_left ~> Sublist.sublisteq_filter_left
  5910       le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many
  5911       le_list_rev_take_iff ~> Sublist.sublisteq_append
  5912       le_list_same_length ~> Sublist.sublisteq_same_length
  5913       le_list_take_many_iff ~> Sublist.sublisteq_append'
  5914       less_eq_list.drop ~> less_eq_list_drop
  5915       less_eq_list.induct ~> less_eq_list_induct
  5916       not_le_list_length ~> Sublist.not_sublisteq_length
  5917 
  5918 INCOMPATIBILITY.
  5919 
  5920 * New theory Library/Countable_Set.
  5921 
  5922 * Theory Library/Debug and Library/Parallel provide debugging and
  5923 parallel execution for code generated towards Isabelle/ML.
  5924 
  5925 * Theory Library/FuncSet: Extended support for Pi and extensional and
  5926 introduce the extensional dependent function space "PiE". Replaced
  5927 extensional_funcset by an abbreviation, and renamed lemmas from
  5928 extensional_funcset to PiE as follows:
  5929 
  5930   extensional_empty  ~>  PiE_empty
  5931   extensional_funcset_empty_domain  ~>  PiE_empty_domain
  5932   extensional_funcset_empty_range  ~>  PiE_empty_range
  5933   extensional_funcset_arb  ~>  PiE_arb
  5934   extensional_funcset_mem  ~>  PiE_mem
  5935   extensional_funcset_extend_domainI  ~>  PiE_fun_upd
  5936   extensional_funcset_restrict_domain  ~>  fun_upd_in_PiE
  5937   extensional_funcset_extend_domain_eq  ~>  PiE_insert_eq
  5938   card_extensional_funcset  ~>  card_PiE
  5939   finite_extensional_funcset  ~>  finite_PiE
  5940 
  5941 INCOMPATIBILITY.
  5942 
  5943 * Theory Library/FinFun: theory of almost everywhere constant
  5944 functions (supersedes the AFP entry "Code Generation for Functions as
  5945 Data").
  5946 
  5947 * Theory Library/Phantom: generic phantom type to make a type
  5948 parameter appear in a constant's type.  This alternative to adding
  5949 TYPE('a) as another parameter avoids unnecessary closures in generated
  5950 code.
  5951 
  5952 * Theory Library/RBT_Impl: efficient construction of red-black trees
  5953 from sorted associative lists. Merging two trees with rbt_union may
  5954 return a structurally different tree than before.  Potential
  5955 INCOMPATIBILITY.
  5956 
  5957 * Theory Library/IArray: immutable arrays with code generation.
  5958 
  5959 * Theory Library/Finite_Lattice: theory of finite lattices.
  5960 
  5961 * HOL/Multivariate_Analysis: replaced
  5962 
  5963   "basis :: 'a::euclidean_space => nat => real"
  5964   "\<Chi>\<Chi> :: (nat => real) => 'a::euclidean_space"
  5965 
  5966 on euclidean spaces by using the inner product "_ \<bullet> _" with
  5967 vectors from the Basis set: "\<Chi>\<Chi> i. f i" is superseded by
  5968 "SUM i : Basis. f i * r i".
  5969 
  5970   With this change the following constants are also changed or removed:
  5971 
  5972     DIM('a) :: nat  ~>  card (Basis :: 'a set)   (is an abbreviation)
  5973     a $$ i  ~>  inner a i  (where i : Basis)
  5974     cart_base i  removed
  5975     \<pi>, \<pi>'  removed
  5976 
  5977   Theorems about these constants where removed.
  5978 
  5979   Renamed lemmas:
  5980 
  5981     component_le_norm  ~>  Basis_le_norm
  5982     euclidean_eq  ~>  euclidean_eq_iff
  5983     differential_zero_maxmin_component  ~>  differential_zero_maxmin_cart
  5984     euclidean_simps  ~>  inner_simps
  5985     independent_basis  ~>  independent_Basis
  5986     span_basis  ~>  span_Basis
  5987     in_span_basis  ~>  in_span_Basis
  5988     norm_bound_component_le  ~>  norm_boound_Basis_le
  5989     norm_bound_component_lt  ~>  norm_boound_Basis_lt
  5990     component_le_infnorm  ~>  Basis_le_infnorm
  5991 
  5992 INCOMPATIBILITY.
  5993 
  5994 * HOL/Probability:
  5995 
  5996   - Added simproc "measurable" to automatically prove measurability.
  5997 
  5998   - Added induction rules for sigma sets with disjoint union
  5999     (sigma_sets_induct_disjoint) and for Borel-measurable functions
  6000     (borel_measurable_induct).
  6001 
  6002   - Added the Daniell-Kolmogorov theorem (the existence the limit of a
  6003     projective family).
  6004 
  6005 * HOL/Cardinals: Theories of ordinals and cardinals (supersedes the
  6006 AFP entry "Ordinals_and_Cardinals").
  6007 
  6008 * HOL/BNF: New (co)datatype package based on bounded natural functors
  6009 with support for mixed, nested recursion and interesting non-free
  6010 datatypes.
  6011 
  6012 * HOL/Finite_Set and Relation: added new set and relation operations
  6013 expressed by Finite_Set.fold.
  6014 
  6015 * New theory HOL/Library/RBT_Set: implementation of sets by red-black
  6016 trees for the code generator.
  6017 
  6018 * HOL/Library/RBT and HOL/Library/Mapping have been converted to
  6019 Lifting/Transfer.
  6020 possible INCOMPATIBILITY.
  6021 
  6022 * HOL/Set: renamed Set.project -> Set.filter
  6023 INCOMPATIBILITY.
  6024 
  6025 
  6026 *** Document preparation ***
  6027 
  6028 * Dropped legacy antiquotations "term_style" and "thm_style", since
  6029 styles may be given as arguments to "term" and "thm" already.
  6030 Discontinued legacy styles "prem1" .. "prem19".
  6031 
  6032 * Default LaTeX rendering for \<euro> is now based on eurosym package,
  6033 instead of slightly exotic babel/greek.
  6034 
  6035 * Document variant NAME may use different LaTeX entry point
  6036 document/root_NAME.tex if that file exists, instead of the common
  6037 document/root.tex.
  6038 
  6039 * Simplified custom document/build script, instead of old-style
  6040 document/IsaMakefile.  Minor INCOMPATIBILITY.
  6041 
  6042 
  6043 *** ML ***
  6044 
  6045 * The default limit for maximum number of worker threads is now 8,
  6046 instead of 4, in correspondence to capabilities of contemporary
  6047 hardware and Poly/ML runtime system.
  6048 
  6049 * Type Seq.results and related operations support embedded error
  6050 messages within lazy enumerations, and thus allow to provide
  6051 informative errors in the absence of any usable results.
  6052 
  6053 * Renamed Position.str_of to Position.here to emphasize that this is a
  6054 formal device to inline positions into message text, but not
  6055 necessarily printing visible text.
  6056 
  6057 
  6058 *** System ***
  6059 
  6060 * Advanced support for Isabelle sessions and build management, see
  6061 "system" manual for the chapter of that name, especially the "isabelle
  6062 build" tool and its examples.  The "isabelle mkroot" tool prepares
  6063 session root directories for use with "isabelle build", similar to
  6064 former "isabelle mkdir" for "isabelle usedir".  Note that this affects
  6065 document preparation as well.  INCOMPATIBILITY, isabelle usedir /
  6066 mkdir / make are rendered obsolete.
  6067 
  6068 * Discontinued obsolete Isabelle/build script, it is superseded by the
  6069 regular isabelle build tool.  For example:
  6070 
  6071   isabelle build -s -b HOL
  6072 
  6073 * Discontinued obsolete "isabelle makeall".
  6074 
  6075 * Discontinued obsolete IsaMakefile and ROOT.ML files from the
  6076 Isabelle distribution, except for rudimentary src/HOL/IsaMakefile that
  6077 provides some traditional targets that invoke "isabelle build".  Note
  6078 that this is inefficient!  Applications of Isabelle/HOL involving
  6079 "isabelle make" should be upgraded to use "isabelle build" directly.
  6080 
  6081 * The "isabelle options" tool prints Isabelle system options, as
  6082 required for "isabelle build", for example.
  6083 
  6084 * The "isabelle logo" tool produces EPS and PDF format simultaneously.
  6085 Minor INCOMPATIBILITY in command-line options.
  6086 
  6087 * The "isabelle install" tool has now a simpler command-line.  Minor
  6088 INCOMPATIBILITY.
  6089 
  6090 * The "isabelle components" tool helps to resolve add-on components
  6091 that are not bundled, or referenced from a bare-bones repository
  6092 version of Isabelle.
  6093 
  6094 * Settings variable ISABELLE_PLATFORM_FAMILY refers to the general
  6095 platform family: "linux", "macos", "windows".
  6096 
  6097 * The ML system is configured as regular component, and no longer
  6098 picked up from some surrounding directory.  Potential INCOMPATIBILITY
  6099 for home-made settings.
  6100 
  6101 * Improved ML runtime statistics (heap, threads, future tasks etc.).
  6102 
  6103 * Discontinued support for Poly/ML 5.2.1, which was the last version
  6104 without exception positions and advanced ML compiler/toplevel
  6105 configuration.
  6106 
  6107 * Discontinued special treatment of Proof General -- no longer guess
  6108 PROOFGENERAL_HOME based on accidental file-system layout.  Minor
  6109 INCOMPATIBILITY: provide PROOFGENERAL_HOME and PROOFGENERAL_OPTIONS
  6110 settings manually, or use a Proof General version that has been
  6111 bundled as Isabelle component.
  6112 
  6113 
  6114 
  6115 New in Isabelle2012 (May 2012)
  6116 ------------------------------
  6117 
  6118 *** General ***
  6119 
  6120 * Prover IDE (PIDE) improvements:
  6121 
  6122   - more robust Sledgehammer integration (as before the sledgehammer
  6123     command-line needs to be typed into the source buffer)
  6124   - markup for bound variables
  6125   - markup for types of term variables (displayed as tooltips)
  6126   - support for user-defined Isar commands within the running session
  6127   - improved support for Unicode outside original 16bit range
  6128     e.g. glyph for \<A> (thanks to jEdit 4.5.1)
  6129 
  6130 * Forward declaration of outer syntax keywords within the theory
  6131 header -- minor INCOMPATIBILITY for user-defined commands.  Allow new
  6132 commands to be used in the same theory where defined.
  6133 
  6134 * Auxiliary contexts indicate block structure for specifications with
  6135 additional parameters and assumptions.  Such unnamed contexts may be
  6136 nested within other targets, like 'theory', 'locale', 'class',
  6137 'instantiation' etc.  Results from the local context are generalized
  6138 accordingly and applied to the enclosing target context.  Example:
  6139 
  6140   context
  6141     fixes x y z :: 'a
  6142     assumes xy: "x = y" and yz: "y = z"
  6143   begin
  6144 
  6145   lemma my_trans: "x = z" using xy yz by simp
  6146 
  6147   end
  6148 
  6149   thm my_trans
  6150 
  6151 The most basic application is to factor-out context elements of
  6152 several fixes/assumes/shows theorem statements, e.g. see
  6153 ~~/src/HOL/Isar_Examples/Group_Context.thy
  6154 
  6155 Any other local theory specification element works within the "context
  6156 ... begin ... end" block as well.
  6157 
  6158 * Bundled declarations associate attributed fact expressions with a
  6159 given name in the context.  These may be later included in other
  6160 contexts.  This allows to manage context extensions casually, without
  6161 the logical dependencies of locales and locale interpretation.  See
  6162 commands 'bundle', 'include', 'including' etc. in the isar-ref manual.
  6163 
  6164 * Commands 'lemmas' and 'theorems' allow local variables using 'for'
  6165 declaration, and results are standardized before being stored.  Thus
  6166 old-style "standard" after instantiation or composition of facts
  6167 becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of
  6168 indices of schematic variables.
  6169 
  6170 * Rule attributes in local theory declarations (e.g. locale or class)
  6171 are now statically evaluated: the resulting theorem is stored instead
  6172 of the original expression.  INCOMPATIBILITY in rare situations, where
  6173 the historic accident of dynamic re-evaluation in interpretations
  6174 etc. was exploited.
  6175 
  6176 * New tutorial "Programming and Proving in Isabelle/HOL"
  6177 ("prog-prove").  It completely supersedes "A Tutorial Introduction to
  6178 Structured Isar Proofs" ("isar-overview"), which has been removed.  It
  6179 also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order
  6180 Logic" as the recommended beginners tutorial, but does not cover all
  6181 of the material of that old tutorial.
  6182 
  6183 * Updated and extended reference manuals: "isar-ref",
  6184 "implementation", "system"; reduced remaining material in old "ref"
  6185 manual.
  6186 
  6187 
  6188 *** Pure ***
  6189 
  6190 * Command 'definition' no longer exports the foundational "raw_def"
  6191 into the user context.  Minor INCOMPATIBILITY, may use the regular
  6192 "def" result with attribute "abs_def" to imitate the old version.
  6193 
  6194 * Attribute "abs_def" turns an equation of the form "f x y == t" into
  6195 "f == %x y. t", which ensures that "simp" or "unfold" steps always
  6196 expand it.  This also works for object-logic equality.  (Formerly
  6197 undocumented feature.)
  6198 
  6199 * Sort constraints are now propagated in simultaneous statements, just
  6200 like type constraints.  INCOMPATIBILITY in rare situations, where
  6201 distinct sorts used to be assigned accidentally.  For example:
  6202 
  6203   lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"
  6204 
  6205   lemma "P (x::'a)" and "Q (y::'a::bar)"
  6206     -- "now uniform 'a::bar instead of default sort for first occurrence (!)"
  6207 
  6208 * Rule composition via attribute "OF" (or ML functions OF/MRS) is more
  6209 tolerant against multiple unifiers, as long as the final result is
  6210 unique.  (As before, rules are composed in canonical right-to-left
  6211 order to accommodate newly introduced premises.)
  6212 
  6213 * Renamed some inner syntax categories:
  6214 
  6215     num ~> num_token
  6216     xnum ~> xnum_token
  6217     xstr ~> str_token
  6218 
  6219 Minor INCOMPATIBILITY.  Note that in practice "num_const" or
  6220 "num_position" etc. are mainly used instead (which also include
  6221 position information via constraints).
  6222 
  6223 * Simplified configuration options for syntax ambiguity: see
  6224 "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
  6225 manual.  Minor INCOMPATIBILITY.
  6226 
  6227 * Discontinued configuration option "syntax_positions": atomic terms
  6228 in parse trees are always annotated by position constraints.
  6229 
  6230 * Old code generator for SML and its commands 'code_module',
  6231 'code_library', 'consts_code', 'types_code' have been discontinued.
  6232 Use commands of the generic code generator instead.  INCOMPATIBILITY.
  6233 
  6234 * Redundant attribute "code_inline" has been discontinued. Use
  6235 "code_unfold" instead.  INCOMPATIBILITY.
  6236 
  6237 * Dropped attribute "code_unfold_post" in favor of the its dual
  6238 "code_abbrev", which yields a common pattern in definitions like
  6239 
  6240   definition [code_abbrev]: "f = t"
  6241 
  6242 INCOMPATIBILITY.
  6243 
  6244 * Obsolete 'types' command has been discontinued.  Use 'type_synonym'
  6245 instead.  INCOMPATIBILITY.
  6246 
  6247 * Discontinued old "prems" fact, which used to refer to the accidental
  6248 collection of foundational premises in the context (already marked as
  6249 legacy since Isabelle2011).
  6250 
  6251 
  6252 *** HOL ***
  6253 
  6254 * Type 'a set is now a proper type constructor (just as before
  6255 Isabelle2008).  Definitions mem_def and Collect_def have disappeared.
  6256 Non-trivial INCOMPATIBILITY.  For developments keeping predicates and
  6257 sets separate, it is often sufficient to rephrase some set S that has
  6258 been accidentally used as predicates by "%x. x : S", and some
  6259 predicate P that has been accidentally used as set by "{x. P x}".
  6260 Corresponding proofs in a first step should be pruned from any
  6261 tinkering with former theorems mem_def and Collect_def as far as