NEWS
author wenzelm
Wed Oct 14 14:21:00 2015 +0200 (2015-10-14)
changeset 61437 8bb17fd2fa81
parent 61426 d53db136e8fd
child 61461 77c9643a6353
permissions -rw-r--r--
clarified control symbols;
     1 Isabelle NEWS -- history of user-relevant changes
     2 =================================================
     3 
     4 (Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.)
     5 
     6 
     7 New in this Isabelle version
     8 ----------------------------
     9 
    10 *** General ***
    11 
    12 * Toplevel theorem statements have been simplified as follows:
    13 
    14   theorems             ~>  lemmas
    15   schematic_lemma      ~>  schematic_goal
    16   schematic_theorem    ~>  schematic_goal
    17   schematic_corollary  ~>  schematic_goal
    18 
    19 Command-line tool "isabelle update_theorems" updates theory sources
    20 accordingly.
    21 
    22 * Toplevel theorem statement 'proposition' is another alias for
    23 'theorem'.
    24 
    25 * HTML presentation uses the standard IsabelleText font and Unicode
    26 rendering of Isabelle symbols like Isabelle/Scala/jEdit.  The former
    27 print mode "HTML" looses its special meaning.
    28 
    29 
    30 *** Prover IDE -- Isabelle/Scala/jEdit ***
    31 
    32 * Improved scheduling for urgent print tasks (e.g. command state output,
    33 interactive queries) wrt. long-running background tasks.
    34 
    35 * IDE support for the source-level debugger of Poly/ML, to work with
    36 Isabelle/ML and official Standard ML. Configuration option "ML_debugger"
    37 and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',
    38 'SML_file_no_debug' control compilation of sources with debugging
    39 information. The Debugger panel allows to set breakpoints (via context
    40 menu), step through stopped threads, evaluate local ML expressions etc.
    41 At least one Debugger view needs to be active to have any effect on the
    42 running ML program.
    43 
    44 * The main Isabelle executable is managed as single-instance Desktop
    45 application uniformly on all platforms: Linux, Windows, Mac OS X.
    46 
    47 * The text overview column (status of errors, warnings etc.) is updated
    48 asynchronously, leading to much better editor reactivity. Moreover, the
    49 full document node content is taken into account.
    50 
    51 * The State panel manages explicit proof state output, with jEdit action
    52 "isabelle.update-state" (shortcut S+ENTER) to trigger update according
    53 to cursor position. Option "editor_output_state" controls implicit proof
    54 state output in the Output panel: suppressing this reduces resource
    55 requirements of prover time and GUI space.
    56 
    57 
    58 *** Document preparation ***
    59 
    60 * Isabelle control symbols for markup and formatting:
    61 
    62   \<^noindent>   \noindent
    63   \<^smallskip>   \smallskip
    64   \<^medskip>   \medskip
    65   \<^bigskip>   \bigskip
    66 
    67   \<^item>  \item  (itemize)
    68   \<^enum>  \item  (enumerate)
    69   \<^descr>  \item  (description)
    70 
    71 
    72 *** Isar ***
    73 
    74 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the
    75 proof body as well, abstracted over relevant parameters.
    76 
    77 * Improved type-inference for theorem statement 'obtains': separate
    78 parameter scope for of each clause.
    79 
    80 * Term abbreviations via 'is' patterns also work for schematic
    81 statements: result is abstracted over unknowns.
    82 
    83 * Local goals ('have', 'show', 'hence', 'thus') allow structured
    84 statements like fixes/assumes/shows in theorem specifications, but the
    85 notation is postfix with keywords 'if' (or 'when') and 'for'. For
    86 example:
    87 
    88   have result: "C x y"
    89     if "A x" and "B y"
    90     for x :: 'a and y :: 'a
    91     <proof>
    92 
    93 The local assumptions are bound to the name "that". The result is
    94 exported from context of the statement as usual. The above roughly
    95 corresponds to a raw proof block like this:
    96 
    97   {
    98     fix x :: 'a and y :: 'a
    99     assume that: "A x" "B y"
   100     have "C x y" <proof>
   101   }
   102   note result = this
   103 
   104 The keyword 'when' may be used instead of 'if', to indicate 'presume'
   105 instead of 'assume' above.
   106 
   107 * The meaning of 'show' with Pure rule statements has changed: premises
   108 are treated in the sense of 'assume', instead of 'presume'. This means,
   109 a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows:
   110 
   111   show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
   112 
   113 or:
   114 
   115   show "C x" if "A x" "B x" for x
   116 
   117 Rare INCOMPATIBILITY, the old behaviour may be recovered as follows:
   118 
   119   show "C x" when "A x" "B x" for x
   120 
   121 * New command 'supply' supports fact definitions during goal refinement
   122 ('apply' scripts).
   123 
   124 * New command 'consider' states rules for generalized elimination and
   125 case splitting. This is like a toplevel statement "theorem obtains" used
   126 within a proof body; or like a multi-branch 'obtain' without activation
   127 of the local context elements yet.
   128 
   129 * Proof method "cases" allows to specify the rule as first entry of
   130 chained facts.  This is particularly useful with 'consider':
   131 
   132   consider (a) A | (b) B | (c) C <proof>
   133   then have something
   134   proof cases
   135     case a
   136     then show ?thesis <proof>
   137   next
   138     case b
   139     then show ?thesis <proof>
   140   next
   141     case c
   142     then show ?thesis <proof>
   143   qed
   144 
   145 * Command 'case' allows fact name and attribute specification like this:
   146 
   147   case a: (c xs)
   148   case a [attributes]: (c xs)
   149 
   150 Facts that are introduced by invoking the case context are uniformly
   151 qualified by "a"; the same name is used for the cumulative fact. The old
   152 form "case (c xs) [attributes]" is no longer supported. Rare
   153 INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,
   154 and always put attributes in front.
   155 
   156 * The standard proof method of commands 'proof' and '..' is now called
   157 "standard" to make semantically clear what it is; the old name "default"
   158 is still available as legacy for some time. Documentation now explains
   159 '..' more accurately as "by standard" instead of "by rule".
   160 
   161 * Command 'subgoal' allows to impose some structure on backward
   162 refinements, to avoid proof scripts degenerating into long of 'apply'
   163 sequences. Further explanations and examples are given in the isar-ref
   164 manual.
   165 
   166 * Proof method "goal_cases" turns the current subgoals into cases within
   167 the context; the conclusion is bound to variable ?case in each case. For
   168 example:
   169 
   170 lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
   171   and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
   172 proof goal_cases
   173   case (1 x)
   174   then show ?case using \<open>A x\<close> \<open>B x\<close> sorry
   175 next
   176   case (2 y z)
   177   then show ?case using \<open>U y\<close> \<open>V z\<close> sorry
   178 qed
   179 
   180 lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
   181   and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
   182 proof goal_cases
   183   case prems: 1
   184   then show ?case using prems sorry
   185 next
   186   case prems: 2
   187   then show ?case using prems sorry
   188 qed
   189 
   190 * The undocumented feature of implicit cases goal1, goal2, goal3, etc.
   191 is marked as legacy, and will be removed eventually. The proof method
   192 "goals" achieves a similar effect within regular Isar; often it can be
   193 done more adequately by other means (e.g. 'consider').
   194 
   195 * Nesting of Isar goal structure has been clarified: the context after
   196 the initial backwards refinement is retained for the whole proof, within
   197 all its context sections (as indicated via 'next'). This is e.g.
   198 relevant for 'using', 'including', 'supply':
   199 
   200   have "A \<and> A" if a: A for A
   201     supply [simp] = a
   202   proof
   203     show A by simp
   204   next
   205     show A by simp
   206   qed
   207 
   208 * Method "sleep" succeeds after a real-time delay (in seconds). This is
   209 occasionally useful for demonstration and testing purposes.
   210 
   211 
   212 *** Pure ***
   213 
   214 * Command 'print_definitions' prints dependencies of definitional
   215 specifications. This functionality used to be part of 'print_theory'.
   216 
   217 * The vacuous fact "TERM x" may be established "by fact" or as `TERM x`
   218 as well, not just "by this" or "." as before.
   219 
   220 * Configuration option rule_insts_schematic has been discontinued
   221 (intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.
   222 
   223 * Abbreviations in type classes now carry proper sort constraint.
   224 Rare INCOMPATIBILITY in situations where the previous misbehaviour
   225 has been exploited.
   226 
   227 * Refinement of user-space type system in type classes: pseudo-local
   228 operations behave more similar to abbreviations.  Potential
   229 INCOMPATIBILITY in exotic situations.
   230 
   231 
   232 *** HOL ***
   233 
   234 * Combinator to represent case distinction on products is named "case_prod",
   235 uniformly, discontinuing any input aliasses.  Very popular theorem aliasses
   236 have been retained.
   237 Consolidated facts:
   238   PairE ~> prod.exhaust
   239   Pair_eq ~> prod.inject
   240   pair_collapse ~> prod.collapse
   241   Pair_fst_snd_eq ~> prod_eq_iff
   242   split_twice ~> prod.case_distrib
   243   split_weak_cong ~> prod.case_cong_weak
   244   split_split ~> prod.split
   245   split_split_asm ~> prod.split_asm
   246   splitI ~> case_prodI
   247   splitD ~> case_prodD
   248   splitI2 ~> case_prodI2
   249   splitI2' ~> case_prodI2'
   250   splitE ~> case_prodE
   251   splitE' ~> case_prodE'
   252   split_pair ~> case_prod_Pair
   253   split_eta ~> case_prod_eta
   254   split_comp ~> case_prod_comp
   255   mem_splitI ~> mem_case_prodI
   256   mem_splitI2 ~> mem_case_prodI2
   257   mem_splitE ~> mem_case_prodE
   258   The_split ~> The_case_prod
   259   cond_split_eta ~> cond_case_prod_eta
   260   Collect_split_in_rel_leE ~> Collect_case_prod_in_rel_leE
   261   Collect_split_in_rel_leI ~> Collect_case_prod_in_rel_leI
   262   in_rel_Collect_split_eq ~> in_rel_Collect_case_prod_eq
   263   Collect_split_Grp_eqD ~> Collect_case_prod_Grp_eqD
   264   Collect_split_Grp_inD ~> Collect_case_prod_Grp_in
   265   Domain_Collect_split ~> Domain_Collect_case_prod
   266   Image_Collect_split ~> Image_Collect_case_prod
   267   Range_Collect_split ~> Range_Collect_case_prod
   268   Eps_split ~> Eps_case_prod
   269   Eps_split_eq ~> Eps_case_prod_eq
   270   split_rsp ~> case_prod_rsp
   271   curry_split ~> curry_case_prod
   272   split_curry ~> case_prod_curry
   273 Changes in structure HOLogic:
   274   split_const ~> case_prod_const
   275   mk_split ~> mk_case_prod
   276   mk_psplits ~> mk_ptupleabs
   277   strip_psplits ~> strip_ptupleabs
   278 INCOMPATIBILITY.
   279 
   280 * Commands 'inductive' and 'inductive_set' work better when names for
   281 intro rules are omitted: the "cases" and "induct" rules no longer
   282 declare empty case_names, but no case_names at all. This allows to use
   283 numbered cases in proofs, without requiring method "goal_cases".
   284 
   285 * The 'typedef' command has been upgraded from a partially checked
   286 "axiomatization", to a full definitional specification that takes the
   287 global collection of overloaded constant / type definitions into
   288 account. Type definitions with open dependencies on overloaded
   289 definitions need to be specified as "typedef (overloaded)". This
   290 provides extra robustness in theory construction. Rare INCOMPATIBILITY.
   291 
   292 * Qualification of various formal entities in the libraries is done more
   293 uniformly via "context begin qualified definition ... end" instead of
   294 old-style "hide_const (open) ...". Consequently, both the defined
   295 constant and its defining fact become qualified, e.g. Option.is_none and
   296 Option.is_none_def. Occasional INCOMPATIBILITY in applications.
   297 
   298 * Some old and rarely used ASCII replacement syntax has been removed.
   299 INCOMPATIBILITY, standard syntax with symbols should be used instead.
   300 The subsequent commands help to reproduce the old forms, e.g. to
   301 simplify porting old theories:
   302 
   303   type_notation Map.map  (infixr "~=>" 0)
   304   notation Map.map_comp  (infixl "o'_m" 55)
   305 
   306   type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21)
   307 
   308   notation FuncSet.funcset  (infixr "->" 60)
   309   notation FuncSet.extensional_funcset  (infixr "->\<^sub>E" 60)
   310 
   311   notation Omega_Words_Fun.conc (infixr "conc" 65)
   312 
   313   notation Preorder.equiv ("op ~~")
   314     and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50)
   315 
   316 * The alternative notation "\<Colon>" for type and sort constraints has been
   317 removed: in LaTeX document output it looks the same as "::".
   318 INCOMPATIBILITY, use plain "::" instead.
   319 
   320 * Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has
   321 been removed. INCOMPATIBILITY.
   322 
   323 * Quickcheck setup for finite sets.
   324 
   325 * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
   326 
   327 * Sledgehammer:
   328   - The MaSh relevance filter has been sped up.
   329   - Proof reconstruction has been improved, to minimize the incidence of
   330     cases where Sledgehammer gives a proof that does not work.
   331   - Auto Sledgehammer now minimizes and preplays the results.
   332   - Handle Vampire 4.0 proof output without raising exception.
   333   - Eliminated "MASH" environment variable. Use the "MaSh" option in
   334     Isabelle/jEdit instead. INCOMPATIBILITY.
   335   - Eliminated obsolete "blocking" option and related subcommands.
   336 
   337 * Nitpick:
   338   - Fixed soundness bug in translation of "finite" predicate.
   339   - Fixed soundness bug in "destroy_constrs" optimization.
   340   - Removed "check_potential" and "check_genuine" options.
   341   - Eliminated obsolete "blocking" option.
   342 
   343 * New (co)datatype package:
   344   - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
   345     structure on the raw type to an abstract type defined using typedef.
   346   - Always generate "case_transfer" theorem.
   347 
   348 * Transfer:
   349   - new methods for interactive debugging of 'transfer' and
   350     'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',
   351     'transfer_prover_start' and 'transfer_prover_end'.
   352 
   353 * Division on integers is bootstrapped directly from division on
   354 naturals and uses generic numeral algorithm for computations.
   355 Slight INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes
   356 former simprocs binary_int_div and binary_int_mod
   357 
   358 * Tightened specification of class semiring_no_zero_divisors.  Slight
   359 INCOMPATIBILITY.
   360 
   361 * Class algebraic_semidom introduces common algebraic notions of
   362 integral (semi)domains, particularly units.  Although
   363 logically subsumed by fields, is is not a super class of these
   364 in order not to burden fields with notions that are trivial there.
   365 
   366 * Class normalization_semidom specifies canonical representants
   367 for equivalence classes of associated elements in an integral
   368 (semi)domain.  This formalizes associated elements as well.
   369 
   370 * Abstract specification of gcd/lcm operations in classes semiring_gcd,
   371 semiring_Gcd, semiring_Lcd.  Minor INCOMPATIBILITY: facts gcd_nat.commute
   372 and gcd_int.commute are subsumed by gcd.commute, as well as gcd_nat.assoc
   373 and gcd_int.assoc by gcd.assoc.
   374 
   375 * Former constants Fields.divide (_ / _) and Divides.div (_ div _)
   376 are logically unified to Rings.divide in syntactic type class
   377 Rings.divide, with infix syntax (_ div _).  Infix syntax (_ / _)
   378 for field division is added later as abbreviation in class Fields.inverse.
   379 INCOMPATIBILITY,  instantiations must refer to Rings.divide rather
   380 than the former separate constants, hence infix syntax (_ / _) is usually
   381 not available during instantiation.
   382 
   383 * Library/Multiset:
   384   - Renamed multiset inclusion operators:
   385       < ~> <#
   386       \<subset> ~> \<subset>#
   387       <= ~> <=#
   388       \<le> ~> \<le>#
   389       \<subseteq> ~> \<subseteq>#
   390     INCOMPATIBILITY.
   391   - "'a multiset" is no longer an instance of the "order",
   392     "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",
   393     "semilattice_inf", and "semilattice_sup" type classes. The theorems
   394     previously provided by these type classes (directly or indirectly)
   395     are now available through the "subset_mset" interpretation
   396     (e.g. add_mono ~> subset_mset.add_mono).
   397     INCOMPATIBILITY.
   398   - Renamed conversions:
   399       multiset_of ~> mset
   400       multiset_of_set ~> mset_set
   401       set_of ~> set_mset
   402     INCOMPATIBILITY
   403   - Renamed lemmas:
   404       mset_le_def ~> subseteq_mset_def
   405       mset_less_def ~> subset_mset_def
   406       less_eq_multiset.rep_eq ~> subseteq_mset_def
   407     INCOMPATIBILITY
   408   - Removed lemmas generated by lift_definition:
   409     less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer
   410     less_eq_multiset_def
   411     INCOMPATIBILITY
   412 
   413 * Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals and Cauchy's
   414 integral theorem, ported from HOL Light
   415 
   416 * Multivariate_Analysis: Added topological concepts such as connected components
   417 and the inside or outside of a set.
   418 
   419 * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'
   420 command. Minor INCOMPATIBILITY, use 'function' instead.
   421 
   422 * Recursive function definitions ('fun', 'function', 'partial_function')
   423 no longer expose the low-level "_def" facts of the internal
   424 construction. INCOMPATIBILITY, enable option "function_defs" in the
   425 context for rare situations where these facts are really needed.
   426 
   427 * Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
   428 
   429 * Library/Omega_Words_Fun: Infinite words modeled as functions nat => 'a.
   430 
   431 
   432 *** ML ***
   433 
   434 * The auxiliary module Pure/display.ML has been eliminated. Its
   435 elementary thm print operations are now in Pure/more_thm.ML and thus
   436 called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.
   437 
   438 * Simproc programming interfaces have been simplified:
   439 Simplifier.make_simproc and Simplifier.define_simproc supersede various
   440 forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that
   441 term patterns for the left-hand sides are specified with implicitly
   442 fixed variables, like top-level theorem statements. INCOMPATIBILITY.
   443 
   444 * Instantiation rules have been re-organized as follows:
   445 
   446   Thm.instantiate  (*low-level instantiation with named arguments*)
   447   Thm.instantiate' (*version with positional arguments*)
   448 
   449   Drule.infer_instantiate  (*instantiation with type inference*)
   450   Drule.infer_instantiate'  (*version with positional arguments*)
   451 
   452 The LHS only requires variable specifications, instead of full terms.
   453 Old cterm_instantiate is superseded by infer_instantiate.
   454 INCOMPATIBILITY, need to re-adjust some ML names and types accordingly.
   455 
   456 * Old tactic shorthands atac, rtac, etac, dtac, ftac have been
   457 discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
   458 instead (with proper context).
   459 
   460 * Thm.instantiate (and derivatives) no longer require the LHS of the
   461 instantiation to be certified: plain variables are given directly.
   462 
   463 * Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous
   464 quasi-bound variables (like the Simplifier), instead of accidentally
   465 named local fixes. This has the potential to improve stability of proof
   466 tools, but can also cause INCOMPATIBILITY for tools that don't observe
   467 the proof context discipline.
   468 
   469 
   470 *** System ***
   471 
   472 * Property values in etc/symbols may contain spaces, if written with the
   473 replacement character "␣" (Unicode point 0x2324).  For example:
   474 
   475   \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono
   476 
   477 * Command-line tool "isabelle jedit_client" allows to connect to already
   478 running Isabelle/jEdit process. This achieves the effect of
   479 single-instance applications seen on common GUI desktops.
   480 
   481 * Command-line tool "isabelle update_then" expands old Isar command
   482 conflations:
   483 
   484     hence  ~>  then have
   485     thus   ~>  then show
   486 
   487 This syntax is more orthogonal and improves readability and
   488 maintainability of proofs.
   489 
   490 * Poly/ML default platform architecture may be changed from 32bit to
   491 64bit via system option ML_system_64. A system restart (and rebuild)
   492 is required after change.
   493 
   494 * Poly/ML 5.5.3 runs natively on x86-windows and x86_64-windows,
   495 which both allow larger heap space than former x86-cygwin.
   496 
   497 * Java runtime environment for x86_64-windows allows to use larger heap
   498 space.
   499 
   500 * Java runtime options are determined separately for 32bit vs. 64bit
   501 platforms as follows.
   502 
   503   - Isabelle desktop application: platform-specific files that are
   504     associated with the main app bundle
   505 
   506   - isabelle jedit: settings
   507     JEDIT_JAVA_SYSTEM_OPTIONS
   508     JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64
   509 
   510   - isabelle build: settings
   511     ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64
   512 
   513 * Bash shell function "jvmpath" has been renamed to "platform_path": it
   514 is relevant both for Poly/ML and JVM processes.
   515 
   516 
   517 
   518 New in Isabelle2015 (May 2015)
   519 ------------------------------
   520 
   521 *** General ***
   522 
   523 * Local theory specification commands may have a 'private' or
   524 'qualified' modifier to restrict name space accesses to the local scope,
   525 as provided by some "context begin ... end" block. For example:
   526 
   527   context
   528   begin
   529 
   530   private definition ...
   531   private lemma ...
   532 
   533   qualified definition ...
   534   qualified lemma ...
   535 
   536   lemma ...
   537   theorem ...
   538 
   539   end
   540 
   541 * Command 'experiment' opens an anonymous locale context with private
   542 naming policy.
   543 
   544 * Command 'notepad' requires proper nesting of begin/end and its proof
   545 structure in the body: 'oops' is no longer supported here. Minor
   546 INCOMPATIBILITY, use 'sorry' instead.
   547 
   548 * Command 'named_theorems' declares a dynamic fact within the context,
   549 together with an attribute to maintain the content incrementally. This
   550 supersedes functor Named_Thms in Isabelle/ML, but with a subtle change
   551 of semantics due to external visual order vs. internal reverse order.
   552 
   553 * 'find_theorems': search patterns which are abstractions are
   554 schematically expanded before search. Search results match the naive
   555 expectation more closely, particularly wrt. abbreviations.
   556 INCOMPATIBILITY.
   557 
   558 * Commands 'method_setup' and 'attribute_setup' now work within a local
   559 theory context.
   560 
   561 * Outer syntax commands are managed authentically within the theory
   562 context, without implicit global state. Potential for accidental
   563 INCOMPATIBILITY, make sure that required theories are really imported.
   564 
   565 * Historical command-line terminator ";" is no longer accepted (and
   566 already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle
   567 update_semicolons" to remove obsolete semicolons from old theory
   568 sources.
   569 
   570 * Structural composition of proof methods (meth1; meth2) in Isar
   571 corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
   572 
   573 * The Eisbach proof method language allows to define new proof methods
   574 by combining existing ones with their usual syntax. The "match" proof
   575 method provides basic fact/term matching in addition to
   576 premise/conclusion matching through Subgoal.focus, and binds fact names
   577 from matches as well as term patterns within matches. The Isabelle
   578 documentation provides an entry "eisbach" for the Eisbach User Manual.
   579 Sources and various examples are in ~~/src/HOL/Eisbach/.
   580 
   581 
   582 *** Prover IDE -- Isabelle/Scala/jEdit ***
   583 
   584 * Improved folding mode "isabelle" based on Isar syntax. Alternatively,
   585 the "sidekick" mode may be used for document structure.
   586 
   587 * Extended bracket matching based on Isar language structure. System
   588 option jedit_structure_limit determines maximum number of lines to scan
   589 in the buffer.
   590 
   591 * Support for BibTeX files: context menu, context-sensitive token
   592 marker, SideKick parser.
   593 
   594 * Document antiquotation @{cite} provides formal markup, which is
   595 interpreted semi-formally based on .bib files that happen to be open in
   596 the editor (hyperlinks, completion etc.).
   597 
   598 * Less waste of vertical space via negative line spacing (see Global
   599 Options / Text Area).
   600 
   601 * Improved graphview panel with optional output of PNG or PDF, for
   602 display of 'thy_deps', 'class_deps' etc.
   603 
   604 * The commands 'thy_deps' and 'class_deps' allow optional bounds to
   605 restrict the visualized hierarchy.
   606 
   607 * Improved scheduling for asynchronous print commands (e.g. provers
   608 managed by the Sledgehammer panel) wrt. ongoing document processing.
   609 
   610 
   611 *** Document preparation ***
   612 
   613 * Document markup commands 'chapter', 'section', 'subsection',
   614 'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any
   615 context, even before the initial 'theory' command. Obsolete proof
   616 commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been
   617 discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw'
   618 instead. The old 'header' command is still retained for some time, but
   619 should be replaced by 'chapter', 'section' etc. (using "isabelle
   620 update_header"). Minor INCOMPATIBILITY.
   621 
   622 * Official support for "tt" style variants, via \isatt{...} or
   623 \begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
   624 verbatim environment of LaTeX is no longer used. This allows @{ML} etc.
   625 as argument to other macros (such as footnotes).
   626 
   627 * Document antiquotation @{verbatim} prints ASCII text literally in "tt"
   628 style.
   629 
   630 * Discontinued obsolete option "document_graph": session_graph.pdf is
   631 produced unconditionally for HTML browser_info and PDF-LaTeX document.
   632 
   633 * Diagnostic commands and document markup commands within a proof do not
   634 affect the command tag for output. Thus commands like 'thm' are subject
   635 to proof document structure, and no longer "stick out" accidentally.
   636 Commands 'text' and 'txt' merely differ in the LaTeX style, not their
   637 tags. Potential INCOMPATIBILITY in exotic situations.
   638 
   639 * System option "pretty_margin" is superseded by "thy_output_margin",
   640 which is also accessible via document antiquotation option "margin".
   641 Only the margin for document output may be changed, but not the global
   642 pretty printing: that is 76 for plain console output, and adapted
   643 dynamically in GUI front-ends. Implementations of document
   644 antiquotations need to observe the margin explicitly according to
   645 Thy_Output.string_of_margin. Minor INCOMPATIBILITY.
   646 
   647 * Specification of 'document_files' in the session ROOT file is
   648 mandatory for document preparation. The legacy mode with implicit
   649 copying of the document/ directory is no longer supported. Minor
   650 INCOMPATIBILITY.
   651 
   652 
   653 *** Pure ***
   654 
   655 * Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
   656 etc.) allow an optional context of local variables ('for' declaration):
   657 these variables become schematic in the instantiated theorem; this
   658 behaviour is analogous to 'for' in attributes "where" and "of".
   659 Configuration option rule_insts_schematic (default false) controls use
   660 of schematic variables outside the context. Minor INCOMPATIBILITY,
   661 declare rule_insts_schematic = true temporarily and update to use local
   662 variable declarations or dummy patterns instead.
   663 
   664 * Explicit instantiation via attributes "where", "of", and proof methods
   665 "rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
   666 ("_") that stand for anonymous local variables.
   667 
   668 * Generated schematic variables in standard format of exported facts are
   669 incremented to avoid material in the proof context. Rare
   670 INCOMPATIBILITY, explicit instantiation sometimes needs to refer to
   671 different index.
   672 
   673 * Lexical separation of signed and unsigned numerals: categories "num"
   674 and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence
   675 of numeral signs, particularly in expressions involving infix syntax
   676 like "(- 1) ^ n".
   677 
   678 * Old inner token category "xnum" has been discontinued.  Potential
   679 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num"
   680 token category instead.
   681 
   682 
   683 *** HOL ***
   684 
   685 * New (co)datatype package:
   686   - The 'datatype_new' command has been renamed 'datatype'. The old
   687     command of that name is now called 'old_datatype' and is provided
   688     by "~~/src/HOL/Library/Old_Datatype.thy". See
   689     'isabelle doc datatypes' for information on porting.
   690     INCOMPATIBILITY.
   691   - Renamed theorems:
   692       disc_corec ~> corec_disc
   693       disc_corec_iff ~> corec_disc_iff
   694       disc_exclude ~> distinct_disc
   695       disc_exhaust ~> exhaust_disc
   696       disc_map_iff ~> map_disc_iff
   697       sel_corec ~> corec_sel
   698       sel_exhaust ~> exhaust_sel
   699       sel_map ~> map_sel
   700       sel_set ~> set_sel
   701       sel_split ~> split_sel
   702       sel_split_asm ~> split_sel_asm
   703       strong_coinduct ~> coinduct_strong
   704       weak_case_cong ~> case_cong_weak
   705     INCOMPATIBILITY.
   706   - The "no_code" option to "free_constructors", "datatype_new", and
   707     "codatatype" has been renamed "plugins del: code".
   708     INCOMPATIBILITY.
   709   - The rules "set_empty" have been removed. They are easy
   710     consequences of other set rules "by auto".
   711     INCOMPATIBILITY.
   712   - The rule "set_cases" is now registered with the "[cases set]"
   713     attribute. This can influence the behavior of the "cases" proof
   714     method when more than one case rule is applicable (e.g., an
   715     assumption is of the form "w : set ws" and the method "cases w"
   716     is invoked). The solution is to specify the case rule explicitly
   717     (e.g. "cases w rule: widget.exhaust").
   718     INCOMPATIBILITY.
   719   - Renamed theories:
   720       BNF_Comp ~> BNF_Composition
   721       BNF_FP_Base ~> BNF_Fixpoint_Base
   722       BNF_GFP ~> BNF_Greatest_Fixpoint
   723       BNF_LFP ~> BNF_Least_Fixpoint
   724       BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions
   725       Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions
   726     INCOMPATIBILITY.
   727   - Lifting and Transfer setup for basic HOL types sum and prod (also
   728     option) is now performed by the BNF package. Theories Lifting_Sum,
   729     Lifting_Product and Lifting_Option from Main became obsolete and
   730     were removed. Changed definitions of the relators rel_prod and
   731     rel_sum (using inductive).
   732     INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead
   733     of rel_prod_def and rel_sum_def.
   734     Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names
   735     changed (e.g. map_prod_transfer ~> prod.map_transfer).
   736   - Parametricity theorems for map functions, relators, set functions,
   737     constructors, case combinators, discriminators, selectors and
   738     (co)recursors are automatically proved and registered as transfer
   739     rules.
   740 
   741 * Old datatype package:
   742   - The old 'datatype' command has been renamed 'old_datatype', and
   743     'rep_datatype' has been renamed 'old_rep_datatype'. They are
   744     provided by "~~/src/HOL/Library/Old_Datatype.thy". See
   745     'isabelle doc datatypes' for information on porting.
   746     INCOMPATIBILITY.
   747   - Renamed theorems:
   748       weak_case_cong ~> case_cong_weak
   749     INCOMPATIBILITY.
   750   - Renamed theory:
   751       ~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy
   752     INCOMPATIBILITY.
   753 
   754 * Nitpick:
   755   - Fixed soundness bug related to the strict and non-strict subset
   756     operations.
   757 
   758 * Sledgehammer:
   759   - CVC4 is now included with Isabelle instead of CVC3 and run by
   760     default.
   761   - Z3 is now always enabled by default, now that it is fully open
   762     source. The "z3_non_commercial" option is discontinued.
   763   - Minimization is now always enabled by default.
   764     Removed sub-command:
   765       min
   766   - Proof reconstruction, both one-liners and Isar, has been
   767     dramatically improved.
   768   - Improved support for CVC4 and veriT.
   769 
   770 * Old and new SMT modules:
   771   - The old 'smt' method has been renamed 'old_smt' and moved to
   772     'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility,
   773     until applications have been ported to use the new 'smt' method. For
   774     the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must
   775     be installed, and the environment variable "OLD_Z3_SOLVER" must
   776     point to it.
   777     INCOMPATIBILITY.
   778   - The 'smt2' method has been renamed 'smt'.
   779     INCOMPATIBILITY.
   780   - New option 'smt_reconstruction_step_timeout' to limit the
   781     reconstruction time of Z3 proof steps in the new 'smt' method.
   782   - New option 'smt_statistics' to display statistics of the new 'smt'
   783     method, especially runtime statistics of Z3 proof reconstruction.
   784 
   785 * Lifting: command 'lift_definition' allows to execute lifted constants
   786 that have as a return type a datatype containing a subtype. This
   787 overcomes long-time limitations in the area of code generation and
   788 lifting, and avoids tedious workarounds.
   789 
   790 * Command and antiquotation "value" provide different evaluation slots
   791 (again), where the previous strategy (NBE after ML) serves as default.
   792 Minor INCOMPATIBILITY.
   793 
   794 * Add NO_MATCH-simproc, allows to check for syntactic non-equality.
   795 
   796 * field_simps: Use NO_MATCH-simproc for distribution rules, to avoid
   797 non-termination in case of distributing a division. With this change
   798 field_simps is in some cases slightly less powerful, if it fails try to
   799 add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY.
   800 
   801 * Separate class no_zero_divisors has been given up in favour of fully
   802 algebraic semiring_no_zero_divisors. INCOMPATIBILITY.
   803 
   804 * Class linordered_semidom really requires no zero divisors.
   805 INCOMPATIBILITY.
   806 
   807 * Classes division_ring, field and linordered_field always demand
   808 "inverse 0 = 0". Given up separate classes division_ring_inverse_zero,
   809 field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY.
   810 
   811 * Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit
   812 additive inverse operation. INCOMPATIBILITY.
   813 
   814 * Complex powers and square roots. The functions "ln" and "powr" are now
   815 overloaded for types real and complex, and 0 powr y = 0 by definition.
   816 INCOMPATIBILITY: type constraints may be necessary.
   817 
   818 * The functions "sin" and "cos" are now defined for any type of sort
   819 "{real_normed_algebra_1,banach}" type, so in particular on "real" and
   820 "complex" uniformly. Minor INCOMPATIBILITY: type constraints may be
   821 needed.
   822 
   823 * New library of properties of the complex transcendental functions sin,
   824 cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light.
   825 
   826 * The factorial function, "fact", now has type "nat => 'a" (of a sort
   827 that admits numeric types including nat, int, real and complex.
   828 INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type
   829 constraint, and the combination "real (fact k)" is likely to be
   830 unsatisfactory. If a type conversion is still necessary, then use
   831 "of_nat (fact k)" or "real_of_nat (fact k)".
   832 
   833 * Removed functions "natfloor" and "natceiling", use "nat o floor" and
   834 "nat o ceiling" instead. A few of the lemmas have been retained and
   835 adapted: in their names "natfloor"/"natceiling" has been replaced by
   836 "nat_floor"/"nat_ceiling".
   837 
   838 * Qualified some duplicated fact names required for boostrapping the
   839 type class hierarchy:
   840   ab_add_uminus_conv_diff ~> diff_conv_add_uminus
   841   field_inverse_zero ~> inverse_zero
   842   field_divide_inverse ~> divide_inverse
   843   field_inverse ~> left_inverse
   844 Minor INCOMPATIBILITY.
   845 
   846 * Eliminated fact duplicates:
   847   mult_less_imp_less_right ~> mult_right_less_imp_less
   848   mult_less_imp_less_left ~> mult_left_less_imp_less
   849 Minor INCOMPATIBILITY.
   850 
   851 * Fact consolidation: even_less_0_iff is subsumed by
   852 double_add_less_zero_iff_single_add_less_zero (simp by default anyway).
   853 
   854 * Generalized and consolidated some theorems concerning divsibility:
   855   dvd_reduce ~> dvd_add_triv_right_iff
   856   dvd_plus_eq_right ~> dvd_add_right_iff
   857   dvd_plus_eq_left ~> dvd_add_left_iff
   858 Minor INCOMPATIBILITY.
   859 
   860 * "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _"
   861 and part of theory Main.
   862   even_def ~> even_iff_mod_2_eq_zero
   863 INCOMPATIBILITY.
   864 
   865 * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor
   866 INCOMPATIBILITY.
   867 
   868 * Bootstrap of listsum as special case of abstract product over lists.
   869 Fact rename:
   870     listsum_def ~> listsum.eq_foldr
   871 INCOMPATIBILITY.
   872 
   873 * Product over lists via constant "listprod".
   874 
   875 * Theory List: renamed drop_Suc_conv_tl and nth_drop' to
   876 Cons_nth_drop_Suc.
   877 
   878 * New infrastructure for compiling, running, evaluating and testing
   879 generated code in target languages in HOL/Library/Code_Test. See
   880 HOL/Codegenerator_Test/Code_Test* for examples.
   881 
   882 * Library/Multiset:
   883   - Introduced "replicate_mset" operation.
   884   - Introduced alternative characterizations of the multiset ordering in
   885     "Library/Multiset_Order".
   886   - Renamed multiset ordering:
   887       <# ~> #<#
   888       <=# ~> #<=#
   889       \<subset># ~> #\<subset>#
   890       \<subseteq># ~> #\<subseteq>#
   891     INCOMPATIBILITY.
   892   - Introduced abbreviations for ill-named multiset operations:
   893       <#, \<subset># abbreviate < (strict subset)
   894       <=#, \<le>#, \<subseteq># abbreviate <= (subset or equal)
   895     INCOMPATIBILITY.
   896   - Renamed
   897       in_multiset_of ~> in_multiset_in_set
   898       Multiset.fold ~> fold_mset
   899       Multiset.filter ~> filter_mset
   900     INCOMPATIBILITY.
   901   - Removed mcard, is equal to size.
   902   - Added attributes:
   903       image_mset.id [simp]
   904       image_mset_id [simp]
   905       elem_multiset_of_set [simp, intro]
   906       comp_fun_commute_plus_mset [simp]
   907       comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp]
   908       in_mset_fold_plus_iff [iff]
   909       set_of_Union_mset [simp]
   910       in_Union_mset_iff [iff]
   911     INCOMPATIBILITY.
   912 
   913 * Library/Sum_of_Squares: simplified and improved "sos" method. Always
   914 use local CSDP executable, which is much faster than the NEOS server.
   915 The "sos_cert" functionality is invoked as "sos" with additional
   916 argument. Minor INCOMPATIBILITY.
   917 
   918 * HOL-Decision_Procs: New counterexample generator quickcheck
   919 [approximation] for inequalities of transcendental functions. Uses
   920 hardware floating point arithmetic to randomly discover potential
   921 counterexamples. Counterexamples are certified with the "approximation"
   922 method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
   923 examples.
   924 
   925 * HOL-Probability: Reworked measurability prover
   926   - applies destructor rules repeatedly
   927   - removed application splitting (replaced by destructor rule)
   928   - added congruence rules to rewrite measure spaces under the sets
   929     projection
   930 
   931 * New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for
   932 single-step rewriting with subterm selection based on patterns.
   933 
   934 
   935 *** ML ***
   936 
   937 * Subtle change of name space policy: undeclared entries are now
   938 considered inaccessible, instead of accessible via the fully-qualified
   939 internal name. This mainly affects Name_Space.intern (and derivatives),
   940 which may produce an unexpected Long_Name.hidden prefix. Note that
   941 contemporary applications use the strict Name_Space.check (and
   942 derivatives) instead, which is not affected by the change. Potential
   943 INCOMPATIBILITY in rare applications of Name_Space.intern.
   944 
   945 * Subtle change of error semantics of Toplevel.proof_of: regular user
   946 ERROR instead of internal Toplevel.UNDEF.
   947 
   948 * Basic combinators map, fold, fold_map, split_list, apply are available
   949 as parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
   950 
   951 * Renamed "pairself" to "apply2", in accordance to @{apply 2}.
   952 INCOMPATIBILITY.
   953 
   954 * Former combinators NAMED_CRITICAL and CRITICAL for central critical
   955 sections have been discontinued, in favour of the more elementary
   956 Multithreading.synchronized and its high-level derivative
   957 Synchronized.var (which is usually sufficient in applications). Subtle
   958 INCOMPATIBILITY: synchronized access needs to be atomic and cannot be
   959 nested.
   960 
   961 * Synchronized.value (ML) is actually synchronized (as in Scala): subtle
   962 change of semantics with minimal potential for INCOMPATIBILITY.
   963 
   964 * The main operations to certify logical entities are Thm.ctyp_of and
   965 Thm.cterm_of with a local context; old-style global theory variants are
   966 available as Thm.global_ctyp_of and Thm.global_cterm_of.
   967 INCOMPATIBILITY.
   968 
   969 * Elementary operations in module Thm are no longer pervasive.
   970 INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of,
   971 Thm.term_of etc.
   972 
   973 * Proper context for various elementary tactics: assume_tac,
   974 resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac,
   975 compose_tac, Splitter.split_tac etc. INCOMPATIBILITY.
   976 
   977 * Tactical PARALLEL_ALLGOALS is the most common way to refer to
   978 PARALLEL_GOALS.
   979 
   980 * Goal.prove_multi is superseded by the fully general Goal.prove_common,
   981 which also allows to specify a fork priority.
   982 
   983 * Antiquotation @{command_spec "COMMAND"} is superseded by
   984 @{command_keyword COMMAND} (usually without quotes and with PIDE
   985 markup). Minor INCOMPATIBILITY.
   986 
   987 * Cartouches within ML sources are turned into values of type
   988 Input.source (with formal position information).
   989 
   990 
   991 *** System ***
   992 
   993 * The Isabelle tool "update_cartouches" changes theory files to use
   994 cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
   995 
   996 * The Isabelle tool "build" provides new options -X, -k, -x.
   997 
   998 * Discontinued old-fashioned "codegen" tool. Code generation can always
   999 be externally triggered using an appropriate ROOT file plus a
  1000 corresponding theory. Parametrization is possible using environment
  1001 variables, or ML snippets in the most extreme cases. Minor
  1002 INCOMPATIBILITY.
  1003 
  1004 * JVM system property "isabelle.threads" determines size of Scala thread
  1005 pool, like Isabelle system option "threads" for ML.
  1006 
  1007 * JVM system property "isabelle.laf" determines the default Swing
  1008 look-and-feel, via internal class name or symbolic name as in the jEdit
  1009 menu Global Options / Appearance.
  1010 
  1011 * Support for Proof General and Isar TTY loop has been discontinued.
  1012 Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.
  1013 
  1014 
  1015 
  1016 New in Isabelle2014 (August 2014)
  1017 ---------------------------------
  1018 
  1019 *** General ***
  1020 
  1021 * Support for official Standard ML within the Isabelle context.
  1022 Command 'SML_file' reads and evaluates the given Standard ML file.
  1023 Toplevel bindings are stored within the theory context; the initial
  1024 environment is restricted to the Standard ML implementation of
  1025 Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'
  1026 and 'SML_export' allow to exchange toplevel bindings between the two
  1027 separate environments.  See also ~~/src/Tools/SML/Examples.thy for
  1028 some examples.
  1029 
  1030 * Standard tactics and proof methods such as "clarsimp", "auto" and
  1031 "safe" now preserve equality hypotheses "x = expr" where x is a free
  1032 variable.  Locale assumptions and chained facts containing "x"
  1033 continue to be useful.  The new method "hypsubst_thin" and the
  1034 configuration option "hypsubst_thin" (within the attribute name space)
  1035 restore the previous behavior.  INCOMPATIBILITY, especially where
  1036 induction is done after these methods or when the names of free and
  1037 bound variables clash.  As first approximation, old proofs may be
  1038 repaired by "using [[hypsubst_thin = true]]" in the critical spot.
  1039 
  1040 * More static checking of proof methods, which allows the system to
  1041 form a closure over the concrete syntax.  Method arguments should be
  1042 processed in the original proof context as far as possible, before
  1043 operating on the goal state.  In any case, the standard discipline for
  1044 subgoal-addressing needs to be observed: no subgoals or a subgoal
  1045 number that is out of range produces an empty result sequence, not an
  1046 exception.  Potential INCOMPATIBILITY for non-conformant tactical
  1047 proof tools.
  1048 
  1049 * Lexical syntax (inner and outer) supports text cartouches with
  1050 arbitrary nesting, and without escapes of quotes etc.  The Prover IDE
  1051 supports input via ` (backquote).
  1052 
  1053 * The outer syntax categories "text" (for formal comments and document
  1054 markup commands) and "altstring" (for literal fact references) allow
  1055 cartouches as well, in addition to the traditional mix of quotations.
  1056 
  1057 * Syntax of document antiquotation @{rail} now uses \<newline> instead
  1058 of "\\", to avoid the optical illusion of escaped backslash within
  1059 string token.  General renovation of its syntax using text cartouches.
  1060 Minor INCOMPATIBILITY.
  1061 
  1062 * Discontinued legacy_isub_isup, which was a temporary workaround for
  1063 Isabelle/ML in Isabelle2013-1.  The prover process no longer accepts
  1064 old identifier syntax with \<^isub> or \<^isup>.  Potential
  1065 INCOMPATIBILITY.
  1066 
  1067 * Document antiquotation @{url} produces markup for the given URL,
  1068 which results in an active hyperlink within the text.
  1069 
  1070 * Document antiquotation @{file_unchecked} is like @{file}, but does
  1071 not check existence within the file-system.
  1072 
  1073 * Updated and extended manuals: codegen, datatypes, implementation,
  1074 isar-ref, jedit, system.
  1075 
  1076 
  1077 *** Prover IDE -- Isabelle/Scala/jEdit ***
  1078 
  1079 * Improved Document panel: simplified interaction where every single
  1080 mouse click (re)opens document via desktop environment or as jEdit
  1081 buffer.
  1082 
  1083 * Support for Navigator plugin (with toolbar buttons), with connection
  1084 to PIDE hyperlinks.
  1085 
  1086 * Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
  1087 Open text buffers take precedence over copies within the file-system.
  1088 
  1089 * Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
  1090 auxiliary ML files.
  1091 
  1092 * Improved syntactic and semantic completion mechanism, with simple
  1093 templates, completion language context, name-space completion,
  1094 file-name completion, spell-checker completion.
  1095 
  1096 * Refined GUI popup for completion: more robust key/mouse event
  1097 handling and propagation to enclosing text area -- avoid loosing
  1098 keystrokes with slow / remote graphics displays.
  1099 
  1100 * Completion popup supports both ENTER and TAB (default) to select an
  1101 item, depending on Isabelle options.
  1102 
  1103 * Refined insertion of completion items wrt. jEdit text: multiple
  1104 selections, rectangular selections, rectangular selection as "tall
  1105 caret".
  1106 
  1107 * Integrated spell-checker for document text, comments etc. with
  1108 completion popup and context-menu.
  1109 
  1110 * More general "Query" panel supersedes "Find" panel, with GUI access
  1111 to commands 'find_theorems' and 'find_consts', as well as print
  1112 operations for the context.  Minor incompatibility in keyboard
  1113 shortcuts etc.: replace action isabelle-find by isabelle-query.
  1114 
  1115 * Search field for all output panels ("Output", "Query", "Info" etc.)
  1116 to highlight text via regular expression.
  1117 
  1118 * Option "jedit_print_mode" (see also "Plugin Options / Isabelle /
  1119 General") allows to specify additional print modes for the prover
  1120 process, without requiring old-fashioned command-line invocation of
  1121 "isabelle jedit -m MODE".
  1122 
  1123 * More support for remote files (e.g. http) using standard Java
  1124 networking operations instead of jEdit virtual file-systems.
  1125 
  1126 * Empty editors buffers that are no longer required (e.g.\ via theory
  1127 imports) are automatically removed from the document model.
  1128 
  1129 * Improved monitor panel.
  1130 
  1131 * Improved Console/Scala plugin: more uniform scala.Console output,
  1132 more robust treatment of threads and interrupts.
  1133 
  1134 * Improved management of dockable windows: clarified keyboard focus
  1135 and window placement wrt. main editor view; optional menu item to
  1136 "Detach" a copy where this makes sense.
  1137 
  1138 * New Simplifier Trace panel provides an interactive view of the
  1139 simplification process, enabled by the "simp_trace_new" attribute
  1140 within the context.
  1141 
  1142 
  1143 *** Pure ***
  1144 
  1145 * Low-level type-class commands 'classes', 'classrel', 'arities' have
  1146 been discontinued to avoid the danger of non-trivial axiomatization
  1147 that is not immediately visible.  INCOMPATIBILITY, use regular
  1148 'instance' command with proof.  The required OFCLASS(...) theorem
  1149 might be postulated via 'axiomatization' beforehand, or the proof
  1150 finished trivially if the underlying class definition is made vacuous
  1151 (without any assumptions).  See also Isabelle/ML operations
  1152 Axclass.class_axiomatization, Axclass.classrel_axiomatization,
  1153 Axclass.arity_axiomatization.
  1154 
  1155 * Basic constants of Pure use more conventional names and are always
  1156 qualified.  Rare INCOMPATIBILITY, but with potentially serious
  1157 consequences, notably for tools in Isabelle/ML.  The following
  1158 renaming needs to be applied:
  1159 
  1160   ==             ~>  Pure.eq
  1161   ==>            ~>  Pure.imp
  1162   all            ~>  Pure.all
  1163   TYPE           ~>  Pure.type
  1164   dummy_pattern  ~>  Pure.dummy_pattern
  1165 
  1166 Systematic porting works by using the following theory setup on a
  1167 *previous* Isabelle version to introduce the new name accesses for the
  1168 old constants:
  1169 
  1170 setup {*
  1171   fn thy => thy
  1172     |> Sign.root_path
  1173     |> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="
  1174     |> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"
  1175     |> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"
  1176     |> Sign.restore_naming thy
  1177 *}
  1178 
  1179 Thus ML antiquotations like @{const_name Pure.eq} may be used already.
  1180 Later the application is moved to the current Isabelle version, and
  1181 the auxiliary aliases are deleted.
  1182 
  1183 * Attributes "where" and "of" allow an optional context of local
  1184 variables ('for' declaration): these variables become schematic in the
  1185 instantiated theorem.
  1186 
  1187 * Obsolete attribute "standard" has been discontinued (legacy since
  1188 Isabelle2012).  Potential INCOMPATIBILITY, use explicit 'for' context
  1189 where instantiations with schematic variables are intended (for
  1190 declaration commands like 'lemmas' or attributes like "of").  The
  1191 following temporary definition may help to port old applications:
  1192 
  1193   attribute_setup standard =
  1194     "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
  1195 
  1196 * More thorough check of proof context for goal statements and
  1197 attributed fact expressions (concerning background theory, declared
  1198 hyps).  Potential INCOMPATIBILITY, tools need to observe standard
  1199 context discipline.  See also Assumption.add_assumes and the more
  1200 primitive Thm.assume_hyps.
  1201 
  1202 * Inner syntax token language allows regular quoted strings "..."
  1203 (only makes sense in practice, if outer syntax is delimited
  1204 differently, e.g. via cartouches).
  1205 
  1206 * Command 'print_term_bindings' supersedes 'print_binds' for clarity,
  1207 but the latter is retained some time as Proof General legacy.
  1208 
  1209 * Code generator preprocessor: explicit control of simp tracing on a
  1210 per-constant basis.  See attribute "code_preproc".
  1211 
  1212 
  1213 *** HOL ***
  1214 
  1215 * Code generator: enforce case of identifiers only for strict target
  1216 language requirements.  INCOMPATIBILITY.
  1217 
  1218 * Code generator: explicit proof contexts in many ML interfaces.
  1219 INCOMPATIBILITY.
  1220 
  1221 * Code generator: minimize exported identifiers by default.  Minor
  1222 INCOMPATIBILITY.
  1223 
  1224 * Code generation for SML and OCaml: dropped arcane "no_signatures"
  1225 option.  Minor INCOMPATIBILITY.
  1226 
  1227 * "declare [[code abort: ...]]" replaces "code_abort ...".
  1228 INCOMPATIBILITY.
  1229 
  1230 * "declare [[code drop: ...]]" drops all code equations associated
  1231 with the given constants.
  1232 
  1233 * Code generations are provided for make, fields, extend and truncate
  1234 operations on records.
  1235 
  1236 * Command and antiquotation "value" are now hardcoded against nbe and
  1237 ML.  Minor INCOMPATIBILITY.
  1238 
  1239 * Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY.
  1240 
  1241 * The symbol "\<newline>" may be used within char or string literals
  1242 to represent (Char Nibble0 NibbleA), i.e. ASCII newline.
  1243 
  1244 * Qualified String.implode and String.explode.  INCOMPATIBILITY.
  1245 
  1246 * Simplifier: Enhanced solver of preconditions of rewrite rules can
  1247 now deal with conjunctions.  For help with converting proofs, the old
  1248 behaviour of the simplifier can be restored like this: declare/using
  1249 [[simp_legacy_precond]].  This configuration option will disappear
  1250 again in the future.  INCOMPATIBILITY.
  1251 
  1252 * Simproc "finite_Collect" is no longer enabled by default, due to
  1253 spurious crashes and other surprises.  Potential INCOMPATIBILITY.
  1254 
  1255 * Moved new (co)datatype package and its dependencies from session
  1256   "HOL-BNF" to "HOL".  The commands 'bnf', 'wrap_free_constructors',
  1257   'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now
  1258   part of theory "Main".
  1259 
  1260   Theory renamings:
  1261     FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
  1262     Library/Wfrec.thy ~> Wfrec.thy
  1263     Library/Zorn.thy ~> Zorn.thy
  1264     Cardinals/Order_Relation.thy ~> Order_Relation.thy
  1265     Library/Order_Union.thy ~> Cardinals/Order_Union.thy
  1266     Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy
  1267     Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy
  1268     Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy
  1269     Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy
  1270     Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy
  1271     BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy
  1272     BNF/Basic_BNFs.thy ~> Basic_BNFs.thy
  1273     BNF/BNF_Comp.thy ~> BNF_Comp.thy
  1274     BNF/BNF_Def.thy ~> BNF_Def.thy
  1275     BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy
  1276     BNF/BNF_GFP.thy ~> BNF_GFP.thy
  1277     BNF/BNF_LFP.thy ~> BNF_LFP.thy
  1278     BNF/BNF_Util.thy ~> BNF_Util.thy
  1279     BNF/Coinduction.thy ~> Coinduction.thy
  1280     BNF/More_BNFs.thy ~> Library/More_BNFs.thy
  1281     BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy
  1282     BNF/Examples/* ~> BNF_Examples/*
  1283 
  1284   New theories:
  1285     Wellorder_Extension.thy (split from Zorn.thy)
  1286     Library/Cardinal_Notations.thy
  1287     Library/BNF_Axomatization.thy
  1288     BNF_Examples/Misc_Primcorec.thy
  1289     BNF_Examples/Stream_Processor.thy
  1290 
  1291   Discontinued theories:
  1292     BNF/BNF.thy
  1293     BNF/Equiv_Relations_More.thy
  1294 
  1295 INCOMPATIBILITY.
  1296 
  1297 * New (co)datatype package:
  1298   - Command 'primcorec' is fully implemented.
  1299   - Command 'datatype_new' generates size functions ("size_xxx" and
  1300     "size") as required by 'fun'.
  1301   - BNFs are integrated with the Lifting tool and new-style
  1302     (co)datatypes with Transfer.
  1303   - Renamed commands:
  1304       datatype_new_compat ~> datatype_compat
  1305       primrec_new ~> primrec
  1306       wrap_free_constructors ~> free_constructors
  1307     INCOMPATIBILITY.
  1308   - The generated constants "xxx_case" and "xxx_rec" have been renamed
  1309     "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
  1310     INCOMPATIBILITY.
  1311   - The constant "xxx_(un)fold" and related theorems are no longer
  1312     generated.  Use "xxx_(co)rec" or define "xxx_(un)fold" manually
  1313     using "prim(co)rec".
  1314     INCOMPATIBILITY.
  1315   - No discriminators are generated for nullary constructors by
  1316     default, eliminating the need for the odd "=:" syntax.
  1317     INCOMPATIBILITY.
  1318   - No discriminators or selectors are generated by default by
  1319     "datatype_new", unless custom names are specified or the new
  1320     "discs_sels" option is passed.
  1321     INCOMPATIBILITY.
  1322 
  1323 * Old datatype package:
  1324   - The generated theorems "xxx.cases" and "xxx.recs" have been
  1325     renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" ->
  1326     "sum.case").  INCOMPATIBILITY.
  1327   - The generated constants "xxx_case", "xxx_rec", and "xxx_size" have
  1328     been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g.,
  1329     "prod_case" ~> "case_prod").  INCOMPATIBILITY.
  1330 
  1331 * The types "'a list" and "'a option", their set and map functions,
  1332   their relators, and their selectors are now produced using the new
  1333   BNF-based datatype package.
  1334 
  1335   Renamed constants:
  1336     Option.set ~> set_option
  1337     Option.map ~> map_option
  1338     option_rel ~> rel_option
  1339 
  1340   Renamed theorems:
  1341     set_def ~> set_rec[abs_def]
  1342     map_def ~> map_rec[abs_def]
  1343     Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
  1344     option.recs ~> option.rec
  1345     list_all2_def ~> list_all2_iff
  1346     set.simps ~> set_simps (or the slightly different "list.set")
  1347     map.simps ~> list.map
  1348     hd.simps ~> list.sel(1)
  1349     tl.simps ~> list.sel(2-3)
  1350     the.simps ~> option.sel
  1351 
  1352 INCOMPATIBILITY.
  1353 
  1354 * The following map functions and relators have been renamed:
  1355     sum_map ~> map_sum
  1356     map_pair ~> map_prod
  1357     prod_rel ~> rel_prod
  1358     sum_rel ~> rel_sum
  1359     fun_rel ~> rel_fun
  1360     set_rel ~> rel_set
  1361     filter_rel ~> rel_filter
  1362     fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy")
  1363     cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy")
  1364     vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy")
  1365 
  1366 INCOMPATIBILITY.
  1367 
  1368 * Lifting and Transfer:
  1369   - a type variable as a raw type is supported
  1370   - stronger reflexivity prover
  1371   - rep_eq is always generated by lift_definition
  1372   - setup for Lifting/Transfer is now automated for BNFs
  1373     + holds for BNFs that do not contain a dead variable
  1374     + relator_eq, relator_mono, relator_distr, relator_domain,
  1375       relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total,
  1376       right_unique, right_total, left_unique, left_total are proved
  1377       automatically
  1378     + definition of a predicator is generated automatically
  1379     + simplification rules for a predicator definition are proved
  1380       automatically for datatypes
  1381   - consolidation of the setup of Lifting/Transfer
  1382     + property that a relator preservers reflexivity is not needed any
  1383       more
  1384       Minor INCOMPATIBILITY.
  1385     + left_total and left_unique rules are now transfer rules
  1386       (reflexivity_rule attribute not needed anymore)
  1387       INCOMPATIBILITY.
  1388     + Domainp does not have to be a separate assumption in
  1389       relator_domain theorems (=> more natural statement)
  1390       INCOMPATIBILITY.
  1391   - registration of code equations is more robust
  1392     Potential INCOMPATIBILITY.
  1393   - respectfulness proof obligation is preprocessed to a more readable
  1394     form
  1395     Potential INCOMPATIBILITY.
  1396   - eq_onp is always unfolded in respectfulness proof obligation
  1397     Potential INCOMPATIBILITY.
  1398   - unregister lifting setup for Code_Numeral.integer and
  1399     Code_Numeral.natural
  1400     Potential INCOMPATIBILITY.
  1401   - Lifting.invariant -> eq_onp
  1402     INCOMPATIBILITY.
  1403 
  1404 * New internal SAT solver "cdclite" that produces models and proof
  1405 traces.  This solver replaces the internal SAT solvers "enumerate" and
  1406 "dpll".  Applications that explicitly used one of these two SAT
  1407 solvers should use "cdclite" instead. In addition, "cdclite" is now
  1408 the default SAT solver for the "sat" and "satx" proof methods and
  1409 corresponding tactics; the old default can be restored using "declare
  1410 [[sat_solver = zchaff_with_proofs]]".  Minor INCOMPATIBILITY.
  1411 
  1412 * SMT module: A new version of the SMT module, temporarily called
  1413 "SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g.,
  1414 4.3). The new proof method is called "smt2". CVC3 and CVC4 are also
  1415 supported as oracles. Yices is no longer supported, because no version
  1416 of the solver can handle both SMT-LIB 2 and quantifiers.
  1417 
  1418 * Activation of Z3 now works via "z3_non_commercial" system option
  1419 (without requiring restart), instead of former settings variable
  1420 "Z3_NON_COMMERCIAL".  The option can be edited in Isabelle/jEdit menu
  1421 Plugin Options / Isabelle / General.
  1422 
  1423 * Sledgehammer:
  1424   - Z3 can now produce Isar proofs.
  1425   - MaSh overhaul:
  1426     . New SML-based learning algorithms eliminate the dependency on
  1427       Python and increase performance and reliability.
  1428     . MaSh and MeSh are now used by default together with the
  1429       traditional MePo (Meng-Paulson) relevance filter. To disable
  1430       MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin
  1431       Options / Isabelle / General to "none".
  1432   - New option:
  1433       smt_proofs
  1434   - Renamed options:
  1435       isar_compress ~> compress
  1436       isar_try0 ~> try0
  1437 
  1438 INCOMPATIBILITY.
  1439 
  1440 * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
  1441 
  1442 * Nitpick:
  1443   - Fixed soundness bug whereby mutually recursive datatypes could
  1444     take infinite values.
  1445   - Fixed soundness bug with low-level number functions such as
  1446     "Abs_Integ" and "Rep_Integ".
  1447   - Removed "std" option.
  1448   - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to
  1449     "hide_types".
  1450 
  1451 * Metis: Removed legacy proof method 'metisFT'. Use 'metis
  1452 (full_types)' instead. INCOMPATIBILITY.
  1453 
  1454 * Try0: Added 'algebra' and 'meson' to the set of proof methods.
  1455 
  1456 * Adjustion of INF and SUP operations:
  1457   - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
  1458   - Consolidated theorem names containing INFI and SUPR: have INF and
  1459     SUP instead uniformly.
  1460   - More aggressive normalization of expressions involving INF and Inf
  1461     or SUP and Sup.
  1462   - INF_image and SUP_image do not unfold composition.
  1463   - Dropped facts INF_comp, SUP_comp.
  1464   - Default congruence rules strong_INF_cong and strong_SUP_cong, with
  1465     simplifier implication in premises.  Generalize and replace former
  1466     INT_cong, SUP_cong
  1467 
  1468 INCOMPATIBILITY.
  1469 
  1470 * SUP and INF generalized to conditionally_complete_lattice.
  1471 
  1472 * Swapped orientation of facts image_comp and vimage_comp:
  1473 
  1474   image_compose ~> image_comp [symmetric]
  1475   image_comp ~> image_comp [symmetric]
  1476   vimage_compose ~> vimage_comp [symmetric]
  1477   vimage_comp ~> vimage_comp [symmetric]
  1478 
  1479 INCOMPATIBILITY.
  1480 
  1481 * Theory reorganization: split of Big_Operators.thy into
  1482 Groups_Big.thy and Lattices_Big.thy.
  1483 
  1484 * Consolidated some facts about big group operators:
  1485 
  1486     setsum_0' ~> setsum.neutral
  1487     setsum_0 ~> setsum.neutral_const
  1488     setsum_addf ~> setsum.distrib
  1489     setsum_cartesian_product ~> setsum.cartesian_product
  1490     setsum_cases ~> setsum.If_cases
  1491     setsum_commute ~> setsum.commute
  1492     setsum_cong ~> setsum.cong
  1493     setsum_delta ~> setsum.delta
  1494     setsum_delta' ~> setsum.delta'
  1495     setsum_diff1' ~> setsum.remove
  1496     setsum_empty ~> setsum.empty
  1497     setsum_infinite ~> setsum.infinite
  1498     setsum_insert ~> setsum.insert
  1499     setsum_inter_restrict'' ~> setsum.inter_filter
  1500     setsum_mono_zero_cong_left ~> setsum.mono_neutral_cong_left
  1501     setsum_mono_zero_cong_right ~> setsum.mono_neutral_cong_right
  1502     setsum_mono_zero_left ~> setsum.mono_neutral_left
  1503     setsum_mono_zero_right ~> setsum.mono_neutral_right
  1504     setsum_reindex ~> setsum.reindex
  1505     setsum_reindex_cong ~> setsum.reindex_cong
  1506     setsum_reindex_nonzero ~> setsum.reindex_nontrivial
  1507     setsum_restrict_set ~> setsum.inter_restrict
  1508     setsum_Plus ~> setsum.Plus
  1509     setsum_setsum_restrict ~> setsum.commute_restrict
  1510     setsum_Sigma ~> setsum.Sigma
  1511     setsum_subset_diff ~> setsum.subset_diff
  1512     setsum_Un_disjoint ~> setsum.union_disjoint
  1513     setsum_UN_disjoint ~> setsum.UNION_disjoint
  1514     setsum_Un_Int ~> setsum.union_inter
  1515     setsum_Union_disjoint ~> setsum.Union_disjoint
  1516     setsum_UNION_zero ~> setsum.Union_comp
  1517     setsum_Un_zero ~> setsum.union_inter_neutral
  1518     strong_setprod_cong ~> setprod.strong_cong
  1519     strong_setsum_cong ~> setsum.strong_cong
  1520     setprod_1' ~> setprod.neutral
  1521     setprod_1 ~> setprod.neutral_const
  1522     setprod_cartesian_product ~> setprod.cartesian_product
  1523     setprod_cong ~> setprod.cong
  1524     setprod_delta ~> setprod.delta
  1525     setprod_delta' ~> setprod.delta'
  1526     setprod_empty ~> setprod.empty
  1527     setprod_infinite ~> setprod.infinite
  1528     setprod_insert ~> setprod.insert
  1529     setprod_mono_one_cong_left ~> setprod.mono_neutral_cong_left
  1530     setprod_mono_one_cong_right ~> setprod.mono_neutral_cong_right
  1531     setprod_mono_one_left ~> setprod.mono_neutral_left
  1532     setprod_mono_one_right ~> setprod.mono_neutral_right
  1533     setprod_reindex ~> setprod.reindex
  1534     setprod_reindex_cong ~> setprod.reindex_cong
  1535     setprod_reindex_nonzero ~> setprod.reindex_nontrivial
  1536     setprod_Sigma ~> setprod.Sigma
  1537     setprod_subset_diff ~> setprod.subset_diff
  1538     setprod_timesf ~> setprod.distrib
  1539     setprod_Un2 ~> setprod.union_diff2
  1540     setprod_Un_disjoint ~> setprod.union_disjoint
  1541     setprod_UN_disjoint ~> setprod.UNION_disjoint
  1542     setprod_Un_Int ~> setprod.union_inter
  1543     setprod_Union_disjoint ~> setprod.Union_disjoint
  1544     setprod_Un_one ~> setprod.union_inter_neutral
  1545 
  1546   Dropped setsum_cong2 (simple variant of setsum.cong).
  1547   Dropped setsum_inter_restrict' (simple variant of setsum.inter_restrict)
  1548   Dropped setsum_reindex_id, setprod_reindex_id
  1549     (simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]).
  1550 
  1551 INCOMPATIBILITY.
  1552 
  1553 * Abolished slightly odd global lattice interpretation for min/max.
  1554 
  1555   Fact consolidations:
  1556     min_max.inf_assoc ~> min.assoc
  1557     min_max.inf_commute ~> min.commute
  1558     min_max.inf_left_commute ~> min.left_commute
  1559     min_max.inf_idem ~> min.idem
  1560     min_max.inf_left_idem ~> min.left_idem
  1561     min_max.inf_right_idem ~> min.right_idem
  1562     min_max.sup_assoc ~> max.assoc
  1563     min_max.sup_commute ~> max.commute
  1564     min_max.sup_left_commute ~> max.left_commute
  1565     min_max.sup_idem ~> max.idem
  1566     min_max.sup_left_idem ~> max.left_idem
  1567     min_max.sup_inf_distrib1 ~> max_min_distrib2
  1568     min_max.sup_inf_distrib2 ~> max_min_distrib1
  1569     min_max.inf_sup_distrib1 ~> min_max_distrib2
  1570     min_max.inf_sup_distrib2 ~> min_max_distrib1
  1571     min_max.distrib ~> min_max_distribs
  1572     min_max.inf_absorb1 ~> min.absorb1
  1573     min_max.inf_absorb2 ~> min.absorb2
  1574     min_max.sup_absorb1 ~> max.absorb1
  1575     min_max.sup_absorb2 ~> max.absorb2
  1576     min_max.le_iff_inf ~> min.absorb_iff1
  1577     min_max.le_iff_sup ~> max.absorb_iff2
  1578     min_max.inf_le1 ~> min.cobounded1
  1579     min_max.inf_le2 ~> min.cobounded2
  1580     le_maxI1, min_max.sup_ge1 ~> max.cobounded1
  1581     le_maxI2, min_max.sup_ge2 ~> max.cobounded2
  1582     min_max.le_infI1 ~> min.coboundedI1
  1583     min_max.le_infI2 ~> min.coboundedI2
  1584     min_max.le_supI1 ~> max.coboundedI1
  1585     min_max.le_supI2 ~> max.coboundedI2
  1586     min_max.less_infI1 ~> min.strict_coboundedI1
  1587     min_max.less_infI2 ~> min.strict_coboundedI2
  1588     min_max.less_supI1 ~> max.strict_coboundedI1
  1589     min_max.less_supI2 ~> max.strict_coboundedI2
  1590     min_max.inf_mono ~> min.mono
  1591     min_max.sup_mono ~> max.mono
  1592     min_max.le_infI, min_max.inf_greatest ~> min.boundedI
  1593     min_max.le_supI, min_max.sup_least ~> max.boundedI
  1594     min_max.le_inf_iff ~> min.bounded_iff
  1595     min_max.le_sup_iff ~> max.bounded_iff
  1596 
  1597 For min_max.inf_sup_aci, prefer (one of) min.commute, min.assoc,
  1598 min.left_commute, min.left_idem, max.commute, max.assoc,
  1599 max.left_commute, max.left_idem directly.
  1600 
  1601 For min_max.inf_sup_ord, prefer (one of) min.cobounded1,
  1602 min.cobounded2, max.cobounded1m max.cobounded2 directly.
  1603 
  1604 For min_ac or max_ac, prefer more general collection ac_simps.
  1605 
  1606 INCOMPATIBILITY.
  1607 
  1608 * Theorem disambiguation Inf_le_Sup (on finite sets) ~>
  1609 Inf_fin_le_Sup_fin.  INCOMPATIBILITY.
  1610 
  1611 * Qualified constant names Wellfounded.acc, Wellfounded.accp.
  1612 INCOMPATIBILITY.
  1613 
  1614 * Fact generalization and consolidation:
  1615     neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
  1616 
  1617 INCOMPATIBILITY.
  1618 
  1619 * Purely algebraic definition of even.  Fact generalization and
  1620   consolidation:
  1621     nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd
  1622     even_zero_(nat|int) ~> even_zero
  1623 
  1624 INCOMPATIBILITY.
  1625 
  1626 * Abolished neg_numeral.
  1627   - Canonical representation for minus one is "- 1".
  1628   - Canonical representation for other negative numbers is "- (numeral _)".
  1629   - When devising rule sets for number calculation, consider the
  1630     following canonical cases: 0, 1, numeral _, - 1, - numeral _.
  1631   - HOLogic.dest_number also recognizes numerals in non-canonical forms
  1632     like "numeral One", "- numeral One", "- 0" and even "- ... - _".
  1633   - Syntax for negative numerals is mere input syntax.
  1634 
  1635 INCOMPATIBILITY.
  1636 
  1637 * Reduced name variants for rules on associativity and commutativity:
  1638 
  1639     add_assoc ~> add.assoc
  1640     add_commute ~> add.commute
  1641     add_left_commute ~> add.left_commute
  1642     mult_assoc ~> mult.assoc
  1643     mult_commute ~> mult.commute
  1644     mult_left_commute ~> mult.left_commute
  1645     nat_add_assoc ~> add.assoc
  1646     nat_add_commute ~> add.commute
  1647     nat_add_left_commute ~> add.left_commute
  1648     nat_mult_assoc ~> mult.assoc
  1649     nat_mult_commute ~> mult.commute
  1650     eq_assoc ~> iff_assoc
  1651     eq_left_commute ~> iff_left_commute
  1652 
  1653 INCOMPATIBILITY.
  1654 
  1655 * Fact collections add_ac and mult_ac are considered old-fashioned.
  1656 Prefer ac_simps instead, or specify rules
  1657 (add|mult).(assoc|commute|left_commute) individually.
  1658 
  1659 * Elimination of fact duplicates:
  1660     equals_zero_I ~> minus_unique
  1661     diff_eq_0_iff_eq ~> right_minus_eq
  1662     nat_infinite ~> infinite_UNIV_nat
  1663     int_infinite ~> infinite_UNIV_int
  1664 
  1665 INCOMPATIBILITY.
  1666 
  1667 * Fact name consolidation:
  1668     diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus
  1669     minus_le_self_iff ~> neg_less_eq_nonneg
  1670     le_minus_self_iff ~> less_eq_neg_nonpos
  1671     neg_less_nonneg ~> neg_less_pos
  1672     less_minus_self_iff ~> less_neg_neg [simp]
  1673 
  1674 INCOMPATIBILITY.
  1675 
  1676 * More simplification rules on unary and binary minus:
  1677 add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,
  1678 add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,
  1679 add_minus_cancel, diff_add_cancel, le_add_same_cancel1,
  1680 le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,
  1681 minus_add_cancel, uminus_add_conv_diff.  These correspondingly have
  1682 been taken away from fact collections algebra_simps and field_simps.
  1683 INCOMPATIBILITY.
  1684 
  1685 To restore proofs, the following patterns are helpful:
  1686 
  1687 a) Arbitrary failing proof not involving "diff_def":
  1688 Consider simplification with algebra_simps or field_simps.
  1689 
  1690 b) Lifting rules from addition to subtraction:
  1691 Try with "using <rule for addition> of [... "- _" ...]" by simp".
  1692 
  1693 c) Simplification with "diff_def": just drop "diff_def".
  1694 Consider simplification with algebra_simps or field_simps;
  1695 or the brute way with
  1696 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
  1697 
  1698 * Introduce bdd_above and bdd_below in theory
  1699 Conditionally_Complete_Lattices, use them instead of explicitly
  1700 stating boundedness of sets.
  1701 
  1702 * ccpo.admissible quantifies only over non-empty chains to allow more
  1703 syntax-directed proof rules; the case of the empty chain shows up as
  1704 additional case in fixpoint induction proofs.  INCOMPATIBILITY.
  1705 
  1706 * Removed and renamed theorems in Series:
  1707   summable_le         ~>  suminf_le
  1708   suminf_le           ~>  suminf_le_const
  1709   series_pos_le       ~>  setsum_le_suminf
  1710   series_pos_less     ~>  setsum_less_suminf
  1711   suminf_ge_zero      ~>  suminf_nonneg
  1712   suminf_gt_zero      ~>  suminf_pos
  1713   suminf_gt_zero_iff  ~>  suminf_pos_iff
  1714   summable_sumr_LIMSEQ_suminf  ~>  summable_LIMSEQ
  1715   suminf_0_le         ~>  suminf_nonneg [rotate]
  1716   pos_summable        ~>  summableI_nonneg_bounded
  1717   ratio_test          ~>  summable_ratio_test
  1718 
  1719   removed series_zero, replaced by sums_finite
  1720 
  1721   removed auxiliary lemmas:
  1722 
  1723     sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group,
  1724     half, le_Suc_ex_iff, lemma_realpow_diff_sumr,
  1725     real_setsum_nat_ivl_bounded, summable_le2, ratio_test_lemma2,
  1726     sumr_minus_one_realpow_zerom, sumr_one_lb_realpow_zero,
  1727     summable_convergent_sumr_iff, sumr_diff_mult_const
  1728 
  1729 INCOMPATIBILITY.
  1730 
  1731 * Replace (F)DERIV syntax by has_derivative:
  1732   - "(f has_derivative f') (at x within s)" replaces "FDERIV f x : s : f'"
  1733 
  1734   - "(f has_field_derivative f') (at x within s)" replaces "DERIV f x : s : f'"
  1735 
  1736   - "f differentiable at x within s" replaces "_ differentiable _ in _" syntax
  1737 
  1738   - removed constant isDiff
  1739 
  1740   - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as
  1741     input syntax.
  1742 
  1743   - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed.
  1744 
  1745   - Renamed FDERIV_... lemmas to has_derivative_...
  1746 
  1747   - renamed deriv (the syntax constant used for "DERIV _ _ :> _") to DERIV
  1748 
  1749   - removed DERIV_intros, has_derivative_eq_intros
  1750 
  1751   - introduced derivative_intros and deriative_eq_intros which
  1752     includes now rules for DERIV, has_derivative and
  1753     has_vector_derivative.
  1754 
  1755   - Other renamings:
  1756     differentiable_def        ~>  real_differentiable_def
  1757     differentiableE           ~>  real_differentiableE
  1758     fderiv_def                ~>  has_derivative_at
  1759     field_fderiv_def          ~>  field_has_derivative_at
  1760     isDiff_der                ~>  differentiable_def
  1761     deriv_fderiv              ~>  has_field_derivative_def
  1762     deriv_def                 ~>  DERIV_def
  1763 
  1764 INCOMPATIBILITY.
  1765 
  1766 * Include more theorems in continuous_intros. Remove the
  1767 continuous_on_intros, isCont_intros collections, these facts are now
  1768 in continuous_intros.
  1769 
  1770 * Theorems about complex numbers are now stated only using Re and Im,
  1771 the Complex constructor is not used anymore. It is possible to use
  1772 primcorec to defined the behaviour of a complex-valued function.
  1773 
  1774 Removed theorems about the Complex constructor from the simpset, they
  1775 are available as the lemma collection legacy_Complex_simps. This
  1776 especially removes
  1777 
  1778     i_complex_of_real: "ii * complex_of_real r = Complex 0 r".
  1779 
  1780 Instead the reverse direction is supported with
  1781     Complex_eq: "Complex a b = a + \<i> * b"
  1782 
  1783 Moved csqrt from Fundamental_Algebra_Theorem to Complex.
  1784 
  1785   Renamings:
  1786     Re/Im                  ~>  complex.sel
  1787     complex_Re/Im_zero     ~>  zero_complex.sel
  1788     complex_Re/Im_add      ~>  plus_complex.sel
  1789     complex_Re/Im_minus    ~>  uminus_complex.sel
  1790     complex_Re/Im_diff     ~>  minus_complex.sel
  1791     complex_Re/Im_one      ~>  one_complex.sel
  1792     complex_Re/Im_mult     ~>  times_complex.sel
  1793     complex_Re/Im_inverse  ~>  inverse_complex.sel
  1794     complex_Re/Im_scaleR   ~>  scaleR_complex.sel
  1795     complex_Re/Im_i        ~>  ii.sel
  1796     complex_Re/Im_cnj      ~>  cnj.sel
  1797     Re/Im_cis              ~>  cis.sel
  1798 
  1799     complex_divide_def   ~>  divide_complex_def
  1800     complex_norm_def     ~>  norm_complex_def
  1801     cmod_def             ~>  norm_complex_de
  1802 
  1803   Removed theorems:
  1804     complex_zero_def
  1805     complex_add_def
  1806     complex_minus_def
  1807     complex_diff_def
  1808     complex_one_def
  1809     complex_mult_def
  1810     complex_inverse_def
  1811     complex_scaleR_def
  1812 
  1813 INCOMPATIBILITY.
  1814 
  1815 * Theory Lubs moved HOL image to HOL-Library. It is replaced by
  1816 Conditionally_Complete_Lattices.  INCOMPATIBILITY.
  1817 
  1818 * HOL-Library: new theory src/HOL/Library/Tree.thy.
  1819 
  1820 * HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it
  1821 is subsumed by session Kleene_Algebra in AFP.
  1822 
  1823 * HOL-Library / theory RBT: various constants and facts are hidden;
  1824 lifting setup is unregistered.  INCOMPATIBILITY.
  1825 
  1826 * HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
  1827 
  1828 * HOL-Word: bit representations prefer type bool over type bit.
  1829 INCOMPATIBILITY.
  1830 
  1831 * HOL-Word:
  1832   - Abandoned fact collection "word_arith_alts", which is a duplicate
  1833     of "word_arith_wis".
  1834   - Dropped first (duplicated) element in fact collections
  1835     "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
  1836     "uint_word_arith_bintrs".
  1837 
  1838 * HOL-Number_Theory:
  1839   - consolidated the proofs of the binomial theorem
  1840   - the function fib is again of type nat => nat and not overloaded
  1841   - no more references to Old_Number_Theory in the HOL libraries
  1842     (except the AFP)
  1843 
  1844 INCOMPATIBILITY.
  1845 
  1846 * HOL-Multivariate_Analysis:
  1847   - Type class ordered_real_vector for ordered vector spaces.
  1848   - New theory Complex_Basic_Analysis defining complex derivatives,
  1849     holomorphic functions, etc., ported from HOL Light's canal.ml.
  1850   - Changed order of ordered_euclidean_space to be compatible with
  1851     pointwise ordering on products. Therefore instance of
  1852     conditionally_complete_lattice and ordered_real_vector.
  1853     INCOMPATIBILITY: use box instead of greaterThanLessThan or
  1854     explicit set-comprehensions with eucl_less for other (half-)open
  1855     intervals.
  1856   - removed dependencies on type class ordered_euclidean_space with
  1857     introduction of "cbox" on euclidean_space
  1858     - renamed theorems:
  1859         interval ~> box
  1860         mem_interval ~> mem_box
  1861         interval_eq_empty ~> box_eq_empty
  1862         interval_ne_empty ~> box_ne_empty
  1863         interval_sing(1) ~> cbox_sing
  1864         interval_sing(2) ~> box_sing
  1865         subset_interval_imp ~> subset_box_imp
  1866         subset_interval ~> subset_box
  1867         open_interval ~> open_box
  1868         closed_interval ~> closed_cbox
  1869         interior_closed_interval ~> interior_cbox
  1870         bounded_closed_interval ~> bounded_cbox
  1871         compact_interval ~> compact_cbox
  1872         bounded_subset_closed_interval_symmetric ~> bounded_subset_cbox_symmetric
  1873         bounded_subset_closed_interval ~> bounded_subset_cbox
  1874         mem_interval_componentwiseI ~> mem_box_componentwiseI
  1875         convex_box ~> convex_prod
  1876         rel_interior_real_interval ~> rel_interior_real_box
  1877         convex_interval ~> convex_box
  1878         convex_hull_eq_real_interval ~> convex_hull_eq_real_cbox
  1879         frechet_derivative_within_closed_interval ~> frechet_derivative_within_cbox
  1880         content_closed_interval' ~> content_cbox'
  1881         elementary_subset_interval ~> elementary_subset_box
  1882         diameter_closed_interval ~> diameter_cbox
  1883         frontier_closed_interval ~> frontier_cbox
  1884         frontier_open_interval ~> frontier_box
  1885         bounded_subset_open_interval_symmetric ~> bounded_subset_box_symmetric
  1886         closure_open_interval ~> closure_box
  1887         open_closed_interval_convex ~> open_cbox_convex
  1888         open_interval_midpoint ~> box_midpoint
  1889         content_image_affinity_interval ~> content_image_affinity_cbox
  1890         is_interval_interval ~> is_interval_cbox + is_interval_box + is_interval_closed_interval
  1891         bounded_interval ~> bounded_closed_interval + bounded_boxes
  1892 
  1893     - respective theorems for intervals over the reals:
  1894         content_closed_interval + content_cbox
  1895         has_integral + has_integral_real
  1896         fine_division_exists + fine_division_exists_real
  1897         has_integral_null + has_integral_null_real
  1898         tagged_division_union_interval + tagged_division_union_interval_real
  1899         has_integral_const + has_integral_const_real
  1900         integral_const + integral_const_real
  1901         has_integral_bound + has_integral_bound_real
  1902         integrable_continuous + integrable_continuous_real
  1903         integrable_subinterval + integrable_subinterval_real
  1904         has_integral_reflect_lemma + has_integral_reflect_lemma_real
  1905         integrable_reflect + integrable_reflect_real
  1906         integral_reflect + integral_reflect_real
  1907         image_affinity_interval + image_affinity_cbox
  1908         image_smult_interval + image_smult_cbox
  1909         integrable_const + integrable_const_ivl
  1910         integrable_on_subinterval + integrable_on_subcbox
  1911 
  1912   - renamed theorems:
  1913     derivative_linear         ~>  has_derivative_bounded_linear
  1914     derivative_is_linear      ~>  has_derivative_linear
  1915     bounded_linear_imp_linear ~>  bounded_linear.linear
  1916 
  1917 * HOL-Probability:
  1918   - Renamed positive_integral to nn_integral:
  1919 
  1920     . Renamed all lemmas "*positive_integral*" to *nn_integral*"
  1921       positive_integral_positive ~> nn_integral_nonneg
  1922 
  1923     . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
  1924 
  1925   - replaced the Lebesgue integral on real numbers by the more general
  1926     Bochner integral for functions into a real-normed vector space.
  1927 
  1928     integral_zero               ~>  integral_zero / integrable_zero
  1929     integral_minus              ~>  integral_minus / integrable_minus
  1930     integral_add                ~>  integral_add / integrable_add
  1931     integral_diff               ~>  integral_diff / integrable_diff
  1932     integral_setsum             ~>  integral_setsum / integrable_setsum
  1933     integral_multc              ~>  integral_mult_left / integrable_mult_left
  1934     integral_cmult              ~>  integral_mult_right / integrable_mult_right
  1935     integral_triangle_inequality~>  integral_norm_bound
  1936     integrable_nonneg           ~>  integrableI_nonneg
  1937     integral_positive           ~>  integral_nonneg_AE
  1938     integrable_abs_iff          ~>  integrable_abs_cancel
  1939     positive_integral_lim_INF   ~>  nn_integral_liminf
  1940     lebesgue_real_affine        ~>  lborel_real_affine
  1941     borel_integral_has_integral ~>  has_integral_lebesgue_integral
  1942     integral_indicator          ~>
  1943          integral_real_indicator / integrable_real_indicator
  1944     positive_integral_fst       ~>  nn_integral_fst'
  1945     positive_integral_fst_measurable ~> nn_integral_fst
  1946     positive_integral_snd_measurable ~> nn_integral_snd
  1947 
  1948     integrable_fst_measurable   ~>
  1949          integral_fst / integrable_fst / AE_integrable_fst
  1950 
  1951     integrable_snd_measurable   ~>
  1952          integral_snd / integrable_snd / AE_integrable_snd
  1953 
  1954     integral_monotone_convergence  ~>
  1955          integral_monotone_convergence / integrable_monotone_convergence
  1956 
  1957     integral_monotone_convergence_at_top  ~>
  1958          integral_monotone_convergence_at_top /
  1959          integrable_monotone_convergence_at_top
  1960 
  1961     has_integral_iff_positive_integral_lebesgue  ~>
  1962          has_integral_iff_has_bochner_integral_lebesgue_nonneg
  1963 
  1964     lebesgue_integral_has_integral  ~>
  1965          has_integral_integrable_lebesgue_nonneg
  1966 
  1967     positive_integral_lebesgue_has_integral  ~>
  1968          integral_has_integral_lebesgue_nonneg /
  1969          integrable_has_integral_lebesgue_nonneg
  1970 
  1971     lebesgue_integral_real_affine  ~>
  1972          nn_integral_real_affine
  1973 
  1974     has_integral_iff_positive_integral_lborel  ~>
  1975          integral_has_integral_nonneg / integrable_has_integral_nonneg
  1976 
  1977     The following theorems where removed:
  1978 
  1979     lebesgue_integral_nonneg
  1980     lebesgue_integral_uminus
  1981     lebesgue_integral_cmult
  1982     lebesgue_integral_multc
  1983     lebesgue_integral_cmult_nonneg
  1984     integral_cmul_indicator
  1985     integral_real
  1986 
  1987   - Formalized properties about exponentially, Erlang, and normal
  1988     distributed random variables.
  1989 
  1990 * HOL-Decision_Procs: Separate command 'approximate' for approximative
  1991 computation in src/HOL/Decision_Procs/Approximation.  Minor
  1992 INCOMPATIBILITY.
  1993 
  1994 
  1995 *** Scala ***
  1996 
  1997 * The signature and semantics of Document.Snapshot.cumulate_markup /
  1998 select_markup have been clarified.  Markup is now traversed in the
  1999 order of reports given by the prover: later markup is usually more
  2000 specific and may override results accumulated so far.  The elements
  2001 guard is mandatory and checked precisely.  Subtle INCOMPATIBILITY.
  2002 
  2003 * Substantial reworking of internal PIDE protocol communication
  2004 channels.  INCOMPATIBILITY.
  2005 
  2006 
  2007 *** ML ***
  2008 
  2009 * Subtle change of semantics of Thm.eq_thm: theory stamps are not
  2010 compared (according to Thm.thm_ord), but assumed to be covered by the
  2011 current background theory.  Thus equivalent data produced in different
  2012 branches of the theory graph usually coincides (e.g. relevant for
  2013 theory merge).  Note that the softer Thm.eq_thm_prop is often more
  2014 appropriate than Thm.eq_thm.
  2015 
  2016 * Proper context for basic Simplifier operations: rewrite_rule,
  2017 rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to
  2018 pass runtime Proof.context (and ensure that the simplified entity
  2019 actually belongs to it).
  2020 
  2021 * Proper context discipline for read_instantiate and instantiate_tac:
  2022 variables that are meant to become schematic need to be given as
  2023 fixed, and are generalized by the explicit context of local variables.
  2024 This corresponds to Isar attributes "where" and "of" with 'for'
  2025 declaration.  INCOMPATIBILITY, also due to potential change of indices
  2026 of schematic variables.
  2027 
  2028 * Moved ML_Compiler.exn_trace and other operations on exceptions to
  2029 structure Runtime.  Minor INCOMPATIBILITY.
  2030 
  2031 * Discontinued old Toplevel.debug in favour of system option
  2032 "ML_exception_trace", which may be also declared within the context
  2033 via "declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
  2034 
  2035 * Renamed configuration option "ML_trace" to "ML_source_trace". Minor
  2036 INCOMPATIBILITY.
  2037 
  2038 * Configuration option "ML_print_depth" controls the pretty-printing
  2039 depth of the ML compiler within the context.  The old print_depth in
  2040 ML is still available as default_print_depth, but rarely used.  Minor
  2041 INCOMPATIBILITY.
  2042 
  2043 * Toplevel function "use" refers to raw ML bootstrap environment,
  2044 without Isar context nor antiquotations.  Potential INCOMPATIBILITY.
  2045 Note that 'ML_file' is the canonical command to load ML files into the
  2046 formal context.
  2047 
  2048 * Simplified programming interface to define ML antiquotations, see
  2049 structure ML_Antiquotation.  Minor INCOMPATIBILITY.
  2050 
  2051 * ML antiquotation @{here} refers to its source position, which is
  2052 occasionally useful for experimentation and diagnostic purposes.
  2053 
  2054 * ML antiquotation @{path} produces a Path.T value, similarly to
  2055 Path.explode, but with compile-time check against the file-system and
  2056 some PIDE markup.  Note that unlike theory source, ML does not have a
  2057 well-defined master directory, so an absolute symbolic path
  2058 specification is usually required, e.g. "~~/src/HOL".
  2059 
  2060 * ML antiquotation @{print} inlines a function to print an arbitrary
  2061 ML value, which is occasionally useful for diagnostic or demonstration
  2062 purposes.
  2063 
  2064 
  2065 *** System ***
  2066 
  2067 * Proof General with its traditional helper scripts is now an optional
  2068 Isabelle component, e.g. see ProofGeneral-4.2-2 from the Isabelle
  2069 component repository http://isabelle.in.tum.de/components/.  Note that
  2070 the "system" manual provides general explanations about add-on
  2071 components, especially those that are not bundled with the release.
  2072 
  2073 * The raw Isabelle process executable has been renamed from
  2074 "isabelle-process" to "isabelle_process", which conforms to common
  2075 shell naming conventions, and allows to define a shell function within
  2076 the Isabelle environment to avoid dynamic path lookup.  Rare
  2077 incompatibility for old tools that do not use the ISABELLE_PROCESS
  2078 settings variable.
  2079 
  2080 * Former "isabelle tty" has been superseded by "isabelle console",
  2081 with implicit build like "isabelle jedit", and without the mostly
  2082 obsolete Isar TTY loop.
  2083 
  2084 * Simplified "isabelle display" tool.  Settings variables DVI_VIEWER
  2085 and PDF_VIEWER now refer to the actual programs, not shell
  2086 command-lines.  Discontinued option -c: invocation may be asynchronous
  2087 via desktop environment, without any special precautions.  Potential
  2088 INCOMPATIBILITY with ambitious private settings.
  2089 
  2090 * Removed obsolete "isabelle unsymbolize".  Note that the usual format
  2091 for email communication is the Unicode rendering of Isabelle symbols,
  2092 as produced by Isabelle/jEdit, for example.
  2093 
  2094 * Removed obsolete tool "wwwfind". Similar functionality may be
  2095 integrated into Isabelle/jEdit eventually.
  2096 
  2097 * Improved 'display_drafts' concerning desktop integration and
  2098 repeated invocation in PIDE front-end: re-use single file
  2099 $ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.
  2100 
  2101 * Session ROOT specifications require explicit 'document_files' for
  2102 robust dependencies on LaTeX sources.  Only these explicitly given
  2103 files are copied to the document output directory, before document
  2104 processing is started.
  2105 
  2106 * Windows: support for regular TeX installation (e.g. MiKTeX) instead
  2107 of TeX Live from Cygwin.
  2108 
  2109 
  2110 
  2111 New in Isabelle2013-2 (December 2013)
  2112 -------------------------------------
  2113 
  2114 *** Prover IDE -- Isabelle/Scala/jEdit ***
  2115 
  2116 * More robust editing of running commands with internal forks,
  2117 e.g. non-terminating 'by' steps.
  2118 
  2119 * More relaxed Sledgehammer panel: avoid repeated application of query
  2120 after edits surrounding the command location.
  2121 
  2122 * More status information about commands that are interrupted
  2123 accidentally (via physical event or Poly/ML runtime system signal,
  2124 e.g. out-of-memory).
  2125 
  2126 
  2127 *** System ***
  2128 
  2129 * More robust termination of external processes managed by
  2130 Isabelle/ML: support cancellation of tasks within the range of
  2131 milliseconds, as required for PIDE document editing with automatically
  2132 tried tools (e.g. Sledgehammer).
  2133 
  2134 * Reactivated Isabelle/Scala kill command for external processes on
  2135 Mac OS X, which was accidentally broken in Isabelle2013-1 due to a
  2136 workaround for some Debian/Ubuntu Linux versions from 2013.
  2137 
  2138 
  2139 
  2140 New in Isabelle2013-1 (November 2013)
  2141 -------------------------------------
  2142 
  2143 *** General ***
  2144 
  2145 * Discontinued obsolete 'uses' within theory header.  Note that
  2146 commands like 'ML_file' work without separate declaration of file
  2147 dependencies.  Minor INCOMPATIBILITY.
  2148 
  2149 * Discontinued redundant 'use' command, which was superseded by
  2150 'ML_file' in Isabelle2013.  Minor INCOMPATIBILITY.
  2151 
  2152 * Simplified subscripts within identifiers, using plain \<^sub>
  2153 instead of the second copy \<^isub> and \<^isup>.  Superscripts are
  2154 only for literal tokens within notation; explicit mixfix annotations
  2155 for consts or fixed variables may be used as fall-back for unusual
  2156 names.  Obsolete \<twosuperior> has been expanded to \<^sup>2 in
  2157 Isabelle/HOL.  INCOMPATIBILITY, use "isabelle update_sub_sup" to
  2158 standardize symbols as a starting point for further manual cleanup.
  2159 The ML reference variable "legacy_isub_isup" may be set as temporary
  2160 workaround, to make the prover accept a subset of the old identifier
  2161 syntax.
  2162 
  2163 * Document antiquotations: term style "isub" has been renamed to
  2164 "sub".  Minor INCOMPATIBILITY.
  2165 
  2166 * Uniform management of "quick_and_dirty" as system option (see also
  2167 "isabelle options"), configuration option within the context (see also
  2168 Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor
  2169 INCOMPATIBILITY, need to use more official Isabelle means to access
  2170 quick_and_dirty, instead of historical poking into mutable reference.
  2171 
  2172 * Renamed command 'print_configs' to 'print_options'.  Minor
  2173 INCOMPATIBILITY.
  2174 
  2175 * Proper diagnostic command 'print_state'.  Old 'pr' (with its
  2176 implicit change of some global references) is retained for now as
  2177 control command, e.g. for ProofGeneral 3.7.x.
  2178 
  2179 * Discontinued 'print_drafts' command with its old-fashioned PS output
  2180 and Unix command-line print spooling.  Minor INCOMPATIBILITY: use
  2181 'display_drafts' instead and print via the regular document viewer.
  2182 
  2183 * Updated and extended "isar-ref" and "implementation" manual,
  2184 eliminated old "ref" manual.
  2185 
  2186 
  2187 *** Prover IDE -- Isabelle/Scala/jEdit ***
  2188 
  2189 * New manual "jedit" for Isabelle/jEdit, see isabelle doc or
  2190 Documentation panel.
  2191 
  2192 * Dockable window "Documentation" provides access to Isabelle
  2193 documentation.
  2194 
  2195 * Dockable window "Find" provides query operations for formal entities
  2196 (GUI front-end to 'find_theorems' command).
  2197 
  2198 * Dockable window "Sledgehammer" manages asynchronous / parallel
  2199 sledgehammer runs over existing document sources, independently of
  2200 normal editing and checking process.
  2201 
  2202 * Dockable window "Timing" provides an overview of relevant command
  2203 timing information, depending on option jedit_timing_threshold.  The
  2204 same timing information is shown in the extended tooltip of the
  2205 command keyword, when hovering the mouse over it while the CONTROL or
  2206 COMMAND modifier is pressed.
  2207 
  2208 * Improved dockable window "Theories": Continuous checking of proof
  2209 document (visible and required parts) may be controlled explicitly,
  2210 using check box or shortcut "C+e ENTER".  Individual theory nodes may
  2211 be marked explicitly as required and checked in full, using check box
  2212 or shortcut "C+e SPACE".
  2213 
  2214 * Improved completion mechanism, which is now managed by the
  2215 Isabelle/jEdit plugin instead of SideKick.  Refined table of Isabelle
  2216 symbol abbreviations (see $ISABELLE_HOME/etc/symbols).
  2217 
  2218 * Standard jEdit keyboard shortcut C+b complete-word is remapped to
  2219 isabelle.complete for explicit completion in Isabelle sources.
  2220 INCOMPATIBILITY wrt. jEdit defaults, may have to invent new shortcuts
  2221 to resolve conflict.
  2222 
  2223 * Improved support of various "minor modes" for Isabelle NEWS,
  2224 options, session ROOT etc., with completion and SideKick tree view.
  2225 
  2226 * Strictly monotonic document update, without premature cancellation of
  2227 running transactions that are still needed: avoid reset/restart of
  2228 such command executions while editing.
  2229 
  2230 * Support for asynchronous print functions, as overlay to existing
  2231 document content.
  2232 
  2233 * Support for automatic tools in HOL, which try to prove or disprove
  2234 toplevel theorem statements.
  2235 
  2236 * Action isabelle.reset-font-size resets main text area font size
  2237 according to Isabelle/Scala plugin option "jedit_font_reset_size" (see
  2238 also "Plugin Options / Isabelle / General").  It can be bound to some
  2239 keyboard shortcut by the user (e.g. C+0 and/or C+NUMPAD0).
  2240 
  2241 * File specifications in jEdit (e.g. file browser) may refer to
  2242 $ISABELLE_HOME and $ISABELLE_HOME_USER on all platforms.  Discontinued
  2243 obsolete $ISABELLE_HOME_WINDOWS variable.
  2244 
  2245 * Improved support for Linux look-and-feel "GTK+", see also "Utilities
  2246 / Global Options / Appearance".
  2247 
  2248 * Improved support of native Mac OS X functionality via "MacOSX"
  2249 plugin, which is now enabled by default.
  2250 
  2251 
  2252 *** Pure ***
  2253 
  2254 * Commands 'interpretation' and 'sublocale' are now target-sensitive.
  2255 In particular, 'interpretation' allows for non-persistent
  2256 interpretation within "context ... begin ... end" blocks offering a
  2257 light-weight alternative to 'sublocale'.  See "isar-ref" manual for
  2258 details.
  2259 
  2260 * Improved locales diagnostic command 'print_dependencies'.
  2261 
  2262 * Discontinued obsolete 'axioms' command, which has been marked as
  2263 legacy since Isabelle2009-2.  INCOMPATIBILITY, use 'axiomatization'
  2264 instead, while observing its uniform scope for polymorphism.
  2265 
  2266 * Discontinued empty name bindings in 'axiomatization'.
  2267 INCOMPATIBILITY.
  2268 
  2269 * System option "proofs" has been discontinued.  Instead the global
  2270 state of Proofterm.proofs is persistently compiled into logic images
  2271 as required, notably HOL-Proofs.  Users no longer need to change
  2272 Proofterm.proofs dynamically.  Minor INCOMPATIBILITY.
  2273 
  2274 * Syntax translation functions (print_translation etc.) always depend
  2275 on Proof.context.  Discontinued former "(advanced)" option -- this is
  2276 now the default.  Minor INCOMPATIBILITY.
  2277 
  2278 * Former global reference trace_unify_fail is now available as
  2279 configuration option "unify_trace_failure" (global context only).
  2280 
  2281 * SELECT_GOAL now retains the syntactic context of the overall goal
  2282 state (schematic variables etc.).  Potential INCOMPATIBILITY in rare
  2283 situations.
  2284 
  2285 
  2286 *** HOL ***
  2287 
  2288 * Stronger precedence of syntax for big intersection and union on
  2289 sets, in accordance with corresponding lattice operations.
  2290 INCOMPATIBILITY.
  2291 
  2292 * Notation "{p:A. P}" now allows tuple patterns as well.
  2293 
  2294 * Nested case expressions are now translated in a separate check phase
  2295 rather than during parsing. The data for case combinators is separated
  2296 from the datatype package. The declaration attribute
  2297 "case_translation" can be used to register new case combinators:
  2298 
  2299   declare [[case_translation case_combinator constructor1 ... constructorN]]
  2300 
  2301 * Code generator:
  2302   - 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' /
  2303     'code_instance'.
  2304   - 'code_identifier' declares name hints for arbitrary identifiers in
  2305     generated code, subsuming 'code_modulename'.
  2306 
  2307 See the isar-ref manual for syntax diagrams, and the HOL theories for
  2308 examples.
  2309 
  2310 * Attibute 'code': 'code' now declares concrete and abstract code
  2311 equations uniformly.  Use explicit 'code equation' and 'code abstract'
  2312 to distinguish both when desired.
  2313 
  2314 * Discontinued theories Code_Integer and Efficient_Nat by a more
  2315 fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,
  2316 Code_Target_Nat and Code_Target_Numeral.  See the tutorial on code
  2317 generation for details.  INCOMPATIBILITY.
  2318 
  2319 * Numeric types are mapped by default to target language numerals:
  2320 natural (replaces former code_numeral) and integer (replaces former
  2321 code_int).  Conversions are available as integer_of_natural /
  2322 natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and
  2323 Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in
  2324 ML).  INCOMPATIBILITY.
  2325 
  2326 * Function package: For mutually recursive functions f and g, separate
  2327 cases rules f.cases and g.cases are generated instead of unusable
  2328 f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY,
  2329 in the case that the unusable rule was used nevertheless.
  2330 
  2331 * Function package: For each function f, new rules f.elims are
  2332 generated, which eliminate equalities of the form "f x = t".
  2333 
  2334 * New command 'fun_cases' derives ad-hoc elimination rules for
  2335 function equations as simplified instances of f.elims, analogous to
  2336 inductive_cases.  See ~~/src/HOL/ex/Fundefs.thy for some examples.
  2337 
  2338 * Lifting:
  2339   - parametrized correspondence relations are now supported:
  2340     + parametricity theorems for the raw term can be specified in
  2341       the command lift_definition, which allow us to generate stronger
  2342       transfer rules
  2343     + setup_lifting generates stronger transfer rules if parametric
  2344       correspondence relation can be generated
  2345     + various new properties of the relator must be specified to support
  2346       parametricity
  2347     + parametricity theorem for the Quotient relation can be specified
  2348   - setup_lifting generates domain rules for the Transfer package
  2349   - stronger reflexivity prover of respectfulness theorems for type
  2350     copies
  2351   - ===> and --> are now local. The symbols can be introduced
  2352     by interpreting the locale lifting_syntax (typically in an
  2353     anonymous context)
  2354   - Lifting/Transfer relevant parts of Library/Quotient_* are now in
  2355     Main. Potential INCOMPATIBILITY
  2356   - new commands for restoring and deleting Lifting/Transfer context:
  2357     lifting_forget, lifting_update
  2358   - the command print_quotmaps was renamed to print_quot_maps.
  2359     INCOMPATIBILITY
  2360 
  2361 * Transfer:
  2362   - better support for domains in Transfer: replace Domainp T
  2363     by the actual invariant in a transferred goal
  2364   - transfer rules can have as assumptions other transfer rules
  2365   - Experimental support for transferring from the raw level to the
  2366     abstract level: Transfer.transferred attribute
  2367   - Attribute version of the transfer method: untransferred attribute
  2368 
  2369 * Reification and reflection:
  2370   - Reification is now directly available in HOL-Main in structure
  2371     "Reification".
  2372   - Reflection now handles multiple lists with variables also.
  2373   - The whole reflection stack has been decomposed into conversions.
  2374 INCOMPATIBILITY.
  2375 
  2376 * Revised devices for recursive definitions over finite sets:
  2377   - Only one fundamental fold combinator on finite set remains:
  2378     Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b
  2379     This is now identity on infinite sets.
  2380   - Locales ("mini packages") for fundamental definitions with
  2381     Finite_Set.fold: folding, folding_idem.
  2382   - Locales comm_monoid_set, semilattice_order_set and
  2383     semilattice_neutr_order_set for big operators on sets.
  2384     See theory Big_Operators for canonical examples.
  2385     Note that foundational constants comm_monoid_set.F and
  2386     semilattice_set.F correspond to former combinators fold_image
  2387     and fold1 respectively.  These are now gone.  You may use
  2388     those foundational constants as substitutes, but it is
  2389     preferable to interpret the above locales accordingly.
  2390   - Dropped class ab_semigroup_idem_mult (special case of lattice,
  2391     no longer needed in connection with Finite_Set.fold etc.)
  2392   - Fact renames:
  2393       card.union_inter ~> card_Un_Int [symmetric]
  2394       card.union_disjoint ~> card_Un_disjoint
  2395 INCOMPATIBILITY.
  2396 
  2397 * Locale hierarchy for abstract orderings and (semi)lattices.
  2398 
  2399 * Complete_Partial_Order.admissible is defined outside the type class
  2400 ccpo, but with mandatory prefix ccpo. Admissibility theorems lose the
  2401 class predicate assumption or sort constraint when possible.
  2402 INCOMPATIBILITY.
  2403 
  2404 * Introduce type class "conditionally_complete_lattice": Like a
  2405 complete lattice but does not assume the existence of the top and
  2406 bottom elements.  Allows to generalize some lemmas about reals and
  2407 extended reals.  Removed SupInf and replaced it by the instantiation
  2408 of conditionally_complete_lattice for real. Renamed lemmas about
  2409 conditionally-complete lattice from Sup_... to cSup_... and from
  2410 Inf_...  to cInf_... to avoid hidding of similar complete lattice
  2411 lemmas.
  2412 
  2413 * Introduce type class linear_continuum as combination of
  2414 conditionally-complete lattices and inner dense linorders which have
  2415 more than one element.  INCOMPATIBILITY.
  2416 
  2417 * Introduced type classes order_top and order_bot. The old classes top
  2418 and bot only contain the syntax without assumptions.  INCOMPATIBILITY:
  2419 Rename bot -> order_bot, top -> order_top
  2420 
  2421 * Introduce type classes "no_top" and "no_bot" for orderings without
  2422 top and bottom elements.
  2423 
  2424 * Split dense_linorder into inner_dense_order and no_top, no_bot.
  2425 
  2426 * Complex_Main: Unify and move various concepts from
  2427 HOL-Multivariate_Analysis to HOL-Complex_Main.
  2428 
  2429  - Introduce type class (lin)order_topology and
  2430    linear_continuum_topology.  Allows to generalize theorems about
  2431    limits and order.  Instances are reals and extended reals.
  2432 
  2433  - continuous and continuos_on from Multivariate_Analysis:
  2434    "continuous" is the continuity of a function at a filter.  "isCont"
  2435    is now an abbrevitation: "isCont x f == continuous (at _) f".
  2436 
  2437    Generalized continuity lemmas from isCont to continuous on an
  2438    arbitrary filter.
  2439 
  2440  - compact from Multivariate_Analysis. Use Bolzano's lemma to prove
  2441    compactness of closed intervals on reals. Continuous functions
  2442    attain infimum and supremum on compact sets. The inverse of a
  2443    continuous function is continuous, when the function is continuous
  2444    on a compact set.
  2445 
  2446  - connected from Multivariate_Analysis. Use it to prove the
  2447    intermediate value theorem. Show connectedness of intervals on
  2448    linear_continuum_topology).
  2449 
  2450  - first_countable_topology from Multivariate_Analysis. Is used to
  2451    show equivalence of properties on the neighbourhood filter of x and
  2452    on all sequences converging to x.
  2453 
  2454  - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved
  2455    theorems from Library/FDERIV.thy to Deriv.thy and base the
  2456    definition of DERIV on FDERIV. Add variants of DERIV and FDERIV
  2457    which are restricted to sets, i.e. to represent derivatives from
  2458    left or right.
  2459 
  2460  - Removed the within-filter. It is replaced by the principal filter:
  2461 
  2462      F within X = inf F (principal X)
  2463 
  2464  - Introduce "at x within U" as a single constant, "at x" is now an
  2465    abbreviation for "at x within UNIV"
  2466 
  2467  - Introduce named theorem collections tendsto_intros,
  2468    continuous_intros, continuous_on_intros and FDERIV_intros. Theorems
  2469    in tendsto_intros (or FDERIV_intros) are also available as
  2470    tendsto_eq_intros (or FDERIV_eq_intros) where the right-hand side
  2471    is replaced by a congruence rule. This allows to apply them as
  2472    intro rules and then proving equivalence by the simplifier.
  2473 
  2474  - Restructured theories in HOL-Complex_Main:
  2475 
  2476    + Moved RealDef and RComplete into Real
  2477 
  2478    + Introduced Topological_Spaces and moved theorems about
  2479      topological spaces, filters, limits and continuity to it
  2480 
  2481    + Renamed RealVector to Real_Vector_Spaces
  2482 
  2483    + Split Lim, SEQ, Series into Topological_Spaces,
  2484      Real_Vector_Spaces, and Limits
  2485 
  2486    + Moved Ln and Log to Transcendental
  2487 
  2488    + Moved theorems about continuity from Deriv to Topological_Spaces
  2489 
  2490  - Remove various auxiliary lemmas.
  2491 
  2492 INCOMPATIBILITY.
  2493 
  2494 * Nitpick:
  2495   - Added option "spy".
  2496   - Reduce incidence of "too high arity" errors.
  2497 
  2498 * Sledgehammer:
  2499   - Renamed option:
  2500       isar_shrink ~> isar_compress
  2501     INCOMPATIBILITY.
  2502   - Added options "isar_try0", "spy".
  2503   - Better support for "isar_proofs".
  2504   - MaSh has been fined-tuned and now runs as a local server.
  2505 
  2506 * Improved support for ad hoc overloading of constants (see also
  2507 isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).
  2508 
  2509 * Library/Polynomial.thy:
  2510   - Use lifting for primitive definitions.
  2511   - Explicit conversions from and to lists of coefficients, used for
  2512     generated code.
  2513   - Replaced recursion operator poly_rec by fold_coeffs.
  2514   - Prefer pre-existing gcd operation for gcd.
  2515   - Fact renames:
  2516     poly_eq_iff ~> poly_eq_poly_eq_iff
  2517     poly_ext ~> poly_eqI
  2518     expand_poly_eq ~> poly_eq_iff
  2519 IMCOMPATIBILITY.
  2520 
  2521 * New Library/Simps_Case_Conv.thy: Provides commands simps_of_case and
  2522 case_of_simps to convert function definitions between a list of
  2523 equations with patterns on the lhs and a single equation with case
  2524 expressions on the rhs. See also Ex/Simps_Case_Conv_Examples.thy.
  2525 
  2526 * New Library/FSet.thy: type of finite sets defined as a subtype of
  2527 sets defined by Lifting/Transfer.
  2528 
  2529 * Discontinued theory src/HOL/Library/Eval_Witness.  INCOMPATIBILITY.
  2530 
  2531 * Consolidation of library theories on product orders:
  2532 
  2533     Product_Lattice ~> Product_Order -- pointwise order on products
  2534     Product_ord ~> Product_Lexorder -- lexicographic order on products
  2535 
  2536 INCOMPATIBILITY.
  2537 
  2538 * Imperative-HOL: The MREC combinator is considered legacy and no
  2539 longer included by default. INCOMPATIBILITY, use partial_function
  2540 instead, or import theory Legacy_Mrec as a fallback.
  2541 
  2542 * HOL-Algebra: Discontinued theories ~~/src/HOL/Algebra/abstract and
  2543 ~~/src/HOL/Algebra/poly.  Existing theories should be based on
  2544 ~~/src/HOL/Library/Polynomial instead.  The latter provides
  2545 integration with HOL's type classes for rings.  INCOMPATIBILITY.
  2546 
  2547 * HOL-BNF:
  2548   - Various improvements to BNF-based (co)datatype package, including
  2549     new commands "primrec_new", "primcorec", and
  2550     "datatype_new_compat", as well as documentation. See
  2551     "datatypes.pdf" for details.
  2552   - New "coinduction" method to avoid some boilerplate (compared to
  2553     coinduct).
  2554   - Renamed keywords:
  2555     data ~> datatype_new
  2556     codata ~> codatatype
  2557     bnf_def ~> bnf
  2558   - Renamed many generated theorems, including
  2559     discs ~> disc
  2560     map_comp' ~> map_comp
  2561     map_id' ~> map_id
  2562     sels ~> sel
  2563     set_map' ~> set_map
  2564     sets ~> set
  2565 IMCOMPATIBILITY.
  2566 
  2567 
  2568 *** ML ***
  2569 
  2570 * Spec_Check is a Quickcheck tool for Isabelle/ML.  The ML function
  2571 "check_property" allows to check specifications of the form "ALL x y
  2572 z. prop x y z".  See also ~~/src/Tools/Spec_Check/ with its
  2573 Examples.thy in particular.
  2574 
  2575 * Improved printing of exception trace in Poly/ML 5.5.1, with regular
  2576 tracing output in the command transaction context instead of physical
  2577 stdout.  See also Toplevel.debug, Toplevel.debugging and
  2578 ML_Compiler.exn_trace.
  2579 
  2580 * ML type "theory" is now immutable, without any special treatment of
  2581 drafts or linear updates (which could lead to "stale theory" errors in
  2582 the past).  Discontinued obsolete operations like Theory.copy,
  2583 Theory.checkpoint, and the auxiliary type theory_ref.  Minor
  2584 INCOMPATIBILITY.
  2585 
  2586 * More uniform naming of goal functions for skipped proofs:
  2587 
  2588     Skip_Proof.prove  ~>  Goal.prove_sorry
  2589     Skip_Proof.prove_global  ~>  Goal.prove_sorry_global
  2590 
  2591 Minor INCOMPATIBILITY.
  2592 
  2593 * Simplifier tactics and tools use proper Proof.context instead of
  2594 historic type simpset.  Old-style declarations like addsimps,
  2595 addsimprocs etc. operate directly on Proof.context.  Raw type simpset
  2596 retains its use as snapshot of the main Simplifier context, using
  2597 simpset_of and put_simpset on Proof.context.  INCOMPATIBILITY -- port
  2598 old tools by making them depend on (ctxt : Proof.context) instead of
  2599 (ss : simpset), then turn (simpset_of ctxt) into ctxt.
  2600 
  2601 * Modifiers for classical wrappers (e.g. addWrapper, delWrapper)
  2602 operate on Proof.context instead of claset, for uniformity with addIs,
  2603 addEs, addDs etc. Note that claset_of and put_claset allow to manage
  2604 clasets separately from the context.
  2605 
  2606 * Discontinued obsolete ML antiquotations @{claset} and @{simpset}.
  2607 INCOMPATIBILITY, use @{context} instead.
  2608 
  2609 * Antiquotation @{theory_context A} is similar to @{theory A}, but
  2610 presents the result as initial Proof.context.
  2611 
  2612 
  2613 *** System ***
  2614 
  2615 * Discontinued obsolete isabelle usedir, mkdir, make -- superseded by
  2616 "isabelle build" in Isabelle2013.  INCOMPATIBILITY.
  2617 
  2618 * Discontinued obsolete isabelle-process options -f and -u (former
  2619 administrative aliases of option -e).  Minor INCOMPATIBILITY.
  2620 
  2621 * Discontinued obsolete isabelle print tool, and PRINT_COMMAND
  2622 settings variable.
  2623 
  2624 * Discontinued ISABELLE_DOC_FORMAT settings variable and historic
  2625 document formats: dvi.gz, ps, ps.gz -- the default document format is
  2626 always pdf.
  2627 
  2628 * Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to
  2629 specify global resources of the JVM process run by isabelle build.
  2630 
  2631 * Toplevel executable $ISABELLE_HOME/bin/isabelle_scala_script allows
  2632 to run Isabelle/Scala source files as standalone programs.
  2633 
  2634 * Improved "isabelle keywords" tool (for old-style ProofGeneral
  2635 keyword tables): use Isabelle/Scala operations, which inspect outer
  2636 syntax without requiring to build sessions first.
  2637 
  2638 * Sessions may be organized via 'chapter' specifications in the ROOT
  2639 file, which determines a two-level hierarchy of browser info.  The old
  2640 tree-like organization via implicit sub-session relation (with its
  2641 tendency towards erratic fluctuation of URLs) has been discontinued.
  2642 The default chapter is called "Unsorted".  Potential INCOMPATIBILITY
  2643 for HTML presentation of theories.
  2644 
  2645 
  2646 
  2647 New in Isabelle2013 (February 2013)
  2648 -----------------------------------
  2649 
  2650 *** General ***
  2651 
  2652 * Theorem status about oracles and unfinished/failed future proofs is
  2653 no longer printed by default, since it is incompatible with
  2654 incremental / parallel checking of the persistent document model.  ML
  2655 function Thm.peek_status may be used to inspect a snapshot of the
  2656 ongoing evaluation process.  Note that in batch mode --- notably
  2657 isabelle build --- the system ensures that future proofs of all
  2658 accessible theorems in the theory context are finished (as before).
  2659 
  2660 * Configuration option show_markup controls direct inlining of markup
  2661 into the printed representation of formal entities --- notably type
  2662 and sort constraints.  This enables Prover IDE users to retrieve that
  2663 information via tooltips in the output window, for example.
  2664 
  2665 * Command 'ML_file' evaluates ML text from a file directly within the
  2666 theory, without any predeclaration via 'uses' in the theory header.
  2667 
  2668 * Old command 'use' command and corresponding keyword 'uses' in the
  2669 theory header are legacy features and will be discontinued soon.
  2670 Tools that load their additional source files may imitate the
  2671 'ML_file' implementation, such that the system can take care of
  2672 dependencies properly.
  2673 
  2674 * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which
  2675 is called fastforce / fast_force_tac already since Isabelle2011-1.
  2676 
  2677 * Updated and extended "isar-ref" and "implementation" manual, reduced
  2678 remaining material in old "ref" manual.
  2679 
  2680 * Improved support for auxiliary contexts that indicate block structure
  2681 for specifications.  Nesting of "context fixes ... context assumes ..."
  2682 and "class ... context ...".
  2683 
  2684 * Attribute "consumes" allows a negative value as well, which is
  2685 interpreted relatively to the total number of premises of the rule in
  2686 the target context.  This form of declaration is stable when exported
  2687 from a nested 'context' with additional assumptions.  It is the
  2688 preferred form for definitional packages, notably cases/rules produced
  2689 in HOL/inductive and HOL/function.
  2690 
  2691 * More informative error messages for Isar proof commands involving
  2692 lazy enumerations (method applications etc.).
  2693 
  2694 * Refined 'help' command to retrieve outer syntax commands according
  2695 to name patterns (with clickable results).
  2696 
  2697 
  2698 *** Prover IDE -- Isabelle/Scala/jEdit ***
  2699 
  2700 * Parallel terminal proofs ('by') are enabled by default, likewise
  2701 proofs that are built into packages like 'datatype', 'function'.  This
  2702 allows to "run ahead" checking the theory specifications on the
  2703 surface, while the prover is still crunching on internal
  2704 justifications.  Unfinished / cancelled proofs are restarted as
  2705 required to complete full proof checking eventually.
  2706 
  2707 * Improved output panel with tooltips, hyperlinks etc. based on the
  2708 same Rich_Text_Area as regular Isabelle/jEdit buffers.  Activation of
  2709 tooltips leads to some window that supports the same recursively,
  2710 which can lead to stacks of tooltips as the semantic document content
  2711 is explored.  ESCAPE closes the whole stack, individual windows may be
  2712 closed separately, or detached to become independent jEdit dockables.
  2713 
  2714 * Improved support for commands that produce graph output: the text
  2715 message contains a clickable area to open a new instance of the graph
  2716 browser on demand.
  2717 
  2718 * More robust incremental parsing of outer syntax (partial comments,
  2719 malformed symbols).  Changing the balance of open/close quotes and
  2720 comment delimiters works more conveniently with unfinished situations
  2721 that frequently occur in user interaction.
  2722 
  2723 * More efficient painting and improved reactivity when editing large
  2724 files.  More scalable management of formal document content.
  2725 
  2726 * Smarter handling of tracing messages: prover process pauses after
  2727 certain number of messages per command transaction, with some user
  2728 dialog to stop or continue.  This avoids swamping the front-end with
  2729 potentially infinite message streams.
  2730 
  2731 * More plugin options and preferences, based on Isabelle/Scala.  The
  2732 jEdit plugin option panel provides access to some Isabelle/Scala
  2733 options, including tuning parameters for editor reactivity and color
  2734 schemes.
  2735 
  2736 * Dockable window "Symbols" provides some editing support for Isabelle
  2737 symbols.
  2738 
  2739 * Dockable window "Monitor" shows ML runtime statistics.  Note that
  2740 continuous display of the chart slows down the system.
  2741 
  2742 * Improved editing support for control styles: subscript, superscript,
  2743 bold, reset of style -- operating on single symbols or text
  2744 selections.  Cf. keyboard shortcuts C+e DOWN/UP/RIGHT/LEFT.
  2745 
  2746 * Actions isabelle.increase-font-size and isabelle.decrease-font-size
  2747 adjust the main text area font size, and its derivatives for output,
  2748 tooltips etc.  Cf. keyboard shortcuts C-PLUS and C-MINUS, which often
  2749 need to be adapted to local keyboard layouts.
  2750 
  2751 * More reactive completion popup by default: use \t (TAB) instead of
  2752 \n (NEWLINE) to minimize intrusion into regular flow of editing.  See
  2753 also "Plugin Options / SideKick / General / Code Completion Options".
  2754 
  2755 * Implicit check and build dialog of the specified logic session
  2756 image.  For example, HOL, HOLCF, HOL-Nominal can be produced on
  2757 demand, without bundling big platform-dependent heap images in the
  2758 Isabelle distribution.
  2759 
  2760 * Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates
  2761 from Oracle provide better multi-platform experience.  This version is
  2762 now bundled exclusively with Isabelle.
  2763 
  2764 
  2765 *** Pure ***
  2766 
  2767 * Code generation for Haskell: restrict unqualified imports from
  2768 Haskell Prelude to a small set of fundamental operations.
  2769 
  2770 * Command 'export_code': relative file names are interpreted
  2771 relatively to master directory of current theory rather than the
  2772 rather arbitrary current working directory.  INCOMPATIBILITY.
  2773 
  2774 * Discontinued obsolete attribute "COMP".  Potential INCOMPATIBILITY,
  2775 use regular rule composition via "OF" / "THEN", or explicit proof
  2776 structure instead.  Note that Isabelle/ML provides a variety of
  2777 operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
  2778 with some care where this is really required.
  2779 
  2780 * Command 'typ' supports an additional variant with explicit sort
  2781 constraint, to infer and check the most general type conforming to a
  2782 given sort.  Example (in HOL):
  2783 
  2784   typ "_ * _ * bool * unit" :: finite
  2785 
  2786 * Command 'locale_deps' visualizes all locales and their relations as
  2787 a Hasse diagram.
  2788 
  2789 
  2790 *** HOL ***
  2791 
  2792 * Sledgehammer:
  2793 
  2794   - Added MaSh relevance filter based on machine-learning; see the
  2795     Sledgehammer manual for details.
  2796   - Polished Isar proofs generated with "isar_proofs" option.
  2797   - Rationalized type encodings ("type_enc" option).
  2798   - Renamed "kill_provers" subcommand to "kill_all".
  2799   - Renamed options:
  2800       isar_proof ~> isar_proofs
  2801       isar_shrink_factor ~> isar_shrink
  2802       max_relevant ~> max_facts
  2803       relevance_thresholds ~> fact_thresholds
  2804 
  2805 * Quickcheck: added an optimisation for equality premises.  It is
  2806 switched on by default, and can be switched off by setting the
  2807 configuration quickcheck_optimise_equality to false.
  2808 
  2809 * Quotient: only one quotient can be defined by quotient_type
  2810 INCOMPATIBILITY.
  2811 
  2812 * Lifting:
  2813   - generation of an abstraction function equation in lift_definition
  2814   - quot_del attribute
  2815   - renamed no_abs_code -> no_code (INCOMPATIBILITY.)
  2816 
  2817 * Simproc "finite_Collect" rewrites set comprehensions into pointfree
  2818 expressions.
  2819 
  2820 * Preprocessing of the code generator rewrites set comprehensions into
  2821 pointfree expressions.
  2822 
  2823 * The SMT solver Z3 has now by default a restricted set of directly
  2824 supported features. For the full set of features (div/mod, nonlinear
  2825 arithmetic, datatypes/records) with potential proof reconstruction
  2826 failures, enable the configuration option "z3_with_extensions".  Minor
  2827 INCOMPATIBILITY.
  2828 
  2829 * Simplified 'typedef' specifications: historical options for implicit
  2830 set definition and alternative name have been discontinued.  The
  2831 former behavior of "typedef (open) t = A" is now the default, but
  2832 written just "typedef t = A".  INCOMPATIBILITY, need to adapt theories
  2833 accordingly.
  2834 
  2835 * Removed constant "chars"; prefer "Enum.enum" on type "char"
  2836 directly.  INCOMPATIBILITY.
  2837 
  2838 * Moved operation product, sublists and n_lists from theory Enum to
  2839 List.  INCOMPATIBILITY.
  2840 
  2841 * Theorem UN_o generalized to SUP_comp.  INCOMPATIBILITY.
  2842 
  2843 * Class "comm_monoid_diff" formalises properties of bounded
  2844 subtraction, with natural numbers and multisets as typical instances.
  2845 
  2846 * Added combinator "Option.these" with type "'a option set => 'a set".
  2847 
  2848 * Theory "Transitive_Closure": renamed lemmas
  2849 
  2850   reflcl_tranclp -> reflclp_tranclp
  2851   rtranclp_reflcl -> rtranclp_reflclp
  2852 
  2853 INCOMPATIBILITY.
  2854 
  2855 * Theory "Rings": renamed lemmas (in class semiring)
  2856 
  2857   left_distrib ~> distrib_right
  2858   right_distrib ~> distrib_left
  2859 
  2860 INCOMPATIBILITY.
  2861 
  2862 * Generalized the definition of limits:
  2863 
  2864   - Introduced the predicate filterlim (LIM x F. f x :> G) which
  2865     expresses that when the input values x converge to F then the
  2866     output f x converges to G.
  2867 
  2868   - Added filters for convergence to positive (at_top) and negative
  2869     infinity (at_bot).
  2870 
  2871   - Moved infinity in the norm (at_infinity) from
  2872     Multivariate_Analysis to Complex_Main.
  2873 
  2874   - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :>
  2875     at_top".
  2876 
  2877 INCOMPATIBILITY.
  2878 
  2879 * Theory "Library/Option_ord" provides instantiation of option type to
  2880 lattice type classes.
  2881 
  2882 * Theory "Library/Multiset": renamed
  2883 
  2884     constant fold_mset ~> Multiset.fold
  2885     fact fold_mset_commute ~> fold_mset_comm
  2886 
  2887 INCOMPATIBILITY.
  2888 
  2889 * Renamed theory Library/List_Prefix to Library/Sublist, with related
  2890 changes as follows.
  2891 
  2892   - Renamed constants (and related lemmas)
  2893 
  2894       prefix ~> prefixeq
  2895       strict_prefix ~> prefix
  2896 
  2897   - Replaced constant "postfix" by "suffixeq" with swapped argument
  2898     order (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped
  2899     old infix syntax "xs >>= ys"; use "suffixeq ys xs" instead.
  2900     Renamed lemmas accordingly.
  2901 
  2902   - Added constant "list_hembeq" for homeomorphic embedding on
  2903     lists. Added abbreviation "sublisteq" for special case
  2904     "list_hembeq (op =)".
  2905 
  2906   - Theory Library/Sublist no longer provides "order" and "bot" type
  2907     class instances for the prefix order (merely corresponding locale
  2908     interpretations). The type class instances are now in theory
  2909     Library/Prefix_Order.
  2910 
  2911   - The sublist relation of theory Library/Sublist_Order is now based
  2912     on "Sublist.sublisteq".  Renamed lemmas accordingly:
  2913 
  2914       le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff
  2915       le_list_append_mono ~> Sublist.list_hembeq_append_mono
  2916       le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2
  2917       le_list_Cons_EX ~> Sublist.list_hembeq_ConsD
  2918       le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2'
  2919       le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq
  2920       le_list_drop_Cons ~> Sublist.sublisteq_Cons'
  2921       le_list_drop_many ~> Sublist.sublisteq_drop_many
  2922       le_list_filter_left ~> Sublist.sublisteq_filter_left
  2923       le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many
  2924       le_list_rev_take_iff ~> Sublist.sublisteq_append
  2925       le_list_same_length ~> Sublist.sublisteq_same_length
  2926       le_list_take_many_iff ~> Sublist.sublisteq_append'
  2927       less_eq_list.drop ~> less_eq_list_drop
  2928       less_eq_list.induct ~> less_eq_list_induct
  2929       not_le_list_length ~> Sublist.not_sublisteq_length
  2930 
  2931 INCOMPATIBILITY.
  2932 
  2933 * New theory Library/Countable_Set.
  2934 
  2935 * Theory Library/Debug and Library/Parallel provide debugging and
  2936 parallel execution for code generated towards Isabelle/ML.
  2937 
  2938 * Theory Library/FuncSet: Extended support for Pi and extensional and
  2939 introduce the extensional dependent function space "PiE". Replaced
  2940 extensional_funcset by an abbreviation, and renamed lemmas from
  2941 extensional_funcset to PiE as follows:
  2942 
  2943   extensional_empty  ~>  PiE_empty
  2944   extensional_funcset_empty_domain  ~>  PiE_empty_domain
  2945   extensional_funcset_empty_range  ~>  PiE_empty_range
  2946   extensional_funcset_arb  ~>  PiE_arb
  2947   extensional_funcset_mem  ~>  PiE_mem
  2948   extensional_funcset_extend_domainI  ~>  PiE_fun_upd
  2949   extensional_funcset_restrict_domain  ~>  fun_upd_in_PiE
  2950   extensional_funcset_extend_domain_eq  ~>  PiE_insert_eq
  2951   card_extensional_funcset  ~>  card_PiE
  2952   finite_extensional_funcset  ~>  finite_PiE
  2953 
  2954 INCOMPATIBILITY.
  2955 
  2956 * Theory Library/FinFun: theory of almost everywhere constant
  2957 functions (supersedes the AFP entry "Code Generation for Functions as
  2958 Data").
  2959 
  2960 * Theory Library/Phantom: generic phantom type to make a type
  2961 parameter appear in a constant's type.  This alternative to adding
  2962 TYPE('a) as another parameter avoids unnecessary closures in generated
  2963 code.
  2964 
  2965 * Theory Library/RBT_Impl: efficient construction of red-black trees
  2966 from sorted associative lists. Merging two trees with rbt_union may
  2967 return a structurally different tree than before.  Potential
  2968 INCOMPATIBILITY.
  2969 
  2970 * Theory Library/IArray: immutable arrays with code generation.
  2971 
  2972 * Theory Library/Finite_Lattice: theory of finite lattices.
  2973 
  2974 * HOL/Multivariate_Analysis: replaced
  2975 
  2976   "basis :: 'a::euclidean_space => nat => real"
  2977   "\<Chi>\<Chi> :: (nat => real) => 'a::euclidean_space"
  2978 
  2979 on euclidean spaces by using the inner product "_ \<bullet> _" with
  2980 vectors from the Basis set: "\<Chi>\<Chi> i. f i" is superseded by
  2981 "SUM i : Basis. f i * r i".
  2982 
  2983   With this change the following constants are also changed or removed:
  2984 
  2985     DIM('a) :: nat  ~>  card (Basis :: 'a set)   (is an abbreviation)
  2986     a $$ i  ~>  inner a i  (where i : Basis)
  2987     cart_base i  removed
  2988     \<pi>, \<pi>'  removed
  2989 
  2990   Theorems about these constants where removed.
  2991 
  2992   Renamed lemmas:
  2993 
  2994     component_le_norm  ~>  Basis_le_norm
  2995     euclidean_eq  ~>  euclidean_eq_iff
  2996     differential_zero_maxmin_component  ~>  differential_zero_maxmin_cart
  2997     euclidean_simps  ~>  inner_simps
  2998     independent_basis  ~>  independent_Basis
  2999     span_basis  ~>  span_Basis
  3000     in_span_basis  ~>  in_span_Basis
  3001     norm_bound_component_le  ~>  norm_boound_Basis_le
  3002     norm_bound_component_lt  ~>  norm_boound_Basis_lt
  3003     component_le_infnorm  ~>  Basis_le_infnorm
  3004 
  3005 INCOMPATIBILITY.
  3006 
  3007 * HOL/Probability:
  3008 
  3009   - Added simproc "measurable" to automatically prove measurability.
  3010 
  3011   - Added induction rules for sigma sets with disjoint union
  3012     (sigma_sets_induct_disjoint) and for Borel-measurable functions
  3013     (borel_measurable_induct).
  3014 
  3015   - Added the Daniell-Kolmogorov theorem (the existence the limit of a
  3016     projective family).
  3017 
  3018 * HOL/Cardinals: Theories of ordinals and cardinals (supersedes the
  3019 AFP entry "Ordinals_and_Cardinals").
  3020 
  3021 * HOL/BNF: New (co)datatype package based on bounded natural functors
  3022 with support for mixed, nested recursion and interesting non-free
  3023 datatypes.
  3024 
  3025 * HOL/Finite_Set and Relation: added new set and relation operations
  3026 expressed by Finite_Set.fold.
  3027 
  3028 * New theory HOL/Library/RBT_Set: implementation of sets by red-black
  3029 trees for the code generator.
  3030 
  3031 * HOL/Library/RBT and HOL/Library/Mapping have been converted to
  3032 Lifting/Transfer.
  3033 possible INCOMPATIBILITY.
  3034 
  3035 * HOL/Set: renamed Set.project -> Set.filter
  3036 INCOMPATIBILITY.
  3037 
  3038 
  3039 *** Document preparation ***
  3040 
  3041 * Dropped legacy antiquotations "term_style" and "thm_style", since
  3042 styles may be given as arguments to "term" and "thm" already.
  3043 Discontinued legacy styles "prem1" .. "prem19".
  3044 
  3045 * Default LaTeX rendering for \<euro> is now based on eurosym package,
  3046 instead of slightly exotic babel/greek.
  3047 
  3048 * Document variant NAME may use different LaTeX entry point
  3049 document/root_NAME.tex if that file exists, instead of the common
  3050 document/root.tex.
  3051 
  3052 * Simplified custom document/build script, instead of old-style
  3053 document/IsaMakefile.  Minor INCOMPATIBILITY.
  3054 
  3055 
  3056 *** ML ***
  3057 
  3058 * The default limit for maximum number of worker threads is now 8,
  3059 instead of 4, in correspondence to capabilities of contemporary
  3060 hardware and Poly/ML runtime system.
  3061 
  3062 * Type Seq.results and related operations support embedded error
  3063 messages within lazy enumerations, and thus allow to provide
  3064 informative errors in the absence of any usable results.
  3065 
  3066 * Renamed Position.str_of to Position.here to emphasize that this is a
  3067 formal device to inline positions into message text, but not
  3068 necessarily printing visible text.
  3069 
  3070 
  3071 *** System ***
  3072 
  3073 * Advanced support for Isabelle sessions and build management, see
  3074 "system" manual for the chapter of that name, especially the "isabelle
  3075 build" tool and its examples.  The "isabelle mkroot" tool prepares
  3076 session root directories for use with "isabelle build", similar to
  3077 former "isabelle mkdir" for "isabelle usedir".  Note that this affects
  3078 document preparation as well.  INCOMPATIBILITY, isabelle usedir /
  3079 mkdir / make are rendered obsolete.
  3080 
  3081 * Discontinued obsolete Isabelle/build script, it is superseded by the
  3082 regular isabelle build tool.  For example:
  3083 
  3084   isabelle build -s -b HOL
  3085 
  3086 * Discontinued obsolete "isabelle makeall".
  3087 
  3088 * Discontinued obsolete IsaMakefile and ROOT.ML files from the
  3089 Isabelle distribution, except for rudimentary src/HOL/IsaMakefile that
  3090 provides some traditional targets that invoke "isabelle build".  Note
  3091 that this is inefficient!  Applications of Isabelle/HOL involving
  3092 "isabelle make" should be upgraded to use "isabelle build" directly.
  3093 
  3094 * The "isabelle options" tool prints Isabelle system options, as
  3095 required for "isabelle build", for example.
  3096 
  3097 * The "isabelle logo" tool produces EPS and PDF format simultaneously.
  3098 Minor INCOMPATIBILITY in command-line options.
  3099 
  3100 * The "isabelle install" tool has now a simpler command-line.  Minor
  3101 INCOMPATIBILITY.
  3102 
  3103 * The "isabelle components" tool helps to resolve add-on components
  3104 that are not bundled, or referenced from a bare-bones repository
  3105 version of Isabelle.
  3106 
  3107 * Settings variable ISABELLE_PLATFORM_FAMILY refers to the general
  3108 platform family: "linux", "macos", "windows".
  3109 
  3110 * The ML system is configured as regular component, and no longer
  3111 picked up from some surrounding directory.  Potential INCOMPATIBILITY
  3112 for home-made settings.
  3113 
  3114 * Improved ML runtime statistics (heap, threads, future tasks etc.).
  3115 
  3116 * Discontinued support for Poly/ML 5.2.1, which was the last version
  3117 without exception positions and advanced ML compiler/toplevel
  3118 configuration.
  3119 
  3120 * Discontinued special treatment of Proof General -- no longer guess
  3121 PROOFGENERAL_HOME based on accidental file-system layout.  Minor
  3122 INCOMPATIBILITY: provide PROOFGENERAL_HOME and PROOFGENERAL_OPTIONS
  3123 settings manually, or use a Proof General version that has been
  3124 bundled as Isabelle component.
  3125 
  3126 
  3127 
  3128 New in Isabelle2012 (May 2012)
  3129 ------------------------------
  3130 
  3131 *** General ***
  3132 
  3133 * Prover IDE (PIDE) improvements:
  3134 
  3135   - more robust Sledgehammer integration (as before the sledgehammer
  3136     command-line needs to be typed into the source buffer)
  3137   - markup for bound variables
  3138   - markup for types of term variables (displayed as tooltips)
  3139   - support for user-defined Isar commands within the running session
  3140   - improved support for Unicode outside original 16bit range
  3141     e.g. glyph for \<A> (thanks to jEdit 4.5.1)
  3142 
  3143 * Forward declaration of outer syntax keywords within the theory
  3144 header -- minor INCOMPATIBILITY for user-defined commands.  Allow new
  3145 commands to be used in the same theory where defined.
  3146 
  3147 * Auxiliary contexts indicate block structure for specifications with
  3148 additional parameters and assumptions.  Such unnamed contexts may be
  3149 nested within other targets, like 'theory', 'locale', 'class',
  3150 'instantiation' etc.  Results from the local context are generalized
  3151 accordingly and applied to the enclosing target context.  Example:
  3152 
  3153   context
  3154     fixes x y z :: 'a
  3155     assumes xy: "x = y" and yz: "y = z"
  3156   begin
  3157 
  3158   lemma my_trans: "x = z" using xy yz by simp
  3159 
  3160   end
  3161 
  3162   thm my_trans
  3163 
  3164 The most basic application is to factor-out context elements of
  3165 several fixes/assumes/shows theorem statements, e.g. see
  3166 ~~/src/HOL/Isar_Examples/Group_Context.thy
  3167 
  3168 Any other local theory specification element works within the "context
  3169 ... begin ... end" block as well.
  3170 
  3171 * Bundled declarations associate attributed fact expressions with a
  3172 given name in the context.  These may be later included in other
  3173 contexts.  This allows to manage context extensions casually, without
  3174 the logical dependencies of locales and locale interpretation.  See
  3175 commands 'bundle', 'include', 'including' etc. in the isar-ref manual.
  3176 
  3177 * Commands 'lemmas' and 'theorems' allow local variables using 'for'
  3178 declaration, and results are standardized before being stored.  Thus
  3179 old-style "standard" after instantiation or composition of facts
  3180 becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of
  3181 indices of schematic variables.
  3182 
  3183 * Rule attributes in local theory declarations (e.g. locale or class)
  3184 are now statically evaluated: the resulting theorem is stored instead
  3185 of the original expression.  INCOMPATIBILITY in rare situations, where
  3186 the historic accident of dynamic re-evaluation in interpretations
  3187 etc. was exploited.
  3188 
  3189 * New tutorial "Programming and Proving in Isabelle/HOL"
  3190 ("prog-prove").  It completely supersedes "A Tutorial Introduction to
  3191 Structured Isar Proofs" ("isar-overview"), which has been removed.  It
  3192 also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order
  3193 Logic" as the recommended beginners tutorial, but does not cover all
  3194 of the material of that old tutorial.
  3195 
  3196 * Updated and extended reference manuals: "isar-ref",
  3197 "implementation", "system"; reduced remaining material in old "ref"
  3198 manual.
  3199 
  3200 
  3201 *** Pure ***
  3202 
  3203 * Command 'definition' no longer exports the foundational "raw_def"
  3204 into the user context.  Minor INCOMPATIBILITY, may use the regular
  3205 "def" result with attribute "abs_def" to imitate the old version.
  3206 
  3207 * Attribute "abs_def" turns an equation of the form "f x y == t" into
  3208 "f == %x y. t", which ensures that "simp" or "unfold" steps always
  3209 expand it.  This also works for object-logic equality.  (Formerly
  3210 undocumented feature.)
  3211 
  3212 * Sort constraints are now propagated in simultaneous statements, just
  3213 like type constraints.  INCOMPATIBILITY in rare situations, where
  3214 distinct sorts used to be assigned accidentally.  For example:
  3215 
  3216   lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"
  3217 
  3218   lemma "P (x::'a)" and "Q (y::'a::bar)"
  3219     -- "now uniform 'a::bar instead of default sort for first occurrence (!)"
  3220 
  3221 * Rule composition via attribute "OF" (or ML functions OF/MRS) is more
  3222 tolerant against multiple unifiers, as long as the final result is
  3223 unique.  (As before, rules are composed in canonical right-to-left
  3224 order to accommodate newly introduced premises.)
  3225 
  3226 * Renamed some inner syntax categories:
  3227 
  3228     num ~> num_token
  3229     xnum ~> xnum_token
  3230     xstr ~> str_token
  3231 
  3232 Minor INCOMPATIBILITY.  Note that in practice "num_const" or
  3233 "num_position" etc. are mainly used instead (which also include
  3234 position information via constraints).
  3235 
  3236 * Simplified configuration options for syntax ambiguity: see
  3237 "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
  3238 manual.  Minor INCOMPATIBILITY.
  3239 
  3240 * Discontinued configuration option "syntax_positions": atomic terms
  3241 in parse trees are always annotated by position constraints.
  3242 
  3243 * Old code generator for SML and its commands 'code_module',
  3244 'code_library', 'consts_code', 'types_code' have been discontinued.
  3245 Use commands of the generic code generator instead.  INCOMPATIBILITY.
  3246 
  3247 * Redundant attribute "code_inline" has been discontinued. Use
  3248 "code_unfold" instead.  INCOMPATIBILITY.
  3249 
  3250 * Dropped attribute "code_unfold_post" in favor of the its dual
  3251 "code_abbrev", which yields a common pattern in definitions like
  3252 
  3253   definition [code_abbrev]: "f = t"
  3254 
  3255 INCOMPATIBILITY.
  3256 
  3257 * Obsolete 'types' command has been discontinued.  Use 'type_synonym'
  3258 instead.  INCOMPATIBILITY.
  3259 
  3260 * Discontinued old "prems" fact, which used to refer to the accidental
  3261 collection of foundational premises in the context (already marked as
  3262 legacy since Isabelle2011).
  3263 
  3264 
  3265 *** HOL ***
  3266 
  3267 * Type 'a set is now a proper type constructor (just as before
  3268 Isabelle2008).  Definitions mem_def and Collect_def have disappeared.
  3269 Non-trivial INCOMPATIBILITY.  For developments keeping predicates and
  3270 sets separate, it is often sufficient to rephrase some set S that has
  3271 been accidentally used as predicates by "%x. x : S", and some
  3272 predicate P that has been accidentally used as set by "{x. P x}".
  3273 Corresponding proofs in a first step should be pruned from any
  3274 tinkering with former theorems mem_def and Collect_def as far as
  3275 possible.
  3276 
  3277 For developments which deliberately mix predicates and sets, a
  3278 planning step is necessary to determine what should become a predicate
  3279 and what a set.  It can be helpful to carry out that step in
  3280 Isabelle2011-1 before jumping right into the current release.
  3281 
  3282 * Code generation by default implements sets as container type rather
  3283 than predicates.  INCOMPATIBILITY.
  3284 
  3285 * New type synonym 'a rel = ('a * 'a) set
  3286 
  3287 * The representation of numerals has changed.  Datatype "num"
  3288 represents strictly positive binary numerals, along with functions
  3289 "numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent
  3290 positive and negated numeric literals, respectively.  See also
  3291 definitions in ~~/src/HOL/Num.thy.  Potential INCOMPATIBILITY, some
  3292 user theories may require adaptations as follows:
  3293 
  3294   - Theorems with number_ring or number_semiring constraints: These
  3295     classes are gone; use comm_ring_1 or comm_semiring_1 instead.
  3296 
  3297   - Theories defining numeric types: Remove number, number_semiring,
  3298     and number_ring instances. Defer all theorems about numerals until
  3299     after classes one and semigroup_add have been instantiated.
  3300 
  3301   - Numeral-only simp rules: Replace each rule having a "number_of v"
  3302     pattern with two copies, one for numeral and one for neg_numeral.
  3303 
  3304   - Theorems about subclasses of semiring_1 or ring_1: These classes
  3305     automatically support numerals now, so more simp rules and
  3306     simprocs may now apply within the proof.
  3307 
  3308   - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:
  3309     Redefine using other integer operations.
  3310 
  3311 * Transfer: New package intended to generalize the existing
  3312 "descending" method and related theorem attributes from the Quotient
  3313 package.  (Not all functionality is implemented yet, but future
  3314 development will focus on Transfer as an eventual replacement for the
  3315 corresponding parts of the Quotient package.)
  3316 
  3317   - transfer_rule attribute: Maintains a collection of transfer rules,
  3318     which relate constants at two different types. Transfer rules may
  3319     relate different type instances of the same polymorphic constant,
  3320     or they may relate an operation on a raw type to a corresponding
  3321     operation on an abstract type (quotient or subtype). For example:
  3322 
  3323     ((A ===> B) ===> list_all2 A ===> list_all2 B) map map
  3324     (cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int
  3325 
  3326   - transfer method: Replaces a subgoal on abstract types with an
  3327     equivalent subgoal on the corresponding raw types. Constants are
  3328     replaced with corresponding ones according to the transfer rules.
  3329     Goals are generalized over all free variables by default; this is
  3330     necessary for variables whose types change, but can be overridden
  3331     for specific variables with e.g. "transfer fixing: x y z".  The
  3332     variant transfer' method allows replacing a subgoal with one that
  3333     is logically stronger (rather than equivalent).
  3334 
  3335   - relator_eq attribute: Collects identity laws for relators of
  3336     various type constructors, e.g. "list_all2 (op =) = (op =)".  The
  3337     transfer method uses these lemmas to infer transfer rules for
  3338     non-polymorphic constants on the fly.
  3339 
  3340   - transfer_prover method: Assists with proving a transfer rule for a
  3341     new constant, provided the constant is defined in terms of other
  3342     constants that already have transfer rules. It should be applied
  3343     after unfolding the constant definitions.
  3344 
  3345   - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer
  3346     from type nat to type int.
  3347 
  3348 * Lifting: New package intended to generalize the quotient_definition
  3349 facility of the Quotient package; designed to work with Transfer.
  3350 
  3351   - lift_definition command: Defines operations on an abstract type in
  3352     terms of a corresponding operation on a representation
  3353     type.  Example syntax:
  3354 
  3355     lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist"
  3356       is List.insert
  3357 
  3358     Users must discharge a respectfulness proof obligation when each
  3359     constant is defined. (For a type copy, i.e. a typedef with UNIV,
  3360     the proof is discharged automatically.) The obligation is
  3361     presented in a user-friendly, readable form; a respectfulness
  3362     theorem in the standard format and a transfer rule are generated
  3363     by the package.
  3364 
  3365   - Integration with code_abstype: For typedefs (e.g. subtypes
  3366     corresponding to a datatype invariant, such as dlist),
  3367     lift_definition generates a code certificate theorem and sets up
  3368     code generation for each constant.
  3369 
  3370   - setup_lifting command: Sets up the Lifting package to work with a
  3371     user-defined type. The user must provide either a quotient theorem
  3372     or a type_definition theorem.  The package configures transfer
  3373     rules for equality and quantifiers on the type, and sets up the
  3374     lift_definition command to work with the type.
  3375 
  3376   - Usage examples: See Quotient_Examples/Lift_DList.thy,
  3377     Quotient_Examples/Lift_RBT.thy, Quotient_Examples/Lift_FSet.thy,
  3378     Word/Word.thy and Library/Float.thy.
  3379 
  3380 * Quotient package:
  3381 
  3382   - The 'quotient_type' command now supports a 'morphisms' option with
  3383     rep and abs functions, similar to typedef.
  3384 
  3385   - 'quotient_type' sets up new types to work with the Lifting and
  3386     Transfer packages, as with 'setup_lifting'.
  3387 
  3388   - The 'quotient_definition' command now requires the user to prove a
  3389     respectfulness property at the point where the constant is
  3390     defined, similar to lift_definition; INCOMPATIBILITY.
  3391 
  3392   - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems
  3393     accordingly, INCOMPATIBILITY.
  3394 
  3395 * New diagnostic command 'find_unused_assms' to find potentially
  3396 superfluous assumptions in theorems using Quickcheck.
  3397 
  3398 * Quickcheck:
  3399 
  3400   - Quickcheck returns variable assignments as counterexamples, which
  3401     allows to reveal the underspecification of functions under test.
  3402     For example, refuting "hd xs = x", it presents the variable
  3403     assignment xs = [] and x = a1 as a counterexample, assuming that
  3404     any property is false whenever "hd []" occurs in it.
  3405 
  3406     These counterexample are marked as potentially spurious, as
  3407     Quickcheck also returns "xs = []" as a counterexample to the
  3408     obvious theorem "hd xs = hd xs".
  3409 
  3410     After finding a potentially spurious counterexample, Quickcheck
  3411     continues searching for genuine ones.
  3412 
  3413     By default, Quickcheck shows potentially spurious and genuine
  3414     counterexamples. The option "genuine_only" sets quickcheck to only
  3415     show genuine counterexamples.
  3416 
  3417   - The command 'quickcheck_generator' creates random and exhaustive
  3418     value generators for a given type and operations.
  3419 
  3420     It generates values by using the operations as if they were
  3421     constructors of that type.
  3422 
  3423   - Support for multisets.
  3424 
  3425   - Added "use_subtype" options.
  3426 
  3427   - Added "quickcheck_locale" configuration to specify how to process
  3428     conjectures in a locale context.
  3429 
  3430 * Nitpick: Fixed infinite loop caused by the 'peephole_optim' option
  3431 and affecting 'rat' and 'real'.
  3432 
  3433 * Sledgehammer:
  3434   - Integrated more tightly with SPASS, as described in the ITP 2012
  3435     paper "More SPASS with Isabelle".
  3436   - Made it try "smt" as a fallback if "metis" fails or times out.
  3437   - Added support for the following provers: Alt-Ergo (via Why3 and
  3438     TFF1), iProver, iProver-Eq.
  3439   - Sped up the minimizer.
  3440   - Added "lam_trans", "uncurry_aliases", and "minimize" options.
  3441   - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
  3442   - Renamed "sound" option to "strict".
  3443 
  3444 * Metis: Added possibility to specify lambda translations scheme as a
  3445 parenthesized argument (e.g., "by (metis (lifting) ...)").
  3446 
  3447 * SMT: Renamed "smt_fixed" option to "smt_read_only_certificates".
  3448 
  3449 * Command 'try0': Renamed from 'try_methods'. INCOMPATIBILITY.
  3450 
  3451 * New "case_product" attribute to generate a case rule doing multiple
  3452 case distinctions at the same time.  E.g.
  3453 
  3454   list.exhaust [case_product nat.exhaust]
  3455 
  3456 produces a rule which can be used to perform case distinction on both
  3457 a list and a nat.
  3458 
  3459 * New "eventually_elim" method as a generalized variant of the
  3460 eventually_elim* rules.  Supports structured proofs.
  3461 
  3462 * Typedef with implicit set definition is considered legacy.  Use
  3463 "typedef (open)" form instead, which will eventually become the
  3464 default.
  3465 
  3466 * Record: code generation can be switched off manually with
  3467 
  3468   declare [[record_coden = false]]  -- "default true"
  3469 
  3470 * Datatype: type parameters allow explicit sort constraints.
  3471 
  3472 * Concrete syntax for case expressions includes constraints for source
  3473 positions, and thus produces Prover IDE markup for its bindings.
  3474 INCOMPATIBILITY for old-style syntax translations that augment the
  3475 pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
  3476 one_case.
  3477 
  3478 * Clarified attribute "mono_set": pure declaration without modifying
  3479 the result of the fact expression.
  3480 
  3481 * More default pred/set conversions on a couple of relation operations
  3482 and predicates.  Added powers of predicate relations.  Consolidation
  3483 of some relation theorems:
  3484 
  3485   converse_def ~> converse_unfold
  3486   rel_comp_def ~> relcomp_unfold
  3487   symp_def ~> (modified, use symp_def and sym_def instead)
  3488   transp_def ~> transp_trans
  3489   Domain_def ~> Domain_unfold
  3490   Range_def ~> Domain_converse [symmetric]
  3491 
  3492 Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2.
  3493 
  3494 See theory "Relation" for examples for making use of pred/set
  3495 conversions by means of attributes "to_set" and "to_pred".
  3496 
  3497 INCOMPATIBILITY.
  3498 
  3499 * Renamed facts about the power operation on relations, i.e., relpow
  3500 to match the constant's name:
  3501 
  3502   rel_pow_1 ~> relpow_1
  3503   rel_pow_0_I ~> relpow_0_I
  3504   rel_pow_Suc_I ~> relpow_Suc_I
  3505   rel_pow_Suc_I2 ~> relpow_Suc_I2
  3506   rel_pow_0_E ~> relpow_0_E
  3507   rel_pow_Suc_E ~> relpow_Suc_E
  3508   rel_pow_E ~> relpow_E
  3509   rel_pow_Suc_D2 ~> relpow_Suc_D2
  3510   rel_pow_Suc_E2 ~> relpow_Suc_E2
  3511   rel_pow_Suc_D2' ~> relpow_Suc_D2'
  3512   rel_pow_E2 ~> relpow_E2
  3513   rel_pow_add ~> relpow_add
  3514   rel_pow_commute ~> relpow
  3515   rel_pow_empty ~> relpow_empty:
  3516   rtrancl_imp_UN_rel_pow ~> rtrancl_imp_UN_relpow
  3517   rel_pow_imp_rtrancl ~> relpow_imp_rtrancl
  3518   rtrancl_is_UN_rel_pow ~> rtrancl_is_UN_relpow
  3519   rtrancl_imp_rel_pow ~> rtrancl_imp_relpow
  3520   rel_pow_fun_conv ~> relpow_fun_conv
  3521   rel_pow_finite_bounded1 ~> relpow_finite_bounded1
  3522   rel_pow_finite_bounded ~> relpow_finite_bounded
  3523   rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow
  3524   trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow
  3525   single_valued_rel_pow ~> single_valued_relpow
  3526 
  3527 INCOMPATIBILITY.
  3528 
  3529 * Theory Relation: Consolidated constant name for relation composition
  3530 and corresponding theorem names:
  3531 
  3532   - Renamed constant rel_comp to relcomp.
  3533 
  3534   - Dropped abbreviation pred_comp. Use relcompp instead.
  3535 
  3536   - Renamed theorems:
  3537 
  3538     rel_compI ~> relcompI
  3539     rel_compEpair ~> relcompEpair
  3540     rel_compE ~> relcompE
  3541     pred_comp_rel_comp_eq ~> relcompp_relcomp_eq
  3542     rel_comp_empty1 ~> relcomp_empty1
  3543     rel_comp_mono ~> relcomp_mono
  3544     rel_comp_subset_Sigma ~> relcomp_subset_Sigma
  3545     rel_comp_distrib ~> relcomp_distrib
  3546     rel_comp_distrib2 ~> relcomp_distrib2
  3547     rel_comp_UNION_distrib ~> relcomp_UNION_distrib
  3548     rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2
  3549     single_valued_rel_comp ~> single_valued_relcomp
  3550     rel_comp_def ~> relcomp_unfold
  3551     converse_rel_comp ~> converse_relcomp
  3552     pred_compI ~> relcomppI
  3553     pred_compE ~> relcomppE
  3554     pred_comp_bot1 ~> relcompp_bot1
  3555     pred_comp_bot2 ~> relcompp_bot2
  3556     transp_pred_comp_less_eq ~> transp_relcompp_less_eq
  3557     pred_comp_mono ~> relcompp_mono
  3558     pred_comp_distrib ~> relcompp_distrib
  3559     pred_comp_distrib2 ~> relcompp_distrib2
  3560     converse_pred_comp ~> converse_relcompp
  3561 
  3562     finite_rel_comp ~> finite_relcomp
  3563 
  3564     set_rel_comp ~> set_relcomp
  3565 
  3566 INCOMPATIBILITY.
  3567 
  3568 * Theory Divides: Discontinued redundant theorems about div and mod.
  3569 INCOMPATIBILITY, use the corresponding generic theorems instead.
  3570 
  3571   DIVISION_BY_ZERO ~> div_by_0, mod_by_0
  3572   zdiv_self ~> div_self
  3573   zmod_self ~> mod_self
  3574   zdiv_zero ~> div_0
  3575   zmod_zero ~> mod_0
  3576   zdiv_zmod_equality ~> div_mod_equality2
  3577   zdiv_zmod_equality2 ~> div_mod_equality
  3578   zmod_zdiv_trivial ~> mod_div_trivial
  3579   zdiv_zminus_zminus ~> div_minus_minus
  3580   zmod_zminus_zminus ~> mod_minus_minus
  3581   zdiv_zminus2 ~> div_minus_right
  3582   zmod_zminus2 ~> mod_minus_right
  3583   zdiv_minus1_right ~> div_minus1_right
  3584   zmod_minus1_right ~> mod_minus1_right
  3585   zdvd_mult_div_cancel ~> dvd_mult_div_cancel
  3586   zmod_zmult1_eq ~> mod_mult_right_eq
  3587   zpower_zmod ~> power_mod
  3588   zdvd_zmod ~> dvd_mod
  3589   zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd
  3590   mod_mult_distrib ~> mult_mod_left
  3591   mod_mult_distrib2 ~> mult_mod_right
  3592 
  3593 * Removed redundant theorems nat_mult_2 and nat_mult_2_right; use
  3594 generic mult_2 and mult_2_right instead. INCOMPATIBILITY.
  3595 
  3596 * Finite_Set.fold now qualified.  INCOMPATIBILITY.
  3597 
  3598 * Consolidated theorem names concerning fold combinators:
  3599 
  3600   inf_INFI_fold_inf ~> inf_INF_fold_inf
  3601   sup_SUPR_fold_sup ~> sup_SUP_fold_sup
  3602   INFI_fold_inf ~> INF_fold_inf
  3603   SUPR_fold_sup ~> SUP_fold_sup
  3604   union_set ~> union_set_fold
  3605   minus_set ~> minus_set_fold
  3606   INFI_set_fold ~> INF_set_fold
  3607   SUPR_set_fold ~> SUP_set_fold
  3608   INF_code ~> INF_set_foldr
  3609   SUP_code ~> SUP_set_foldr
  3610   foldr.simps ~> foldr.simps (in point-free formulation)
  3611   foldr_fold_rev ~> foldr_conv_fold
  3612   foldl_fold ~> foldl_conv_fold
  3613   foldr_foldr ~> foldr_conv_foldl
  3614   foldl_foldr ~> foldl_conv_foldr
  3615   fold_set_remdups ~> fold_set_fold_remdups
  3616   fold_set ~> fold_set_fold
  3617   fold1_set ~> fold1_set_fold
  3618 
  3619 INCOMPATIBILITY.
  3620 
  3621 * Dropped rarely useful theorems concerning fold combinators:
  3622 foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant,
  3623 rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,
  3624 concat_conv_foldl, foldl_weak_invariant, foldl_invariant,
  3625 foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,
  3626 listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc,
  3627 foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.
  3628 INCOMPATIBILITY.  For the common phrases "%xs. List.foldr plus xs 0"
  3629 and "List.foldl plus 0", prefer "List.listsum".  Otherwise it can be
  3630 useful to boil down "List.foldr" and "List.foldl" to "List.fold" by
  3631 unfolding "foldr_conv_fold" and "foldl_conv_fold".
  3632 
  3633 * Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,
  3634 inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,
  3635 Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,
  3636 INF_set_foldr, SUP_set_foldr.  INCOMPATIBILITY.  Prefer corresponding
  3637 lemmas over fold rather than foldr, or make use of lemmas
  3638 fold_conv_foldr and fold_rev.
  3639 
  3640 * Congruence rules Option.map_cong and Option.bind_cong for recursion
  3641 through option types.
  3642 
  3643 * "Transitive_Closure.ntrancl": bounded transitive closure on
  3644 relations.
  3645 
  3646 * Constant "Set.not_member" now qualified.  INCOMPATIBILITY.
  3647 
  3648 * Theory Int: Discontinued many legacy theorems specific to type int.
  3649 INCOMPATIBILITY, use the corresponding generic theorems instead.
  3650 
  3651   zminus_zminus ~> minus_minus
  3652   zminus_0 ~> minus_zero
  3653   zminus_zadd_distrib ~> minus_add_distrib
  3654   zadd_commute ~> add_commute
  3655   zadd_assoc ~> add_assoc
  3656   zadd_left_commute ~> add_left_commute
  3657   zadd_ac ~> add_ac
  3658   zmult_ac ~> mult_ac
  3659   zadd_0 ~> add_0_left
  3660   zadd_0_right ~> add_0_right
  3661   zadd_zminus_inverse2 ~> left_minus
  3662   zmult_zminus ~> mult_minus_left
  3663   zmult_commute ~> mult_commute
  3664   zmult_assoc ~> mult_assoc
  3665   zadd_zmult_distrib ~> left_distrib
  3666   zadd_zmult_distrib2 ~> right_distrib
  3667   zdiff_zmult_distrib ~> left_diff_distrib
  3668   zdiff_zmult_distrib2 ~> right_diff_distrib
  3669   zmult_1 ~> mult_1_left
  3670   zmult_1_right ~> mult_1_right
  3671   zle_refl ~> order_refl
  3672   zle_trans ~> order_trans
  3673   zle_antisym ~> order_antisym
  3674   zle_linear ~> linorder_linear
  3675   zless_linear ~> linorder_less_linear
  3676   zadd_left_mono ~> add_left_mono
  3677   zadd_strict_right_mono ~> add_strict_right_mono
  3678   zadd_zless_mono ~> add_less_le_mono
  3679   int_0_less_1 ~> zero_less_one
  3680   int_0_neq_1 ~> zero_neq_one
  3681   zless_le ~> less_le
  3682   zpower_zadd_distrib ~> power_add
  3683   zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
  3684   zero_le_zpower_abs ~> zero_le_power_abs
  3685 
  3686 * Theory Deriv: Renamed
  3687 
  3688   DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing
  3689 
  3690 * Theory Library/Multiset: Improved code generation of multisets.
  3691 
  3692 * Theory HOL/Library/Set_Algebras: Addition and multiplication on sets
  3693 are expressed via type classes again. The special syntax
  3694 \<oplus>/\<otimes> has been replaced by plain +/*. Removed constant
  3695 setsum_set, which is now subsumed by Big_Operators.setsum.
  3696 INCOMPATIBILITY.
  3697 
  3698 * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,
  3699 use theory HOL/Library/Nat_Bijection instead.
  3700 
  3701 * Theory HOL/Library/RBT_Impl: Backing implementation of red-black
  3702 trees is now inside a type class context.  Names of affected
  3703 operations and lemmas have been prefixed by rbt_.  INCOMPATIBILITY for
  3704 theories working directly with raw red-black trees, adapt the names as
  3705 follows:
  3706 
  3707   Operations:
  3708   bulkload -> rbt_bulkload
  3709   del_from_left -> rbt_del_from_left
  3710   del_from_right -> rbt_del_from_right
  3711   del -> rbt_del
  3712   delete -> rbt_delete
  3713   ins -> rbt_ins
  3714   insert -> rbt_insert
  3715   insertw -> rbt_insert_with
  3716   insert_with_key -> rbt_insert_with_key
  3717   map_entry -> rbt_map_entry
  3718   lookup -> rbt_lookup
  3719   sorted -> rbt_sorted
  3720   tree_greater -> rbt_greater
  3721   tree_less -> rbt_less
  3722   tree_less_symbol -> rbt_less_symbol
  3723   union -> rbt_union
  3724   union_with -> rbt_union_with
  3725   union_with_key -> rbt_union_with_key
  3726 
  3727   Lemmas:
  3728   balance_left_sorted -> balance_left_rbt_sorted
  3729   balance_left_tree_greater -> balance_left_rbt_greater
  3730   balance_left_tree_less -> balance_left_rbt_less
  3731   balance_right_sorted -> balance_right_rbt_sorted
  3732   balance_right_tree_greater -> balance_right_rbt_greater
  3733   balance_right_tree_less -> balance_right_rbt_less
  3734   balance_sorted -> balance_rbt_sorted
  3735   balance_tree_greater -> balance_rbt_greater
  3736   balance_tree_less -> balance_rbt_less
  3737   bulkload_is_rbt -> rbt_bulkload_is_rbt
  3738   combine_sorted -> combine_rbt_sorted
  3739   combine_tree_greater -> combine_rbt_greater
  3740   combine_tree_less -> combine_rbt_less
  3741   delete_in_tree -> rbt_delete_in_tree
  3742   delete_is_rbt -> rbt_delete_is_rbt
  3743   del_from_left_tree_greater -> rbt_del_from_left_rbt_greater
  3744   del_from_left_tree_less -> rbt_del_from_left_rbt_less
  3745   del_from_right_tree_greater -> rbt_del_from_right_rbt_greater
  3746   del_from_right_tree_less -> rbt_del_from_right_rbt_less
  3747   del_in_tree -> rbt_del_in_tree
  3748   del_inv1_inv2 -> rbt_del_inv1_inv2
  3749   del_sorted -> rbt_del_rbt_sorted
  3750   del_tree_greater -> rbt_del_rbt_greater
  3751   del_tree_less -> rbt_del_rbt_less
  3752   dom_lookup_Branch -> dom_rbt_lookup_Branch
  3753   entries_lookup -> entries_rbt_lookup
  3754   finite_dom_lookup -> finite_dom_rbt_lookup
  3755   insert_sorted -> rbt_insert_rbt_sorted
  3756   insertw_is_rbt -> rbt_insertw_is_rbt
  3757   insertwk_is_rbt -> rbt_insertwk_is_rbt
  3758   insertwk_sorted -> rbt_insertwk_rbt_sorted
  3759   insertw_sorted -> rbt_insertw_rbt_sorted
  3760   ins_sorted -> ins_rbt_sorted
  3761   ins_tree_greater -> ins_rbt_greater
  3762   ins_tree_less -> ins_rbt_less
  3763   is_rbt_sorted -> is_rbt_rbt_sorted
  3764   lookup_balance -> rbt_lookup_balance
  3765   lookup_bulkload -> rbt_lookup_rbt_bulkload
  3766   lookup_delete -> rbt_lookup_rbt_delete
  3767   lookup_Empty -> rbt_lookup_Empty
  3768   lookup_from_in_tree -> rbt_lookup_from_in_tree
  3769   lookup_in_tree -> rbt_lookup_in_tree
  3770   lookup_ins -> rbt_lookup_ins
  3771   lookup_insert -> rbt_lookup_rbt_insert
  3772   lookup_insertw -> rbt_lookup_rbt_insertw
  3773   lookup_insertwk -> rbt_lookup_rbt_insertwk
  3774   lookup_keys -> rbt_lookup_keys
  3775   lookup_map -> rbt_lookup_map
  3776   lookup_map_entry -> rbt_lookup_rbt_map_entry
  3777   lookup_tree_greater -> rbt_lookup_rbt_greater
  3778   lookup_tree_less -> rbt_lookup_rbt_less
  3779   lookup_union -> rbt_lookup_rbt_union
  3780   map_entry_color_of -> rbt_map_entry_color_of
  3781   map_entry_inv1 -> rbt_map_entry_inv1
  3782   map_entry_inv2 -> rbt_map_entry_inv2
  3783   map_entry_is_rbt -> rbt_map_entry_is_rbt
  3784   map_entry_sorted -> rbt_map_entry_rbt_sorted
  3785   map_entry_tree_greater -> rbt_map_entry_rbt_greater
  3786   map_entry_tree_less -> rbt_map_entry_rbt_less
  3787   map_tree_greater -> map_rbt_greater
  3788   map_tree_less -> map_rbt_less
  3789   map_sorted -> map_rbt_sorted
  3790   paint_sorted -> paint_rbt_sorted
  3791   paint_lookup -> paint_rbt_lookup
  3792   paint_tree_greater -> paint_rbt_greater
  3793   paint_tree_less -> paint_rbt_less
  3794   sorted_entries -> rbt_sorted_entries
  3795   tree_greater_eq_trans -> rbt_greater_eq_trans
  3796   tree_greater_nit -> rbt_greater_nit
  3797   tree_greater_prop -> rbt_greater_prop
  3798   tree_greater_simps -> rbt_greater_simps
  3799   tree_greater_trans -> rbt_greater_trans
  3800   tree_less_eq_trans -> rbt_less_eq_trans
  3801   tree_less_nit -> rbt_less_nit
  3802   tree_less_prop -> rbt_less_prop
  3803   tree_less_simps -> rbt_less_simps
  3804   tree_less_trans -> rbt_less_trans
  3805   tree_ord_props -> rbt_ord_props
  3806   union_Branch -> rbt_union_Branch
  3807   union_is_rbt -> rbt_union_is_rbt
  3808   unionw_is_rbt -> rbt_unionw_is_rbt
  3809   unionwk_is_rbt -> rbt_unionwk_is_rbt
  3810   unionwk_sorted -> rbt_unionwk_rbt_sorted
  3811 
  3812 * Theory HOL/Library/Float: Floating point numbers are now defined as
  3813 a subset of the real numbers.  All operations are defined using the
  3814 lifing-framework and proofs use the transfer method.  INCOMPATIBILITY.
  3815 
  3816   Changed Operations:
  3817   float_abs -> abs
  3818   float_nprt -> nprt
  3819   float_pprt -> pprt
  3820   pow2 -> use powr
  3821   round_down -> float_round_down
  3822   round_up -> float_round_up
  3823   scale -> exponent
  3824 
  3825   Removed Operations:
  3826   ceiling_fl, lb_mult, lb_mod, ub_mult, ub_mod
  3827 
  3828   Renamed Lemmas:
  3829   abs_float_def -> Float.compute_float_abs
  3830   bitlen_ge0 -> bitlen_nonneg
  3831   bitlen.simps -> Float.compute_bitlen
  3832   float_components -> Float_mantissa_exponent
  3833   float_divl.simps -> Float.compute_float_divl
  3834   float_divr.simps -> Float.compute_float_divr
  3835   float_eq_odd -> mult_powr_eq_mult_powr_iff
  3836   float_power -> real_of_float_power
  3837   lapprox_posrat_def -> Float.compute_lapprox_posrat
  3838   lapprox_rat.simps -> Float.compute_lapprox_rat
  3839   le_float_def' -> Float.compute_float_le
  3840   le_float_def -> less_eq_float.rep_eq
  3841   less_float_def' -> Float.compute_float_less
  3842   less_float_def -> less_float.rep_eq
  3843   normfloat_def -> Float.compute_normfloat
  3844   normfloat_imp_odd_or_zero -> mantissa_not_dvd and mantissa_noteq_0
  3845   normfloat -> normfloat_def
  3846   normfloat_unique -> use normfloat_def
  3847   number_of_float_Float -> Float.compute_float_numeral, Float.compute_float_neg_numeral
  3848   one_float_def -> Float.compute_float_one
  3849   plus_float_def -> Float.compute_float_plus
  3850   rapprox_posrat_def -> Float.compute_rapprox_posrat
  3851   rapprox_rat.simps -> Float.compute_rapprox_rat
  3852   real_of_float_0 -> zero_float.rep_eq
  3853   real_of_float_1 -> one_float.rep_eq
  3854   real_of_float_abs -> abs_float.rep_eq
  3855   real_of_float_add -> plus_float.rep_eq
  3856   real_of_float_minus -> uminus_float.rep_eq
  3857   real_of_float_mult -> times_float.rep_eq
  3858   real_of_float_simp -> Float.rep_eq
  3859   real_of_float_sub -> minus_float.rep_eq
  3860   round_down.simps -> Float.compute_float_round_down
  3861   round_up.simps -> Float.compute_float_round_up
  3862   times_float_def -> Float.compute_float_times
  3863   uminus_float_def -> Float.compute_float_uminus
  3864   zero_float_def -> Float.compute_float_zero
  3865 
  3866   Lemmas not necessary anymore, use the transfer method:
  3867   bitlen_B0, bitlen_B1, bitlen_ge1, bitlen_Min, bitlen_Pls, float_divl,
  3868   float_divr, float_le_simp, float_less1_mantissa_bound,
  3869   float_less_simp, float_less_zero, float_le_zero,
  3870   float_pos_less1_e_neg, float_pos_m_pos, float_split, float_split2,
  3871   floor_pos_exp, lapprox_posrat, lapprox_posrat_bottom, lapprox_rat,
  3872   lapprox_rat_bottom, normalized_float, rapprox_posrat,
  3873   rapprox_posrat_le1, rapprox_rat, real_of_float_ge0_exp,
  3874   real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl,
  3875   round_up, zero_le_float, zero_less_float
  3876 
  3877 * New theory HOL/Library/DAList provides an abstract type for
  3878 association lists with distinct keys.
  3879 
  3880 * Session HOL/IMP: Added new theory of abstract interpretation of
  3881 annotated commands.
  3882 
  3883 * Session HOL-Import: Re-implementation from scratch is faster,
  3884 simpler, and more scalable.  Requires a proof bundle, which is
  3885 available as an external component.  Discontinued old (and mostly
  3886 dead) Importer for HOL4 and HOL Light.  INCOMPATIBILITY.
  3887 
  3888 * Session HOL-Word: Discontinued many redundant theorems specific to
  3889 type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
  3890 instead.
  3891 
  3892   word_sub_alt ~> word_sub_wi
  3893   word_add_alt ~> word_add_def
  3894   word_mult_alt ~> word_mult_def
  3895   word_minus_alt ~> word_minus_def
  3896   word_0_alt ~> word_0_wi
  3897   word_1_alt ~> word_1_wi
  3898   word_add_0 ~> add_0_left
  3899   word_add_0_right ~> add_0_right
  3900   word_mult_1 ~> mult_1_left
  3901   word_mult_1_right ~> mult_1_right
  3902   word_add_commute ~> add_commute
  3903   word_add_assoc ~> add_assoc
  3904   word_add_left_commute ~> add_left_commute
  3905   word_mult_commute ~> mult_commute
  3906   word_mult_assoc ~> mult_assoc
  3907   word_mult_left_commute ~> mult_left_commute
  3908   word_left_distrib ~> left_distrib
  3909   word_right_distrib ~> right_distrib
  3910   word_left_minus ~> left_minus
  3911   word_diff_0_right ~> diff_0_right
  3912   word_diff_self ~> diff_self
  3913   word_sub_def ~> diff_minus
  3914   word_diff_minus ~> diff_minus
  3915   word_add_ac ~> add_ac
  3916   word_mult_ac ~> mult_ac
  3917   word_plus_ac0 ~> add_0_left add_0_right add_ac
  3918   word_times_ac1 ~> mult_1_left mult_1_right mult_ac
  3919   word_order_trans ~> order_trans
  3920   word_order_refl ~> order_refl
  3921   word_order_antisym ~> order_antisym
  3922   word_order_linear ~> linorder_linear
  3923   lenw1_zero_neq_one ~> zero_neq_one
  3924   word_number_of_eq ~> number_of_eq
  3925   word_of_int_add_hom ~> wi_hom_add
  3926   word_of_int_sub_hom ~> wi_hom_sub
  3927   word_of_int_mult_hom ~> wi_hom_mult
  3928   word_of_int_minus_hom ~> wi_hom_neg
  3929   word_of_int_succ_hom ~> wi_hom_succ
  3930   word_of_int_pred_hom ~> wi_hom_pred
  3931   word_of_int_0_hom ~> word_0_wi
  3932   word_of_int_1_hom ~> word_1_wi
  3933 
  3934 * Session HOL-Word: New proof method "word_bitwise" for splitting
  3935 machine word equalities and inequalities into logical circuits,
  3936 defined in HOL/Word/WordBitwise.thy.  Supports addition, subtraction,
  3937 multiplication, shifting by constants, bitwise operators and numeric
  3938 constants.  Requires fixed-length word types, not 'a word.  Solves
  3939 many standard word identities outright and converts more into first
  3940 order problems amenable to blast or similar.  See also examples in
  3941 HOL/Word/Examples/WordExamples.thy.
  3942 
  3943 * Session HOL-Probability: Introduced the type "'a measure" to
  3944 represent measures, this replaces the records 'a algebra and 'a
  3945 measure_space.  The locales based on subset_class now have two
  3946 locale-parameters the space \<Omega> and the set of measurable sets M.
  3947 The product of probability spaces uses now the same constant as the
  3948 finite product of sigma-finite measure spaces "PiM :: ('i => 'a)
  3949 measure".  Most constants are defined now outside of locales and gain
  3950 an additional parameter, like null_sets, almost_eventually or \<mu>'.
  3951 Measure space constructions for distributions and densities now got
  3952 their own constants distr and density.  Instead of using locales to
  3953 describe measure spaces with a finite space, the measure count_space
  3954 and point_measure is introduced.  INCOMPATIBILITY.
  3955 
  3956   Renamed constants:
  3957   measure -> emeasure
  3958   finite_measure.\<mu>' -> measure
  3959   product_algebra_generator -> prod_algebra
  3960   product_prob_space.emb -> prod_emb
  3961   product_prob_space.infprod_algebra -> PiM
  3962 
  3963   Removed locales:
  3964   completeable_measure_space
  3965   finite_measure_space
  3966   finite_prob_space
  3967   finite_product_finite_prob_space
  3968   finite_product_sigma_algebra
  3969   finite_sigma_algebra
  3970   measure_space
  3971   pair_finite_prob_space
  3972   pair_finite_sigma_algebra
  3973   pair_finite_space
  3974   pair_sigma_algebra
  3975   product_sigma_algebra
  3976 
  3977   Removed constants:
  3978   conditional_space
  3979   distribution -> use distr measure, or distributed predicate
  3980   image_space
  3981   joint_distribution -> use distr measure, or distributed predicate
  3982   pair_measure_generator
  3983   product_prob_space.infprod_algebra -> use PiM
  3984   subvimage
  3985 
  3986   Replacement theorems:
  3987   finite_additivity_sufficient -> ring_of_sets.countably_additiveI_finite
  3988   finite_measure.empty_measure -> measure_empty
  3989   finite_measure.finite_continuity_from_above -> finite_measure.finite_Lim_measure_decseq
  3990   finite_measure.finite_continuity_from_below -> finite_measure.finite_Lim_measure_incseq
  3991   finite_measure.finite_measure_countably_subadditive -> finite_measure.finite_measure_subadditive_countably
  3992   finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure
  3993   finite_measure.finite_measure -> finite_measure.emeasure_finite
  3994   finite_measure.finite_measure_finite_singleton -> finite_measure.finite_measure_eq_setsum_singleton
  3995   finite_measure.positive_measure' -> measure_nonneg
  3996   finite_measure.real_measure -> finite_measure.emeasure_real
  3997   finite_product_prob_space.finite_measure_times -> finite_product_prob_space.finite_measure_PiM_emb
  3998   finite_product_sigma_algebra.in_P -> sets_PiM_I_finite
  3999   finite_product_sigma_algebra.P_empty -> space_PiM_empty, sets_PiM_empty
  4000   information_space.conditional_entropy_eq -> information_space.conditional_entropy_simple_distributed
  4001   information_space.conditional_entropy_positive -> information_space.conditional_entropy_nonneg_simple
  4002   information_space.conditional_mutual_information_eq_mutual_information -> information_space.conditional_mutual_information_eq_mutual_information_simple
  4003   information_space.conditional_mutual_information_generic_positive -> information_space.conditional_mutual_information_nonneg_simple
  4004   information_space.conditional_mutual_information_positive -> information_space.conditional_mutual_information_nonneg_simple
  4005   information_space.entropy_commute -> information_space.entropy_commute_simple
  4006   information_space.entropy_eq -> information_space.entropy_simple_distributed
  4007   information_space.entropy_generic_eq -> information_space.entropy_simple_distributed
  4008   information_space.entropy_positive -> information_space.entropy_nonneg_simple
  4009   information_space.entropy_uniform_max -> information_space.entropy_uniform
  4010   information_space.KL_eq_0_imp -> information_space.KL_eq_0_iff_eq
  4011   information_space.KL_eq_0 -> information_space.KL_same_eq_0
  4012   information_space.KL_ge_0 -> information_space.KL_nonneg
  4013   information_space.mutual_information_eq -> information_space.mutual_information_simple_distributed
  4014   information_space.mutual_information_positive -> information_space.mutual_information_nonneg_simple
  4015   Int_stable_cuboids -> Int_stable_atLeastAtMost
  4016   Int_stable_product_algebra_generator -> positive_integral
  4017   measure_preserving -> equality "distr M N f = N" "f : measurable M N"
  4018   measure_space.additive -> emeasure_additive
  4019   measure_space.AE_iff_null_set -> AE_iff_null
  4020   measure_space.almost_everywhere_def -> eventually_ae_filter
  4021   measure_space.almost_everywhere_vimage -> AE_distrD
  4022   measure_space.continuity_from_above -> INF_emeasure_decseq
  4023   measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq
  4024   measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq
  4025   measure_space.continuity_from_below -> SUP_emeasure_incseq
  4026   measure_space_density -> emeasure_density
  4027   measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density
  4028   measure_space.integrable_vimage -> integrable_distr
  4029   measure_space.integral_translated_density -> integral_density
  4030   measure_space.integral_vimage -> integral_distr
  4031   measure_space.measure_additive -> plus_emeasure
  4032   measure_space.measure_compl -> emeasure_compl
  4033   measure_space.measure_countable_increasing -> emeasure_countable_increasing
  4034   measure_space.measure_countably_subadditive -> emeasure_subadditive_countably
  4035   measure_space.measure_decseq -> decseq_emeasure
  4036   measure_space.measure_Diff -> emeasure_Diff
  4037   measure_space.measure_Diff_null_set -> emeasure_Diff_null_set
  4038   measure_space.measure_eq_0 -> emeasure_eq_0
  4039   measure_space.measure_finitely_subadditive -> emeasure_subadditive_finite
  4040   measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton
  4041   measure_space.measure_incseq -> incseq_emeasure
  4042   measure_space.measure_insert -> emeasure_insert
  4043   measure_space.measure_mono -> emeasure_mono
  4044   measure_space.measure_not_negative -> emeasure_not_MInf
  4045   measure_space.measure_preserving_Int_stable -> measure_eqI_generator_eq
  4046   measure_space.measure_setsum -> setsum_emeasure
  4047   measure_space.measure_setsum_split -> setsum_emeasure_cover
  4048   measure_space.measure_space_vimage -> emeasure_distr
  4049   measure_space.measure_subadditive_finite -> emeasure_subadditive_finite
  4050   measure_space.measure_subadditive -> subadditive
  4051   measure_space.measure_top -> emeasure_space
  4052   measure_space.measure_UN_eq_0 -> emeasure_UN_eq_0
  4053   measure_space.measure_Un_null_set -> emeasure_Un_null_set
  4054   measure_space.positive_integral_translated_density -> positive_integral_density
  4055   measure_space.positive_integral_vimage -> positive_integral_distr
  4056   measure_space.real_continuity_from_above -> Lim_measure_decseq
  4057   measure_space.real_continuity_from_below -> Lim_measure_incseq
  4058   measure_space.real_measure_countably_subadditive -> measure_subadditive_countably
  4059   measure_space.real_measure_Diff -> measure_Diff
  4060   measure_space.real_measure_finite_Union -> measure_finite_Union
  4061   measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton
  4062   measure_space.real_measure_subadditive -> measure_subadditive
  4063   measure_space.real_measure_Union -> measure_Union
  4064   measure_space.real_measure_UNION -> measure_UNION
  4065   measure_space.simple_function_vimage -> simple_function_comp
  4066   measure_space.simple_integral_vimage -> simple_integral_distr
  4067   measure_space.simple_integral_vimage -> simple_integral_distr
  4068   measure_unique_Int_stable -> measure_eqI_generator_eq
  4069   measure_unique_Int_stable_vimage -> measure_eqI_generator_eq
  4070   pair_sigma_algebra.measurable_cut_fst -> sets_Pair1
  4071   pair_sigma_algebra.measurable_cut_snd -> sets_Pair2
  4072   pair_sigma_algebra.measurable_pair_image_fst -> measurable_Pair1
  4073   pair_sigma_algebra.measurable_pair_image_snd -> measurable_Pair2
  4074   pair_sigma_algebra.measurable_product_swap -> measurable_pair_swap_iff
  4075   pair_sigma_algebra.pair_sigma_algebra_measurable -> measurable_pair_swap
  4076   pair_sigma_algebra.pair_sigma_algebra_swap_measurable -> measurable_pair_swap'
  4077   pair_sigma_algebra.sets_swap -> sets_pair_swap
  4078   pair_sigma_finite.measure_cut_measurable_fst -> pair_sigma_finite.measurable_emeasure_Pair1
  4079   pair_sigma_finite.measure_cut_measurable_snd -> pair_sigma_finite.measurable_emeasure_Pair2
  4080   pair_sigma_finite.measure_preserving_swap -> pair_sigma_finite.distr_pair_swap
  4081   pair_sigma_finite.pair_measure_alt2 -> pair_sigma_finite.emeasure_pair_measure_alt2
  4082   pair_sigma_finite.pair_measure_alt -> pair_sigma_finite.emeasure_pair_measure_alt
  4083   pair_sigma_finite.pair_measure_times -> pair_sigma_finite.emeasure_pair_measure_Times
  4084   prob_space.indep_distribution_eq_measure -> prob_space.indep_vars_iff_distr_eq_PiM
  4085   prob_space.indep_var_distributionD -> prob_space.indep_var_distribution_eq
  4086   prob_space.measure_space_1 -> prob_space.emeasure_space_1
  4087   prob_space.prob_space_vimage -> prob_space_distr
  4088   prob_space.random_variable_restrict -> measurable_restrict
  4089   prob_space_unique_Int_stable -> measure_eqI_prob_space
  4090   product_algebraE -> prod_algebraE_all
  4091   product_algebra_generator_der -> prod_algebra_eq_finite
  4092   product_algebra_generator_into_space -> prod_algebra_sets_into_space
  4093   product_algebraI -> sets_PiM_I_finite
  4094   product_measure_exists -> product_sigma_finite.sigma_finite
  4095   product_prob_space.finite_index_eq_finite_product -> product_prob_space.sets_PiM_generator
  4096   product_prob_space.finite_measure_infprod_emb_Pi -> product_prob_space.measure_PiM_emb
  4097   product_prob_space.infprod_spec -> product_prob_space.emeasure_PiM_emb_not_empty
  4098   product_prob_space.measurable_component -> measurable_component_singleton
  4099   product_prob_space.measurable_emb -> measurable_prod_emb
  4100   product_prob_space.measurable_into_infprod_algebra -> measurable_PiM_single
  4101   product_prob_space.measurable_singleton_infprod -> measurable_component_singleton
  4102   product_prob_space.measure_emb -> emeasure_prod_emb
  4103   product_prob_space.measure_preserving_restrict -> product_prob_space.distr_restrict
  4104   product_sigma_algebra.product_algebra_into_space -> space_closed
  4105   product_sigma_finite.measure_fold -> product_sigma_finite.distr_merge
  4106   product_sigma_finite.measure_preserving_component_singelton -> product_sigma_finite.distr_singleton
  4107   product_sigma_finite.measure_preserving_merge -> product_sigma_finite.distr_merge
  4108   sequence_space.measure_infprod -> sequence_space.measure_PiM_countable
  4109   sets_product_algebra -> sets_PiM
  4110   sigma_algebra.measurable_sigma -> measurable_measure_of
  4111   sigma_finite_measure.disjoint_sigma_finite -> sigma_finite_disjoint
  4112   sigma_finite_measure.RN_deriv_vimage -> sigma_finite_measure.RN_deriv_distr
  4113   sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq
  4114   space_product_algebra -> space_PiM
  4115 
  4116 * Session HOL-TPTP: support to parse and import TPTP problems (all
  4117 languages) into Isabelle/HOL.
  4118 
  4119 
  4120 *** FOL ***
  4121 
  4122 * New "case_product" attribute (see HOL).
  4123 
  4124 
  4125 *** ZF ***
  4126 
  4127 * Greater support for structured proofs involving induction or case
  4128 analysis.
  4129 
  4130 * Much greater use of mathematical symbols.
  4131 
  4132 * Removal of many ML theorem bindings.  INCOMPATIBILITY.
  4133 
  4134 
  4135 *** ML ***
  4136 
  4137 * Antiquotation @{keyword "name"} produces a parser for outer syntax
  4138 from a minor keyword introduced via theory header declaration.
  4139 
  4140 * Antiquotation @{command_spec "name"} produces the
  4141 Outer_Syntax.command_spec from a major keyword introduced via theory
  4142 header declaration; it can be passed to Outer_Syntax.command etc.
  4143 
  4144 * Local_Theory.define no longer hard-wires default theorem name
  4145 "foo_def", but retains the binding as given.  If that is Binding.empty
  4146 / Attrib.empty_binding, the result is not registered as user-level
  4147 fact.  The Local_Theory.define_internal variant allows to specify a
  4148 non-empty name (used for the foundation in the background theory),
  4149 while omitting the fact binding in the user-context.  Potential
  4150 INCOMPATIBILITY for derived definitional packages: need to specify
  4151 naming policy for primitive definitions more explicitly.
  4152 
  4153 * Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in
  4154 conformance with similar operations in structure Term and Logic.
  4155 
  4156 * Antiquotation @{attributes [...]} embeds attribute source
  4157 representation into the ML text, which is particularly useful with
  4158 declarations like Local_Theory.note.
  4159 
  4160 * Structure Proof_Context follows standard naming scheme.  Old
  4161 ProofContext has been discontinued.  INCOMPATIBILITY.
  4162 
  4163 * Refined Local_Theory.declaration {syntax, pervasive}, with subtle
  4164 change of semantics: update is applied to auxiliary local theory
  4165 context as well.
  4166 
  4167 * Modernized some old-style infix operations:
  4168 
  4169   addeqcongs    ~> Simplifier.add_eqcong
  4170   deleqcongs    ~> Simplifier.del_eqcong
  4171   addcongs      ~> Simplifier.add_cong
  4172   delcongs      ~> Simplifier.del_cong
  4173   setmksimps    ~> Simplifier.set_mksimps
  4174   setmkcong     ~> Simplifier.set_mkcong
  4175   setmksym      ~> Simplifier.set_mksym
  4176   setmkeqTrue   ~> Simplifier.set_mkeqTrue
  4177   settermless   ~> Simplifier.set_termless
  4178   setsubgoaler  ~> Simplifier.set_subgoaler
  4179   addsplits     ~> Splitter.add_split
  4180   delsplits     ~> Splitter.del_split
  4181 
  4182 
  4183 *** System ***
  4184 
  4185 * USER_HOME settings variable points to cross-platform user home
  4186 directory, which coincides with HOME on POSIX systems only.  Likewise,
  4187 the Isabelle path specification "~" now expands to $USER_HOME, instead
  4188 of former $HOME.  A different default for USER_HOME may be set
  4189 explicitly in shell environment, before Isabelle settings are
  4190 evaluated.  Minor INCOMPATIBILITY: need to adapt Isabelle path where
  4191 the generic user home was intended.
  4192 
  4193 * ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name
  4194 notation, which is useful for the jEdit file browser, for example.
  4195 
  4196 * ISABELLE_JDK_HOME settings variable points to JDK with javac and jar
  4197 (not just JRE).
  4198 
  4199 
  4200 
  4201 New in Isabelle2011-1 (October 2011)
  4202 ------------------------------------
  4203 
  4204 *** General ***
  4205 
  4206 * Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as
  4207 "isabelle jedit" or "ISABELLE_HOME/Isabelle" on the command line.
  4208 
  4209   - Management of multiple theory files directly from the editor
  4210     buffer store -- bypassing the file-system (no requirement to save
  4211     files for checking).
  4212 
  4213   - Markup of formal entities within the text buffer, with semantic
  4214     highlighting, tooltips and hyperlinks to jump to defining source
  4215     positions.
  4216 
  4217   - Improved text rendering, with sub/superscripts in the source
  4218     buffer (including support for copy/paste wrt. output panel, HTML
  4219     theory output and other non-Isabelle text boxes).
  4220 
  4221   - Refined scheduling of proof checking and printing of results,
  4222     based on interactive editor view.  (Note: jEdit folding and
  4223     narrowing allows to restrict buffer perspectives explicitly.)
  4224 
  4225   - Reduced CPU performance requirements, usable on machines with few
  4226     cores.
  4227 
  4228   - Reduced memory requirements due to pruning of unused document
  4229     versions (garbage collection).
  4230 
  4231 See also ~~/src/Tools/jEdit/README.html for further information,
  4232 including some remaining limitations.
  4233 
  4234 * Theory loader: source files are exclusively located via the master
  4235 directory of each theory node (where the .thy file itself resides).
  4236 The global load path (such as src/HOL/Library) has been discontinued.
  4237 Note that the path element ~~ may be used to reference theories in the
  4238 Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet".
  4239 INCOMPATIBILITY.
  4240 
  4241 * Theory loader: source files are identified by content via SHA1
  4242 digests.  Discontinued former path/modtime identification and optional
  4243 ISABELLE_FILE_IDENT plugin scripts.
  4244 
  4245 * Parallelization of nested Isar proofs is subject to
  4246 Goal.parallel_proofs_threshold (default 100).  See also isabelle
  4247 usedir option -Q.
  4248 
  4249 * Name space: former unsynchronized references are now proper
  4250 configuration options, with more conventional names:
  4251 
  4252   long_names   ~> names_long
  4253   short_names  ~> names_short
  4254   unique_names ~> names_unique
  4255 
  4256 Minor INCOMPATIBILITY, need to declare options in context like this:
  4257 
  4258   declare [[names_unique = false]]
  4259 
  4260 * Literal facts `prop` may contain dummy patterns, e.g. `_ = _`.  Note
  4261 that the result needs to be unique, which means fact specifications
  4262 may have to be refined after enriching a proof context.
  4263 
  4264 * Attribute "case_names" has been refined: the assumptions in each case
  4265 can be named now by following the case name with [name1 name2 ...].
  4266 
  4267 * Isabelle/Isar reference manual has been updated and extended:
  4268   - "Synopsis" provides a catalog of main Isar language concepts.
  4269   - Formal references in syntax diagrams, via @{rail} antiquotation.
  4270   - Updated material from classic "ref" manual, notably about
  4271     "Classical Reasoner".
  4272 
  4273 
  4274 *** HOL ***
  4275 
  4276 * Class bot and top require underlying partial order rather than
  4277 preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
  4278 
  4279 * Class complete_lattice: generalized a couple of lemmas from sets;
  4280 generalized theorems INF_cong and SUP_cong.  New type classes for
  4281 complete boolean algebras and complete linear orders.  Lemmas
  4282 Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in
  4283 class complete_linorder.
  4284 
  4285 Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def,
  4286 Sup_fun_def, Inf_apply, Sup_apply.
  4287 
  4288 Removed redundant lemmas (the right hand side gives hints how to
  4289 replace them for (metis ...), or (simp only: ...) proofs):
  4290 
  4291   Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right]
  4292   Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right]
  4293   Inf_binary ~> Inf_insert, Inf_empty, and inf_top_right
  4294   Sup_binary ~> Sup_insert, Sup_empty, and sup_bot_right
  4295   Int_eq_Inter ~> Inf_insert, Inf_empty, and inf_top_right
  4296   Un_eq_Union ~> Sup_insert, Sup_empty, and sup_bot_right
  4297   Inter_def ~> INF_def, image_def
  4298   Union_def ~> SUP_def, image_def
  4299   INT_eq ~> INF_def, and image_def
  4300   UN_eq ~> SUP_def, and image_def
  4301   INF_subset ~> INF_superset_mono [OF _ order_refl]
  4302 
  4303 More consistent and comprehensive names:
  4304 
  4305   INTER_eq_Inter_image ~> INF_def
  4306   UNION_eq_Union_image ~> SUP_def
  4307   INFI_def ~> INF_def
  4308   SUPR_def ~> SUP_def
  4309   INF_leI ~> INF_lower
  4310   INF_leI2 ~> INF_lower2
  4311   le_INFI ~> INF_greatest
  4312   le_SUPI ~> SUP_upper
  4313   le_SUPI2 ~> SUP_upper2
  4314   SUP_leI ~> SUP_least
  4315   INFI_bool_eq ~> INF_bool_eq
  4316   SUPR_bool_eq ~> SUP_bool_eq
  4317   INFI_apply ~> INF_apply
  4318   SUPR_apply ~> SUP_apply
  4319   INTER_def ~> INTER_eq
  4320   UNION_def ~> UNION_eq
  4321 
  4322 INCOMPATIBILITY.
  4323 
  4324 * Renamed theory Complete_Lattice to Complete_Lattices.
  4325 INCOMPATIBILITY.
  4326 
  4327 * Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff,
  4328 INF_image, Inf_insert, INF_top, Inf_top_conv, INF_top_conv, SUP_bot,
  4329 Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image,
  4330 Sup_insert are now declared as [simp].  INCOMPATIBILITY.
  4331 
  4332 * Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff,
  4333 compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem,
  4334 sup_inf_absob, sup_left_idem are now declared as [simp].  Minor
  4335 INCOMPATIBILITY.
  4336 
  4337 * Added syntactic classes "inf" and "sup" for the respective
  4338 constants.  INCOMPATIBILITY: Changes in the argument order of the
  4339 (mostly internal) locale predicates for some derived classes.
  4340 
  4341 * Theorem collections ball_simps and bex_simps do not contain theorems
  4342 referring to UNION any longer; these have been moved to collection
  4343 UN_ball_bex_simps.  INCOMPATIBILITY.
  4344 
  4345 * Theory Archimedean_Field: floor now is defined as parameter of a
  4346 separate type class floor_ceiling.
  4347 
  4348 * Theory Finite_Set: more coherent development of fold_set locales:
  4349 
  4350     locale fun_left_comm ~> locale comp_fun_commute
  4351     locale fun_left_comm_idem ~> locale comp_fun_idem
  4352 
  4353 Both use point-free characterization; interpretation proofs may need
  4354 adjustment.  INCOMPATIBILITY.
  4355 
  4356 * Theory Limits: Type "'a net" has been renamed to "'a filter", in
  4357 accordance with standard mathematical terminology. INCOMPATIBILITY.
  4358 
  4359 * Theory Complex_Main: The locale interpretations for the
  4360 bounded_linear and bounded_bilinear locales have been removed, in
  4361 order to reduce the number of duplicate lemmas. Users must use the
  4362 original names for distributivity theorems, potential INCOMPATIBILITY.
  4363 
  4364   divide.add ~> add_divide_distrib
  4365   divide.diff ~> diff_divide_distrib
  4366   divide.setsum ~> setsum_divide_distrib
  4367   mult.add_right ~> right_distrib
  4368   mult.diff_right ~> right_diff_distrib
  4369   mult_right.setsum ~> setsum_right_distrib
  4370   mult_left.diff ~> left_diff_distrib
  4371 
  4372 * Theory Complex_Main: Several redundant theorems have been removed or
  4373 replaced by more general versions. INCOMPATIBILITY.
  4374 
  4375   real_diff_def ~> minus_real_def
  4376   real_divide_def ~> divide_real_def
  4377   real_less_def ~> less_le
  4378   real_abs_def ~> abs_real_def
  4379   real_sgn_def ~> sgn_real_def
  4380   real_mult_commute ~> mult_commute
  4381   real_mult_assoc ~> mult_assoc
  4382   real_mult_1 ~> mult_1_left
  4383   real_add_mult_distrib ~> left_distrib
  4384   real_zero_not_eq_one ~> zero_neq_one
  4385   real_mult_inverse_left ~> left_inverse
  4386   INVERSE_ZERO ~> inverse_zero
  4387   real_le_refl ~> order_refl
  4388   real_le_antisym ~> order_antisym
  4389   real_le_trans ~> order_trans
  4390   real_le_linear ~> linear
  4391   real_le_eq_diff ~> le_iff_diff_le_0
  4392   real_add_left_mono ~> add_left_mono
  4393   real_mult_order ~> mult_pos_pos
  4394   real_mult_less_mono2 ~> mult_strict_left_mono
  4395   real_of_int_real_of_nat ~> real_of_int_of_nat_eq
  4396   real_0_le_divide_iff ~> zero_le_divide_iff
  4397   realpow_two_disj ~> power2_eq_iff
  4398   real_squared_diff_one_factored ~> square_diff_one_factored
  4399   realpow_two_diff ~> square_diff_square_factored
  4400   reals_complete2 ~> complete_real
  4401   real_sum_squared_expand ~> power2_sum
  4402   exp_ln_eq ~> ln_unique
  4403   expi_add ~> exp_add
  4404   expi_zero ~> exp_zero
  4405   lemma_DERIV_subst ~> DERIV_cong
  4406   LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff
  4407   LIMSEQ_const ~> tendsto_const
  4408   LIMSEQ_norm ~> tendsto_norm
  4409   LIMSEQ_add ~> tendsto_add
  4410   LIMSEQ_minus ~> tendsto_minus
  4411   LIMSEQ_minus_cancel ~> tendsto_minus_cancel
  4412   LIMSEQ_diff ~> tendsto_diff
  4413   bounded_linear.LIMSEQ ~> bounded_linear.tendsto
  4414   bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto
  4415   LIMSEQ_mult ~> tendsto_mult
  4416   LIMSEQ_inverse ~> tendsto_inverse
  4417   LIMSEQ_divide ~> tendsto_divide
  4418   LIMSEQ_pow ~> tendsto_power
  4419   LIMSEQ_setsum ~> tendsto_setsum
  4420   LIMSEQ_setprod ~> tendsto_setprod
  4421   LIMSEQ_norm_zero ~> tendsto_norm_zero_iff
  4422   LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff
  4423   LIMSEQ_imp_rabs ~> tendsto_rabs
  4424   LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]
  4425   LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]
  4426   LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]
  4427   LIMSEQ_Complex ~> tendsto_Complex
  4428   LIM_ident ~> tendsto_ident_at
  4429   LIM_const ~> tendsto_const
  4430   LIM_add ~> tendsto_add
  4431   LIM_add_zero ~> tendsto_add_zero
  4432   LIM_minus ~> tendsto_minus
  4433   LIM_diff ~> tendsto_diff
  4434   LIM_norm ~> tendsto_norm
  4435   LIM_norm_zero ~> tendsto_norm_zero
  4436   LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel
  4437   LIM_norm_zero_iff ~> tendsto_norm_zero_iff
  4438   LIM_rabs ~> tendsto_rabs
  4439   LIM_rabs_zero ~> tendsto_rabs_zero
  4440   LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel
  4441   LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff
  4442   LIM_compose ~> tendsto_compose
  4443   LIM_mult ~> tendsto_mult
  4444   LIM_scaleR ~> tendsto_scaleR
  4445   LIM_of_real ~> tendsto_of_real
  4446   LIM_power ~> tendsto_power
  4447   LIM_inverse ~> tendsto_inverse
  4448   LIM_sgn ~> tendsto_sgn
  4449   isCont_LIM_compose ~> isCont_tendsto_compose
  4450   bounded_linear.LIM ~> bounded_linear.tendsto
  4451   bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero
  4452   bounded_bilinear.LIM ~> bounded_bilinear.tendsto
  4453   bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero
  4454   bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero
  4455   bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero
  4456   LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]
  4457 
  4458 * Theory Complex_Main: The definition of infinite series was
  4459 generalized.  Now it is defined on the type class {topological_space,
  4460 comm_monoid_add}.  Hence it is useable also for extended real numbers.
  4461 
  4462 * Theory Complex_Main: The complex exponential function "expi" is now
  4463 a type-constrained abbreviation for "exp :: complex => complex"; thus
  4464 several polymorphic lemmas about "exp" are now applicable to "expi".
  4465 
  4466 * Code generation:
  4467 
  4468   - Theory Library/Code_Char_ord provides native ordering of
  4469     characters in the target language.
  4470 
  4471   - Commands code_module and code_library are legacy, use export_code
  4472     instead.
  4473 
  4474   - Method "evaluation" is legacy, use method "eval" instead.
  4475 
  4476   - Legacy evaluator "SML" is deactivated by default.  May be
  4477     reactivated by the following theory command:
  4478 
  4479       setup {* Value.add_evaluator ("SML", Codegen.eval_term) *}
  4480 
  4481 * Declare ext [intro] by default.  Rare INCOMPATIBILITY.
  4482 
  4483 * New proof method "induction" that gives induction hypotheses the
  4484 name "IH", thus distinguishing them from further hypotheses that come
  4485 from rule induction.  The latter are still called "hyps".  Method
  4486 "induction" is a thin wrapper around "induct" and follows the same
  4487 syntax.
  4488 
  4489 * Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is
  4490 still available as a legacy feature for some time.
  4491 
  4492 * Nitpick:
  4493   - Added "need" and "total_consts" options.
  4494   - Reintroduced "show_skolems" option by popular demand.
  4495   - Renamed attribute: nitpick_def ~> nitpick_unfold.
  4496     INCOMPATIBILITY.
  4497 
  4498 * Sledgehammer:
  4499   - Use quasi-sound (and efficient) translations by default.
  4500   - Added support for the following provers: E-ToFoF, LEO-II,
  4501     Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax.
  4502   - Automatically preplay and minimize proofs before showing them if
  4503     this can be done within reasonable time.
  4504   - sledgehammer available_provers ~> sledgehammer supported_provers.
  4505     INCOMPATIBILITY.
  4506   - Added "preplay_timeout", "slicing", "type_enc", "sound",
  4507     "max_mono_iters", and "max_new_mono_instances" options.
  4508   - Removed "explicit_apply" and "full_types" options as well as "Full
  4509     Types" Proof General menu item. INCOMPATIBILITY.
  4510 
  4511 * Metis:
  4512   - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.
  4513   - Obsoleted "metisFT" -- use "metis (full_types)" instead.
  4514     INCOMPATIBILITY.
  4515 
  4516 * Command 'try':
  4517   - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and
  4518     "elim:" options. INCOMPATIBILITY.
  4519   - Introduced 'try' that not only runs 'try_methods' but also
  4520     'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'.
  4521 
  4522 * Quickcheck:
  4523   - Added "eval" option to evaluate terms for the found counterexample
  4524     (currently only supported by the default (exhaustive) tester).
  4525   - Added post-processing of terms to obtain readable counterexamples
  4526     (currently only supported by the default (exhaustive) tester).
  4527   - New counterexample generator quickcheck[narrowing] enables
  4528     narrowing-based testing.  Requires the Glasgow Haskell compiler
  4529     with its installation location defined in the Isabelle settings
  4530     environment as ISABELLE_GHC.
  4531   - Removed quickcheck tester "SML" based on the SML code generator
  4532     (formly in HOL/Library).
  4533 
  4534 * Function package: discontinued option "tailrec".  INCOMPATIBILITY,
  4535 use 'partial_function' instead.
  4536 
  4537 * Theory Library/Extended_Reals replaces now the positive extended
  4538 reals found in probability theory. This file is extended by
  4539 Multivariate_Analysis/Extended_Real_Limits.
  4540 
  4541 * Theory Library/Old_Recdef: old 'recdef' package has been moved here,
  4542 from where it must be imported explicitly if it is really required.
  4543 INCOMPATIBILITY.
  4544 
  4545 * Theory Library/Wfrec: well-founded recursion combinator "wfrec" has
  4546 been moved here.  INCOMPATIBILITY.
  4547 
  4548 * Theory Library/Saturated provides type of numbers with saturated
  4549 arithmetic.
  4550 
  4551 * Theory Library/Product_Lattice defines a pointwise ordering for the
  4552 product type 'a * 'b, and provides instance proofs for various order
  4553 and lattice type classes.
  4554 
  4555 * Theory Library/Countable now provides the "countable_datatype" proof
  4556 method for proving "countable" class instances for datatypes.
  4557 
  4558 * Theory Library/Cset_Monad allows do notation for computable sets
  4559 (cset) via the generic monad ad-hoc overloading facility.
  4560 
  4561 * Library: Theories of common data structures are split into theories
  4562 for implementation, an invariant-ensuring type, and connection to an
  4563 abstract type. INCOMPATIBILITY.
  4564 
  4565   - RBT is split into RBT and RBT_Mapping.
  4566   - AssocList is split and renamed into AList and AList_Mapping.
  4567   - DList is split into DList_Impl, DList, and DList_Cset.
  4568   - Cset is split into Cset and List_Cset.
  4569 
  4570 * Theory Library/Nat_Infinity has been renamed to
  4571 Library/Extended_Nat, with name changes of the following types and
  4572 constants:
  4573 
  4574   type inat   ~> type enat
  4575   Fin         ~> enat
  4576   Infty       ~> infinity (overloaded)
  4577   iSuc        ~> eSuc
  4578   the_Fin     ~> the_enat
  4579 
  4580 Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has
  4581 been renamed accordingly. INCOMPATIBILITY.
  4582 
  4583 * Session Multivariate_Analysis: The euclidean_space type class now
  4584 fixes a constant "Basis :: 'a set" consisting of the standard
  4585 orthonormal basis for the type. Users now have the option of
  4586 quantifying over this set instead of using the "basis" function, e.g.
  4587 "ALL x:Basis. P x" vs "ALL i<DIM('a). P (basis i)".
  4588 
  4589 * Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed
  4590 to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants
  4591 "Cart_nth" and "Cart_lambda" have been respectively renamed to
  4592 "vec_nth" and "vec_lambda"; theorems mentioning those names have
  4593 changed to match. Definition theorems for overloaded constants now use
  4594 the standard "foo_vec_def" naming scheme. A few other theorems have
  4595 been renamed as follows (INCOMPATIBILITY):
  4596 
  4597   Cart_eq          ~> vec_eq_iff
  4598   dist_nth_le_cart ~> dist_vec_nth_le
  4599   tendsto_vector   ~> vec_tendstoI
  4600   Cauchy_vector    ~> vec_CauchyI
  4601 
  4602 * Session Multivariate_Analysis: Several duplicate theorems have been
  4603 removed, and other theorems have been renamed or replaced with more
  4604 general versions. INCOMPATIBILITY.
  4605 
  4606   finite_choice ~> finite_set_choice
  4607   eventually_conjI ~> eventually_conj
  4608   eventually_and ~> eventually_conj_iff
  4609   eventually_false ~> eventually_False
  4610   setsum_norm ~> norm_setsum
  4611   Lim_sequentially ~> LIMSEQ_def
  4612   Lim_ident_at ~> LIM_ident
  4613   Lim_const ~> tendsto_const
  4614   Lim_cmul ~> tendsto_scaleR [OF tendsto_const]
  4615   Lim_neg ~> tendsto_minus
  4616   Lim_add ~> tendsto_add
  4617   Lim_sub ~> tendsto_diff
  4618   Lim_mul ~> tendsto_scaleR
  4619   Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]
  4620   Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]
  4621   Lim_linear ~> bounded_linear.tendsto
  4622   Lim_component ~> tendsto_euclidean_component
  4623   Lim_component_cart ~> tendsto_vec_nth
  4624   Lim_inner ~> tendsto_inner [OF tendsto_const]
  4625   dot_lsum ~> inner_setsum_left
  4626   dot_rsum ~> inner_setsum_right
  4627   continuous_cmul ~> continuous_scaleR [OF continuous_const]
  4628   continuous_neg ~> continuous_minus
  4629   continuous_sub ~> continuous_diff
  4630   continuous_vmul ~> continuous_scaleR [OF _ continuous_const]
  4631   continuous_mul ~> continuous_scaleR
  4632   continuous_inv ~> continuous_inverse
  4633   continuous_at_within_inv ~> continuous_at_within_inverse
  4634   continuous_at_inv ~> continuous_at_inverse
  4635   continuous_at_norm ~> continuous_norm [OF continuous_at_id]
  4636   continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id]
  4637   continuous_at_component ~> continuous_component [OF continuous_at_id]
  4638   continuous_on_neg ~> continuous_on_minus
  4639   continuous_on_sub ~> continuous_on_diff
  4640   continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]
  4641   continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const]
  4642   continuous_on_mul ~> continuous_on_scaleR
  4643   continuous_on_mul_real ~> continuous_on_mult
  4644   continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]
  4645   continuous_on_norm ~> continuous_on_norm [OF continuous_on_id]
  4646   continuous_on_inverse ~> continuous_on_inv
  4647   uniformly_continuous_on_neg ~> uniformly_continuous_on_minus
  4648   uniformly_continuous_on_sub ~> uniformly_continuous_on_diff
  4649   subset_interior ~> interior_mono
  4650   subset_closure ~> closure_mono
  4651   closure_univ ~> closure_UNIV
  4652   real_arch_lt ~> reals_Archimedean2
  4653   real_arch ~> reals_Archimedean3
  4654   real_abs_norm ~> abs_norm_cancel
  4655   real_abs_sub_norm ~> norm_triangle_ineq3
  4656   norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2
  4657 
  4658 * Session HOL-Probability:
  4659   - Caratheodory's extension lemma is now proved for ring_of_sets.
  4660   - Infinite products of probability measures are now available.
  4661   - Sigma closure is independent, if the generator is independent
  4662   - Use extended reals instead of positive extended
  4663     reals. INCOMPATIBILITY.
  4664 
  4665 * Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY.
  4666 
  4667   expand_fun_below ~> fun_below_iff
  4668   below_fun_ext ~> fun_belowI
  4669   expand_cfun_eq ~> cfun_eq_iff
  4670   ext_cfun ~> cfun_eqI
  4671   expand_cfun_below ~> cfun_below_iff
  4672   below_cfun_ext ~> cfun_belowI
  4673   monofun_fun_fun ~> fun_belowD
  4674   monofun_fun_arg ~> monofunE
  4675   monofun_lub_fun ~> adm_monofun [THEN admD]
  4676   cont_lub_fun ~> adm_cont [THEN admD]
  4677   cont2cont_Rep_CFun ~> cont2cont_APP
  4678   cont_Rep_CFun_app ~> cont_APP_app
  4679   cont_Rep_CFun_app_app ~> cont_APP_app_app
  4680   cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE]
  4681   cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE]
  4682   contlub_cfun ~> lub_APP [symmetric]
  4683   contlub_LAM ~> lub_LAM [symmetric]
  4684   thelubI ~> lub_eqI
  4685   UU_I ~> bottomI
  4686   lift_distinct1 ~> lift.distinct(1)
  4687   lift_distinct2 ~> lift.distinct(2)
  4688   Def_not_UU ~> lift.distinct(2)
  4689   Def_inject ~> lift.inject
  4690   below_UU_iff ~> below_bottom_iff
  4691   eq_UU_iff ~> eq_bottom_iff
  4692 
  4693 
  4694 *** Document preparation ***
  4695 
  4696 * Antiquotation @{rail} layouts railroad syntax diagrams, see also
  4697 isar-ref manual, both for description and actual application of the
  4698 same.
  4699 
  4700 * Antiquotation @{value} evaluates the given term and presents its
  4701 result.
  4702 
  4703 * Antiquotations: term style "isub" provides ad-hoc conversion of
  4704 variables x1, y23 into subscripted form x\<^isub>1,
  4705 y\<^isub>2\<^isub>3.
  4706 
  4707 * Predefined LaTeX macros for Isabelle symbols \<bind> and \<then>
  4708 (e.g. see ~~/src/HOL/Library/Monad_Syntax.thy).
  4709 
  4710 * Localized \isabellestyle switch can be used within blocks or groups
  4711 like this:
  4712 
  4713   \isabellestyle{it}  %preferred default
  4714   {\isabellestylett @{text "typewriter stuff"}}
  4715 
  4716 * Discontinued special treatment of hard tabulators.  Implicit
  4717 tab-width is now defined as 1.  Potential INCOMPATIBILITY for visual
  4718 layouts.
  4719 
  4720 
  4721 *** ML ***
  4722 
  4723 * The inner syntax of sort/type/term/prop supports inlined YXML
  4724 representations within quoted string tokens.  By encoding logical
  4725 entities via Term_XML (in ML or Scala) concrete syntax can be
  4726 bypassed, which is particularly useful for producing bits of text
  4727 under external program control.
  4728 
  4729 * Antiquotations for ML and document preparation are managed as theory
  4730 data, which requires explicit setup.
  4731 
  4732 * Isabelle_Process.is_active allows tools to check if the official
  4733 process wrapper is running (Isabelle/Scala/jEdit) or the old TTY loop
  4734 (better known as Proof General).
  4735 
  4736 * Structure Proof_Context follows standard naming scheme.  Old
  4737 ProofContext is still available for some time as legacy alias.
  4738 
  4739 * Structure Timing provides various operations for timing; supersedes
  4740 former start_timing/end_timing etc.
  4741 
  4742 * Path.print is the official way to show file-system paths to users
  4743 (including quotes etc.).
  4744 
  4745 * Inner syntax: identifiers in parse trees of generic categories
  4746 "logic", "aprop", "idt" etc. carry position information (disguised as
  4747 type constraints).  Occasional INCOMPATIBILITY with non-compliant
  4748 translations that choke on unexpected type constraints.  Positions can
  4749 be stripped in ML translations via Syntax.strip_positions /
  4750 Syntax.strip_positions_ast, or via the syntax constant
  4751 "_strip_positions" within parse trees.  As last resort, positions can
  4752 be disabled via the configuration option Syntax.positions, which is
  4753 called "syntax_positions" in Isar attribute syntax.
  4754 
  4755 * Discontinued special status of various ML structures that contribute
  4756 to structure Syntax (Ast, Lexicon, Mixfix, Parser, Printer etc.): less
  4757 pervasive content, no inclusion in structure Syntax.  INCOMPATIBILITY,
  4758 refer directly to Ast.Constant, Lexicon.is_identifier,
  4759 Syntax_Trans.mk_binder_tr etc.
  4760 
  4761 * Typed print translation: discontinued show_sorts argument, which is
  4762 already available via context of "advanced" translation.
  4763 
  4764 * Refined PARALLEL_GOALS tactical: degrades gracefully for schematic
  4765 goal states; body tactic needs to address all subgoals uniformly.
  4766 
  4767 * Slightly more special eq_list/eq_set, with shortcut involving
  4768 pointer equality (assumes that eq relation is reflexive).
  4769 
  4770 * Classical tactics use proper Proof.context instead of historic types
  4771 claset/clasimpset.  Old-style declarations like addIs, addEs, addDs
  4772 operate directly on Proof.context.  Raw type claset retains its use as
  4773 snapshot of the classical context, which can be recovered via
  4774 (put_claset HOL_cs) etc.  Type clasimpset has been discontinued.
  4775 INCOMPATIBILITY, classical tactics and derived proof methods require
  4776 proper Proof.context.
  4777 
  4778 
  4779 *** System ***
  4780 
  4781 * Discontinued support for Poly/ML 5.2, which was the last version
  4782 without proper multithreading and TimeLimit implementation.
  4783 
  4784 * Discontinued old lib/scripts/polyml-platform, which has been
  4785 obsolete since Isabelle2009-2.
  4786 
  4787 * Various optional external tools are referenced more robustly and
  4788 uniformly by explicit Isabelle settings as follows:
  4789 
  4790   ISABELLE_CSDP   (formerly CSDP_EXE)
  4791   ISABELLE_GHC    (formerly EXEC_GHC or GHC_PATH)
  4792   ISABELLE_OCAML  (formerly EXEC_OCAML)
  4793   ISABELLE_SWIPL  (formerly EXEC_SWIPL)
  4794   ISABELLE_YAP    (formerly EXEC_YAP)
  4795 
  4796 Note that automated detection from the file-system or search path has
  4797 been discontinued.  INCOMPATIBILITY.
  4798 
  4799 * Scala layer provides JVM method invocation service for static
  4800 methods of type (String)String, see Invoke_Scala.method in ML.  For
  4801 example:
  4802 
  4803   Invoke_Scala.method "java.lang.System.getProperty" "java.home"
  4804 
  4805 Together with YXML.string_of_body/parse_body and XML.Encode/Decode
  4806 this allows to pass structured values between ML and Scala.
  4807 
  4808 * The IsabelleText fonts includes some further glyphs to support the
  4809 Prover IDE.  Potential INCOMPATIBILITY: users who happen to have
  4810 installed a local copy (which is normally *not* required) need to
  4811 delete or update it from ~~/lib/fonts/.
  4812 
  4813 
  4814 
  4815 New in Isabelle2011 (January 2011)
  4816 ----------------------------------
  4817 
  4818 *** General ***
  4819 
  4820 * Experimental Prover IDE based on Isabelle/Scala and jEdit (see
  4821 src/Tools/jEdit).  This also serves as IDE for Isabelle/ML, with
  4822 useful tooltips and hyperlinks produced from its static analysis.  The
  4823 bundled component provides an executable Isabelle tool that can be run
  4824 like this:
  4825 
  4826   Isabelle2011/bin/isabelle jedit
  4827 
  4828 * Significantly improved Isabelle/Isar implementation manual.
  4829 
  4830 * System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
  4831 (and thus refers to something like $HOME/.isabelle/Isabelle2011),
  4832 while the default heap location within that directory lacks that extra
  4833 suffix.  This isolates multiple Isabelle installations from each
  4834 other, avoiding problems with old settings in new versions.
  4835 INCOMPATIBILITY, need to copy/upgrade old user settings manually.
  4836 
  4837 * Source files are always encoded as UTF-8, instead of old-fashioned
  4838 ISO-Latin-1.  INCOMPATIBILITY.  Isabelle LaTeX documents might require
  4839 the following package declarations:
  4840 
  4841   \usepackage[utf8]{inputenc}
  4842   \usepackage{textcomp}
  4843 
  4844 * Explicit treatment of UTF-8 sequences as Isabelle symbols, such that
  4845 a Unicode character is treated as a single symbol, not a sequence of
  4846 non-ASCII bytes as before.  Since Isabelle/ML string literals may
  4847 contain symbols without further backslash escapes, Unicode can now be
  4848 used here as well.  Recall that Symbol.explode in ML provides a
  4849 consistent view on symbols, while raw explode (or String.explode)
  4850 merely give a byte-oriented representation.
  4851 
  4852 * Theory loader: source files are primarily located via the master
  4853 directory of each theory node (where the .thy file itself resides).
  4854 The global load path is still partially available as legacy feature.
  4855 Minor INCOMPATIBILITY due to subtle change in file lookup: use
  4856 explicit paths, relatively to the theory.
  4857 
  4858 * Special treatment of ML file names has been discontinued.
  4859 Historically, optional extensions .ML or .sml were added on demand --
  4860 at the cost of clarity of file dependencies.  Recall that Isabelle/ML
  4861 files exclusively use the .ML extension.  Minor INCOMPATIBILITY.
  4862 
  4863 * Various options that affect pretty printing etc. are now properly
  4864 handled within the context via configuration options, instead of
  4865 unsynchronized references or print modes.  There are both ML Config.T
  4866 entities and Isar declaration attributes to access these.
  4867 
  4868   ML (Config.T)                 Isar (attribute)
  4869 
  4870   eta_contract                  eta_contract
  4871   show_brackets                 show_brackets
  4872   show_sorts                    show_sorts
  4873   show_types                    show_types
  4874   show_question_marks           show_question_marks
  4875   show_consts                   show_consts
  4876   show_abbrevs                  show_abbrevs
  4877 
  4878   Syntax.ast_trace              syntax_ast_trace
  4879   Syntax.ast_stat               syntax_ast_stat
  4880   Syntax.ambiguity_level        syntax_ambiguity_level
  4881 
  4882   Goal_Display.goals_limit      goals_limit
  4883   Goal_Display.show_main_goal   show_main_goal
  4884 
  4885   Method.rule_trace             rule_trace
  4886 
  4887   Thy_Output.display            thy_output_display
  4888   Thy_Output.quotes             thy_output_quotes
  4889   Thy_Output.indent             thy_output_indent
  4890   Thy_Output.source             thy_output_source
  4891   Thy_Output.break              thy_output_break
  4892 
  4893 Note that corresponding "..._default" references in ML may only be
  4894 changed globally at the ROOT session setup, but *not* within a theory.
  4895 The option "show_abbrevs" supersedes the former print mode
  4896 "no_abbrevs" with inverted meaning.
  4897 
  4898 * More systematic naming of some configuration options.
  4899 INCOMPATIBILITY.
  4900 
  4901   trace_simp  ~>  simp_trace
  4902   debug_simp  ~>  simp_debug
  4903 
  4904 * Support for real valued configuration options, using simplistic
  4905 floating-point notation that coincides with the inner syntax for
  4906 float_token.
  4907 
  4908 * Support for real valued preferences (with approximative PGIP type):
  4909 front-ends need to accept "pgint" values in float notation.
  4910 INCOMPATIBILITY.
  4911 
  4912 * The IsabelleText font now includes Cyrillic, Hebrew, Arabic from
  4913 DejaVu Sans.
  4914 
  4915 * Discontinued support for Poly/ML 5.0 and 5.1 versions.
  4916 
  4917 
  4918 *** Pure ***
  4919 
  4920 * Command 'type_synonym' (with single argument) replaces somewhat
  4921 outdated 'types', which is still available as legacy feature for some
  4922 time.
  4923 
  4924 * Command 'nonterminal' (with 'and' separated list of arguments)
  4925 replaces somewhat outdated 'nonterminals'.  INCOMPATIBILITY.
  4926 
  4927 * Command 'notepad' replaces former 'example_proof' for
  4928 experimentation in Isar without any result.  INCOMPATIBILITY.
  4929 
  4930 * Locale interpretation commands 'interpret' and 'sublocale' accept
  4931 lists of equations to map definitions in a locale to appropriate
  4932 entities in the context of the interpretation.  The 'interpretation'
  4933 command already provided this functionality.
  4934 
  4935 * Diagnostic command 'print_dependencies' prints the locale instances
  4936 that would be activated if the specified expression was interpreted in
  4937 the current context.  Variant "print_dependencies!" assumes a context
  4938 without interpretations.
  4939 
  4940 * Diagnostic command 'print_interps' prints interpretations in proofs
  4941 in addition to interpretations in theories.
  4942 
  4943 * Discontinued obsolete 'global' and 'local' commands to manipulate
  4944 the theory name space.  Rare INCOMPATIBILITY.  The ML functions
  4945 Sign.root_path and Sign.local_path may be applied directly where this
  4946 feature is still required for historical reasons.
  4947 
  4948 * Discontinued obsolete 'constdefs' command.  INCOMPATIBILITY, use
  4949 'definition' instead.
  4950 
  4951 * The "prems" fact, which refers to the accidental collection of
  4952 foundational premises in the context, is now explicitly marked as
  4953 legacy feature and will be discontinued soon.  Consider using "assms"
  4954 of the head statement or reference facts by explicit names.
  4955 
  4956 * Document antiquotations @{class} and @{type} print classes and type
  4957 constructors.
  4958 
  4959 * Document antiquotation @{file} checks file/directory entries within
  4960 the local file system.
  4961 
  4962 
  4963 *** HOL ***
  4964 
  4965 * Coercive subtyping: functions can be declared as coercions and type
  4966 inference will add them as necessary upon input of a term.  Theory
  4967 Complex_Main declares real :: nat => real and real :: int => real as
  4968 coercions. A coercion function f is declared like this:
  4969 
  4970   declare [[coercion f]]
  4971 
  4972 To lift coercions through type constructors (e.g. from nat => real to
  4973 nat list => real list), map functions can be declared, e.g.
  4974 
  4975   declare [[coercion_map map]]
  4976 
  4977 Currently coercion inference is activated only in theories including
  4978 real numbers, i.e. descendants of Complex_Main.  This is controlled by
  4979 the configuration option "coercion_enabled", e.g. it can be enabled in
  4980 other theories like this:
  4981 
  4982   declare [[coercion_enabled]]
  4983 
  4984 * Command 'partial_function' provides basic support for recursive
  4985 function definitions over complete partial orders.  Concrete instances
  4986 are provided for i) the option type, ii) tail recursion on arbitrary
  4987 types, and iii) the heap monad of Imperative_HOL.  See
  4988 src/HOL/ex/Fundefs.thy and src/HOL/Imperative_HOL/ex/Linked_Lists.thy
  4989 for examples.
  4990 
  4991 * Function package: f.psimps rules are no longer implicitly declared
  4992 as [simp].  INCOMPATIBILITY.
  4993 
  4994 * Datatype package: theorems generated for executable equality (class
  4995 "eq") carry proper names and are treated as default code equations.
  4996 
  4997 * Inductive package: now offers command 'inductive_simps' to
  4998 automatically derive instantiated and simplified equations for
  4999 inductive predicates, similar to 'inductive_cases'.
  5000 
  5001 * Command 'enriched_type' allows to register properties of the
  5002 functorial structure of types.
  5003 
  5004 * Improved infrastructure for term evaluation using code generator
  5005 techniques, in particular static evaluation conversions.
  5006 
  5007 * Code generator: Scala (2.8 or higher) has been added to the target
  5008 languages.
  5009 
  5010 * Code generator: globbing constant expressions "*" and "Theory.*"
  5011 have been replaced by the more idiomatic "_" and "Theory._".
  5012 INCOMPATIBILITY.
  5013 
  5014 * Code generator: export_code without explicit file declaration prints
  5015 to standard output.  INCOMPATIBILITY.
  5016 
  5017 * Code generator: do not print function definitions for case
  5018 combinators any longer.
  5019 
  5020 * Code generator: simplification with rules determined with
  5021 src/Tools/Code/code_simp.ML and method "code_simp".
  5022 
  5023 * Code generator for records: more idiomatic representation of record
  5024 types.  Warning: records are not covered by ancient SML code
  5025 generation any longer.  INCOMPATIBILITY.  In cases of need, a suitable
  5026 rep_datatype declaration helps to succeed then:
  5027 
  5028   record 'a foo = ...
  5029   ...
  5030   rep_datatype foo_ext ...
  5031 
  5032 * Records: logical foundation type for records does not carry a
  5033 '_type' suffix any longer (obsolete due to authentic syntax).
  5034 INCOMPATIBILITY.
  5035 
  5036 * Quickcheck now by default uses exhaustive testing instead of random
  5037 testing.  Random testing can be invoked by "quickcheck [random]",
  5038 exhaustive testing by "quickcheck [exhaustive]".
  5039 
  5040 * Quickcheck instantiates polymorphic types with small finite
  5041 datatypes by default. This enables a simple execution mechanism to
  5042 handle quantifiers and function equality over the finite datatypes.
  5043 
  5044 * Quickcheck random generator has been renamed from "code" to
  5045 "random".  INCOMPATIBILITY.
  5046 
  5047 * Quickcheck now has a configurable time limit which is set to 30
  5048 seconds by default. This can be changed by adding [timeout = n] to the
  5049 quickcheck command. The time limit for Auto Quickcheck is still set
  5050 independently.
  5051 
  5052 * Quickcheck in locales considers interpretations of that locale for
  5053 counter example search.
  5054 
  5055 * Sledgehammer:
  5056   - Added "smt" and "remote_smt" provers based on the "smt" proof
  5057     method. See the Sledgehammer manual for details ("isabelle doc
  5058     sledgehammer").
  5059   - Renamed commands:
  5060     sledgehammer atp_info ~> sledgehammer running_provers
  5061     sledgehammer atp_kill ~> sledgehammer kill_provers
  5062     sledgehammer available_atps ~> sledgehammer available_provers
  5063     INCOMPATIBILITY.
  5064   - Renamed options:
  5065     sledgehammer [atps = ...] ~> sledgehammer [provers = ...]
  5066     sledgehammer [atp = ...] ~> sledgehammer [prover = ...]
  5067     sledgehammer [timeout = 77 s] ~> sledgehammer [timeout = 77]
  5068     (and "ms" and "min" are no longer supported)
  5069     INCOMPATIBILITY.
  5070 
  5071 * Nitpick:
  5072   - Renamed options:
  5073     nitpick [timeout = 77 s] ~> nitpick [timeout = 77]
  5074     nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]
  5075     INCOMPATIBILITY.
  5076   - Added support for partial quotient types.
  5077   - Added local versions of the "Nitpick.register_xxx" functions.
  5078   - Added "whack" option.
  5079   - Allow registration of quotient types as codatatypes.
  5080   - Improved "merge_type_vars" option to merge more types.
  5081   - Removed unsound "fast_descrs" option.
  5082   - Added custom symmetry breaking for datatypes, making it possible to reach
  5083     higher cardinalities.
  5084   - Prevent the expansion of too large definitions.
  5085 
  5086 * Proof methods "metis" and "meson" now have configuration options
  5087 "meson_trace", "metis_trace", and "metis_verbose" that can be enabled
  5088 to diagnose these tools. E.g.
  5089 
  5090     using [[metis_trace = true]]
  5091 
  5092 * Auto Solve: Renamed "Auto Solve Direct".  The tool is now available
  5093 manually as command 'solve_direct'.
  5094 
  5095 * The default SMT solver Z3 must be enabled explicitly (due to
  5096 licensing issues) by setting the environment variable
  5097 Z3_NON_COMMERCIAL in etc/settings of the component, for example.  For
  5098 commercial applications, the SMT solver CVC3 is provided as fall-back;
  5099 changing the SMT solver is done via the configuration option
  5100 "smt_solver".
  5101 
  5102 * Remote SMT solvers need to be referred to by the "remote_" prefix,
  5103 i.e. "remote_cvc3" and "remote_z3".
  5104 
  5105 * Added basic SMT support for datatypes, records, and typedefs using
  5106 the oracle mode (no proofs).  Direct support of pairs has been dropped
  5107 in exchange (pass theorems fst_conv snd_conv pair_collapse to the SMT
  5108 support for a similar behavior).  Minor INCOMPATIBILITY.
  5109 
  5110 * Changed SMT configuration options:
  5111   - Renamed:
  5112     z3_proofs ~> smt_oracle (with inverted meaning)
  5113     z3_trace_assms ~> smt_trace_used_facts
  5114     INCOMPATIBILITY.
  5115   - Added:
  5116     smt_verbose
  5117     smt_random_seed
  5118     smt_datatypes
  5119     smt_infer_triggers
  5120     smt_monomorph_limit
  5121     cvc3_options
  5122     remote_cvc3_options
  5123     remote_z3_options
  5124     yices_options
  5125 
  5126 * Boogie output files (.b2i files) need to be declared in the theory
  5127 header.
  5128 
  5129 * Simplification procedure "list_to_set_comprehension" rewrites list
  5130 comprehensions applied to List.set to set comprehensions.  Occasional
  5131 INCOMPATIBILITY, may be deactivated like this:
  5132 
  5133   declare [[simproc del: list_to_set_comprehension]]
  5134 
  5135 * Removed old version of primrec package.  INCOMPATIBILITY.
  5136 
  5137 * Removed simplifier congruence rule of "prod_case", as has for long
  5138 been the case with "split".  INCOMPATIBILITY.
  5139 
  5140 * String.literal is a type, but not a datatype.  INCOMPATIBILITY.
  5141 
  5142 * Removed [split_format ... and ... and ...] version of
  5143 [split_format].  Potential INCOMPATIBILITY.
  5144 
  5145 * Predicate "sorted" now defined inductively, with nice induction
  5146 rules.  INCOMPATIBILITY: former sorted.simps now named sorted_simps.
  5147 
  5148 * Constant "contents" renamed to "the_elem", to free the generic name
  5149 contents for other uses.  INCOMPATIBILITY.
  5150 
  5151 * Renamed class eq and constant eq (for code generation) to class
  5152 equal and constant equal, plus renaming of related facts and various
  5153 tuning.  INCOMPATIBILITY.
  5154 
  5155 * Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.
  5156 
  5157 * Removed output syntax "'a ~=> 'b" for "'a => 'b option".
  5158 INCOMPATIBILITY.
  5159 
  5160 * Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to
  5161 avoid confusion with finite sets.  INCOMPATIBILITY.
  5162 
  5163 * Abandoned locales equiv, congruent and congruent2 for equivalence
  5164 relations.  INCOMPATIBILITY: use equivI rather than equiv_intro (same
  5165 for congruent(2)).
  5166 
  5167 * Some previously unqualified names have been qualified:
  5168 
  5169   types
  5170     bool ~> HOL.bool
  5171     nat ~> Nat.nat
  5172 
  5173   constants
  5174     Trueprop ~> HOL.Trueprop
  5175     True ~> HOL.True
  5176     False ~> HOL.False
  5177     op & ~> HOL.conj
  5178     op | ~> HOL.disj
  5179     op --> ~> HOL.implies
  5180     op = ~> HOL.eq
  5181     Not ~> HOL.Not
  5182     The ~> HOL.The
  5183     All ~> HOL.All
  5184     Ex ~> HOL.Ex
  5185     Ex1 ~> HOL.Ex1
  5186     Let ~> HOL.Let
  5187     If ~> HOL.If
  5188     Ball ~> Set.Ball
  5189     Bex ~> Set.Bex
  5190     Suc ~> Nat.Suc
  5191     Pair ~> Product_Type.Pair
  5192     fst ~> Product_Type.fst
  5193     snd ~> Product_Type.snd
  5194     curry ~> Product_Type.curry
  5195     op : ~> Set.member
  5196     Collect ~> Set.Collect
  5197 
  5198 INCOMPATIBILITY.
  5199 
  5200 * More canonical naming convention for some fundamental definitions:
  5201 
  5202     bot_bool_eq ~> bot_bool_def
  5203     top_bool_eq ~> top_bool_def
  5204     inf_bool_eq ~> inf_bool_def
  5205     sup_bool_eq ~> sup_bool_def
  5206     bot_fun_eq  ~> bot_fun_def
  5207     top_fun_eq  ~> top_fun_def
  5208     inf_fun_eq  ~> inf_fun_def
  5209     sup_fun_eq  ~> sup_fun_def
  5210 
  5211 INCOMPATIBILITY.
  5212 
  5213 * More stylized fact names:
  5214 
  5215   expand_fun_eq ~> fun_eq_iff
  5216   expand_set_eq ~> set_eq_iff
  5217   set_ext       ~> set_eqI
  5218   nat_number    ~> eval_nat_numeral
  5219 
  5220 INCOMPATIBILITY.
  5221 
  5222 * Refactoring of code-generation specific operations in theory List:
  5223 
  5224   constants
  5225     null ~> List.null
  5226 
  5227   facts
  5228     mem_iff ~> member_def
  5229     null_empty ~> null_def
  5230 
  5231 INCOMPATIBILITY.  Note that these were not supposed to be used
  5232 regularly unless for striking reasons; their main purpose was code
  5233 generation.
  5234 
  5235 Various operations from the Haskell prelude are used for generating
  5236 Haskell code.
  5237 
  5238 * Term "bij f" is now an abbreviation of "bij_betw f UNIV UNIV".  Term
  5239 "surj f" is now an abbreviation of "range f = UNIV".  The theorems
  5240 bij_def and surj_def are unchanged.  INCOMPATIBILITY.
  5241 
  5242 * Abolished some non-alphabetic type names: "prod" and "sum" replace
  5243 "*" and "+" respectively.  INCOMPATIBILITY.
  5244 
  5245 * Name "Plus" of disjoint sum operator "<+>" is now hidden.  Write
  5246 "Sum_Type.Plus" instead.
  5247 
  5248 * Constant "split" has been merged with constant "prod_case"; names of
  5249 ML functions, facts etc. involving split have been retained so far,
  5250 though.  INCOMPATIBILITY.
  5251 
  5252 * Dropped old infix syntax "_ mem _" for List.member; use "_ : set _"
  5253 instead.  INCOMPATIBILITY.
  5254 
  5255 * Removed lemma "Option.is_none_none" which duplicates "is_none_def".
  5256 INCOMPATIBILITY.
  5257 
  5258 * Former theory Library/Enum is now part of the HOL-Main image.
  5259 INCOMPATIBILITY: all constants of the Enum theory now have to be
  5260 referred to by its qualified name.
  5261 
  5262   enum    ~>  Enum.enum
  5263   nlists  ~>  Enum.nlists
  5264   product ~>  Enum.product
  5265 
  5266 * Theory Library/Monad_Syntax provides do-syntax for monad types.
  5267 Syntax in Library/State_Monad has been changed to avoid ambiguities.
  5268 INCOMPATIBILITY.
  5269 
  5270 * Theory Library/SetsAndFunctions has been split into
  5271 Library/Function_Algebras and Library/Set_Algebras; canonical names
  5272 for instance definitions for functions; various improvements.
  5273 INCOMPATIBILITY.
  5274 
  5275 * Theory Library/Multiset provides stable quicksort implementation of
  5276 sort_key.
  5277 
  5278 * Theory Library/Multiset: renamed empty_idemp ~> empty_neutral.
  5279 INCOMPATIBILITY.
  5280 
  5281 * Session Multivariate_Analysis: introduced a type class for euclidean
  5282 space.  Most theorems are now stated in terms of euclidean spaces
  5283 instead of finite cartesian products.
  5284 
  5285   types
  5286     real ^ 'n ~>  'a::real_vector
  5287               ~>  'a::euclidean_space
  5288               ~>  'a::ordered_euclidean_space
  5289         (depends on your needs)
  5290 
  5291   constants
  5292      _ $ _        ~> _ $$ _
  5293      \<chi> x. _  ~> \<chi>\<chi> x. _
  5294      CARD('n)     ~> DIM('a)
  5295 
  5296 Also note that the indices are now natural numbers and not from some
  5297 finite type. Finite cartesian products of euclidean spaces, products
  5298 of euclidean spaces the real and complex numbers are instantiated to
  5299 be euclidean_spaces.  INCOMPATIBILITY.
  5300 
  5301 * Session Probability: introduced pextreal as positive extended real
  5302 numbers.  Use pextreal as value for measures.  Introduce the
  5303 Radon-Nikodym derivative, product spaces and Fubini's theorem for
  5304 arbitrary sigma finite measures.  Introduces Lebesgue measure based on
  5305 the integral in Multivariate Analysis.  INCOMPATIBILITY.
  5306 
  5307 * Session Imperative_HOL: revamped, corrected dozens of inadequacies.
  5308 INCOMPATIBILITY.
  5309 
  5310 * Session SPARK (with image HOL-SPARK) provides commands to load and
  5311 prove verification conditions generated by the SPARK Ada program
  5312 verifier.  See also src/HOL/SPARK and src/HOL/SPARK/Examples.
  5313 
  5314 
  5315 *** HOL-Algebra ***
  5316 
  5317 * Theorems for additive ring operations (locale abelian_monoid and
  5318 descendants) are generated by interpretation from their multiplicative
  5319 counterparts.  Names (in particular theorem names) have the mandatory
  5320 qualifier 'add'.  Previous theorem names are redeclared for
  5321 compatibility.
  5322 
  5323 * Structure "int_ring" is now an abbreviation (previously a
  5324 definition).  This fits more natural with advanced interpretations.
  5325 
  5326 
  5327 *** HOLCF ***
  5328 
  5329 * The domain package now runs in definitional mode by default: The
  5330 former command 'new_domain' is now called 'domain'.  To use the domain
  5331 package in its original axiomatic mode, use 'domain (unsafe)'.
  5332 INCOMPATIBILITY.
  5333 
  5334 * The new class "domain" is now the default sort.  Class "predomain"
  5335 is an unpointed version of "domain". Theories can be updated by
  5336 replacing sort annotations as shown below.  INCOMPATIBILITY.
  5337 
  5338   'a::type ~> 'a::countable
  5339   'a::cpo  ~> 'a::predomain
  5340   'a::pcpo ~> 'a::domain
  5341 
  5342 * The old type class "rep" has been superseded by class "domain".
  5343 Accordingly, users of the definitional package must remove any
  5344 "default_sort rep" declarations.  INCOMPATIBILITY.
  5345 
  5346 * The domain package (definitional mode) now supports unpointed
  5347 predomain argument types, as long as they are marked 'lazy'. (Strict
  5348 arguments must be in class "domain".) For example, the following
  5349 domain definition now works:
  5350 
  5351   domain natlist = nil | cons (lazy "nat discr") (lazy "natlist")
  5352 
  5353 * Theory HOLCF/Library/HOL_Cpo provides cpo and predomain class
  5354 instances for types from main HOL: bool, nat, int, char, 'a + 'b,
  5355 'a option, and 'a list.  Additionally, it configures fixrec and the
  5356 domain package to work with these types.  For example:
  5357 
  5358   fixrec isInl :: "('a + 'b) u -> tr"
  5359     where "isInl$(up$(Inl x)) = TT" | "isInl$(up$(Inr y)) = FF"
  5360 
  5361   domain V = VFun (lazy "V -> V") | VCon (lazy "nat") (lazy "V list")
  5362 
  5363 * The "(permissive)" option of fixrec has been replaced with a
  5364 per-equation "(unchecked)" option. See
  5365 src/HOL/HOLCF/Tutorial/Fixrec_ex.thy for examples. INCOMPATIBILITY.
  5366 
  5367 * The "bifinite" class no longer fixes a constant "approx"; the class
  5368 now just asserts that such a function exists.  INCOMPATIBILITY.
  5369 
  5370 * Former type "alg_defl" has been renamed to "defl".  HOLCF no longer
  5371 defines an embedding of type 'a defl into udom by default; instances
  5372 of "bifinite" and "domain" classes are available in
  5373 src/HOL/HOLCF/Library/Defl_Bifinite.thy.
  5374 
  5375 * The syntax "REP('a)" has been replaced with "DEFL('a)".
  5376 
  5377 * The predicate "directed" has been removed.  INCOMPATIBILITY.
  5378 
  5379 * The type class "finite_po" has been removed.  INCOMPATIBILITY.
  5380 
  5381 * The function "cprod_map" has been renamed to "prod_map".
  5382 INCOMPATIBILITY.
  5383 
  5384 * The monadic bind operator on each powerdomain has new binder syntax
  5385 similar to sets, e.g. "\<Union>\<sharp>x\<in>xs. t" represents
  5386 "upper_bind\<cdot>xs\<cdot>(\<Lambda> x. t)".
  5387 
  5388 * The infix syntax for binary union on each powerdomain has changed
  5389 from e.g. "+\<sharp>" to "\<union>\<sharp>", for consistency with set
  5390 syntax.  INCOMPATIBILITY.
  5391 
  5392 * The constant "UU" has been renamed to "bottom".  The syntax "UU" is
  5393 still supported as an input translation.
  5394 
  5395 * Renamed some theorems (the original names are also still available).
  5396 
  5397   expand_fun_below   ~> fun_below_iff
  5398   below_fun_ext      ~> fun_belowI
  5399   expand_cfun_eq     ~> cfun_eq_iff
  5400   ext_cfun           ~> cfun_eqI
  5401   expand_cfun_below  ~> cfun_below_iff
  5402   below_cfun_ext     ~> cfun_belowI
  5403   cont2cont_Rep_CFun ~> cont2cont_APP
  5404 
  5405 * The Abs and Rep functions for various types have changed names.
  5406 Related theorem names have also changed to match. INCOMPATIBILITY.
  5407 
  5408   Rep_CFun  ~> Rep_cfun
  5409   Abs_CFun  ~> Abs_cfun
  5410   Rep_Sprod ~> Rep_sprod
  5411   Abs_Sprod ~> Abs_sprod
  5412   Rep_Ssum  ~> Rep_ssum
  5413   Abs_Ssum  ~> Abs_ssum
  5414 
  5415 * Lemmas with names of the form *_defined_iff or *_strict_iff have
  5416 been renamed to *_bottom_iff.  INCOMPATIBILITY.
  5417 
  5418 * Various changes to bisimulation/coinduction with domain package:
  5419 
  5420   - Definitions of "bisim" constants no longer mention definedness.
  5421   - With mutual recursion, "bisim" predicate is now curried.
  5422   - With mutual recursion, each type gets a separate coind theorem.
  5423   - Variable names in bisim_def and coinduct rules have changed.
  5424 
  5425 INCOMPATIBILITY.
  5426 
  5427 * Case combinators generated by the domain package for type "foo" are
  5428 now named "foo_case" instead of "foo_when".  INCOMPATIBILITY.
  5429 
  5430 * Several theorems have been renamed to more accurately reflect the
  5431 names of constants and types involved.  INCOMPATIBILITY.
  5432 
  5433   thelub_const    ~> lub_const
  5434   lub_const       ~> is_lub_const
  5435   thelubI         ~> lub_eqI
  5436   is_lub_lub      ~> is_lubD2
  5437   lubI            ~> is_lub_lub
  5438   unique_lub      ~> is_lub_unique
  5439   is_ub_lub       ~> is_lub_rangeD1
  5440   lub_bin_chain   ~> is_lub_bin_chain
  5441   lub_fun         ~> is_lub_fun
  5442   thelub_fun      ~> lub_fun
  5443   thelub_cfun     ~> lub_cfun
  5444   thelub_Pair     ~> lub_Pair
  5445   lub_cprod       ~> is_lub_prod
  5446   thelub_cprod    ~> lub_prod
  5447   minimal_cprod   ~> minimal_prod
  5448   inst_cprod_pcpo ~> inst_prod_pcpo
  5449   UU_I            ~> bottomI
  5450   compact_UU      ~> compact_bottom
  5451   deflation_UU    ~> deflation_bottom
  5452   finite_deflation_UU ~> finite_deflation_bottom
  5453 
  5454 * Many legacy theorem names have been discontinued.  INCOMPATIBILITY.
  5455 
  5456   sq_ord_less_eq_trans ~> below_eq_trans
  5457   sq_ord_eq_less_trans ~> eq_below_trans
  5458   refl_less            ~> below_refl
  5459   trans_less           ~> below_trans
  5460   antisym_less         ~> below_antisym
  5461   antisym_less_inverse ~> po_eq_conv [THEN iffD1]
  5462   box_less             ~> box_below
  5463   rev_trans_less       ~> rev_below_trans
  5464   not_less2not_eq      ~> not_below2not_eq
  5465   less_UU_iff          ~> below_UU_iff
  5466   flat_less_iff        ~> flat_below_iff
  5467   adm_less             ~> adm_below
  5468   adm_not_less         ~> adm_not_below
  5469   adm_compact_not_less ~> adm_compact_not_below
  5470   less_fun_def         ~> below_fun_def
  5471   expand_fun_less      ~> fun_below_iff
  5472   less_fun_ext         ~> fun_belowI
  5473   less_discr_def       ~> below_discr_def
  5474   discr_less_eq        ~> discr_below_eq
  5475   less_unit_def        ~> below_unit_def
  5476   less_cprod_def       ~> below_prod_def
  5477   prod_lessI           ~> prod_belowI
  5478   Pair_less_iff        ~> Pair_below_iff
  5479   fst_less_iff         ~> fst_below_iff
  5480   snd_less_iff         ~> snd_below_iff
  5481   expand_cfun_less     ~> cfun_below_iff
  5482   less_cfun_ext        ~> cfun_belowI
  5483   injection_less       ~> injection_below
  5484   less_up_def          ~> below_up_def
  5485   not_Iup_less         ~> not_Iup_below
  5486   Iup_less             ~> Iup_below
  5487   up_less              ~> up_below
  5488   Def_inject_less_eq   ~> Def_below_Def
  5489   Def_less_is_eq       ~> Def_below_iff
  5490   spair_less_iff       ~> spair_below_iff
  5491   less_sprod           ~> below_sprod
  5492   spair_less           ~> spair_below
  5493   sfst_less_iff        ~> sfst_below_iff
  5494   ssnd_less_iff        ~> ssnd_below_iff
  5495   fix_least_less       ~> fix_least_below
  5496   dist_less_one        ~> dist_below_one
  5497   less_ONE             ~> below_ONE
  5498   ONE_less_iff         ~> ONE_below_iff
  5499   less_sinlD           ~> below_sinlD
  5500   less_sinrD           ~> below_sinrD
  5501 
  5502 
  5503 *** FOL and ZF ***
  5504 
  5505 * All constant names are now qualified internally and use proper
  5506 identifiers, e.g. "IFOL.eq" instead of "op =".  INCOMPATIBILITY.
  5507 
  5508 
  5509 *** ML ***
  5510 
  5511 * Antiquotation @{assert} inlines a function bool -> unit that raises
  5512 Fail if the argument is false.  Due to inlining the source position of
  5513 failed assertions is included in the error output.
  5514 
  5515 * Discontinued antiquotation @{theory_ref}, which is obsolete since ML
  5516 text is in practice always evaluated with a stable theory checkpoint.
  5517 Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.
  5518 
  5519 * Antiquotation @{theory A} refers to theory A from the ancestry of
  5520 the current context, not any accidental theory loader state as before.
  5521 Potential INCOMPATIBILITY, subtle change in semantics.
  5522 
  5523 * Syntax.pretty_priority (default 0) configures the required priority
  5524 of pretty-printed output and thus affects insertion of parentheses.
  5525 
  5526 * Syntax.default_root (default "any") configures the inner syntax
  5527 category (nonterminal symbol) for parsing of terms.
  5528 
  5529 * Former exception Library.UnequalLengths now coincides with
  5530 ListPair.UnequalLengths.
  5531 
  5532 * Renamed structure MetaSimplifier to Raw_Simplifier.  Note that the
  5533 main functionality is provided by structure Simplifier.
  5534 
  5535 * Renamed raw "explode" function to "raw_explode" to emphasize its
  5536 meaning.  Note that internally to Isabelle, Symbol.explode is used in
  5537 almost all situations.
  5538 
  5539 * Discontinued obsolete function sys_error and exception SYS_ERROR.
  5540 See implementation manual for further details on exceptions in
  5541 Isabelle/ML.
  5542 
  5543 * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
  5544 meaning.
  5545 
  5546 * Renamed structure PureThy to Pure_Thy and moved most of its
  5547 operations to structure Global_Theory, to emphasize that this is
  5548 rarely-used global-only stuff.
  5549 
  5550 * Discontinued Output.debug.  Minor INCOMPATIBILITY, use plain writeln
  5551 instead (or tracing for high-volume output).
  5552 
  5553 * Configuration option show_question_marks only affects regular pretty
  5554 printing of types and terms, not raw Term.string_of_vname.
  5555 
  5556 * ML_Context.thm and ML_Context.thms are no longer pervasive.  Rare
  5557 INCOMPATIBILITY, superseded by static antiquotations @{thm} and
  5558 @{thms} for most purposes.
  5559 
  5560 * ML structure Unsynchronized is never opened, not even in Isar
  5561 interaction mode as before.  Old Unsynchronized.set etc. have been
  5562 discontinued -- use plain := instead.  This should be *rare* anyway,
  5563 since modern tools always work via official context data, notably
  5564 configuration options.
  5565 
  5566 * Parallel and asynchronous execution requires special care concerning
  5567 interrupts.  Structure Exn provides some convenience functions that
  5568 avoid working directly with raw Interrupt.  User code must not absorb
  5569 interrupts -- intermediate handling (for cleanup etc.) needs to be
  5570 followed by re-raising of the original exception.  Another common
  5571 source of mistakes are "handle _" patterns, which make the meaning of
  5572 the program subject to physical effects of the environment.
  5573 
  5574 
  5575 
  5576 New in Isabelle2009-2 (June 2010)
  5577 ---------------------------------
  5578 
  5579 *** General ***
  5580 
  5581 * Authentic syntax for *all* logical entities (type classes, type
  5582 constructors, term constants): provides simple and robust
  5583 correspondence between formal entities and concrete syntax.  Within
  5584 the parse tree / AST representations, "constants" are decorated by
  5585 their category (class, type, const) and spelled out explicitly with
  5586 their full internal name.
  5587 
  5588 Substantial INCOMPATIBILITY concerning low-level syntax declarations
  5589 and translations (translation rules and translation functions in ML).
  5590 Some hints on upgrading:
  5591 
  5592   - Many existing uses of 'syntax' and 'translations' can be replaced
  5593     by more modern 'type_notation', 'notation' and 'abbreviation',
  5594     which are independent of this issue.
  5595 
  5596   - 'translations' require markup within the AST; the term syntax
  5597     provides the following special forms:
  5598 
  5599       CONST c   -- produces syntax version of constant c from context
  5600       XCONST c  -- literally c, checked as constant from context
  5601       c         -- literally c, if declared by 'syntax'
  5602 
  5603     Plain identifiers are treated as AST variables -- occasionally the
  5604     system indicates accidental variables via the error "rhs contains
  5605     extra variables".
  5606 
  5607     Type classes and type constructors are marked according to their
  5608     concrete syntax.  Some old translations rules need to be written
  5609     for the "type" category, using type constructor application
  5610     instead of pseudo-term application of the default category
  5611     "logic".
  5612 
  5613   - 'parse_translation' etc. in ML may use the following
  5614     antiquotations:
  5615 
  5616       @{class_syntax c}   -- type class c within parse tree / AST
  5617       @{term_syntax c}    -- type constructor c within parse tree / AST
  5618       @{const_syntax c}   -- ML version of "CONST c" above
  5619       @{syntax_const c}   -- literally c (checked wrt. 'syntax' declarations)
  5620 
  5621   - Literal types within 'typed_print_translations', i.e. those *not*
  5622     represented as pseudo-terms are represented verbatim.  Use @{class
  5623     c} or @{type_name c} here instead of the above syntax
  5624     antiquotations.
  5625 
  5626 Note that old non-authentic syntax was based on unqualified base
  5627 names, so all of the above "constant" names would coincide.  Recall
  5628 that 'print_syntax' and ML_command "set Syntax.trace_ast" help to
  5629 diagnose syntax problems.
  5630 
  5631 * Type constructors admit general mixfix syntax, not just infix.
  5632 
  5633 * Concrete syntax may be attached to local entities without a proof
  5634 body, too.  This works via regular mixfix annotations for 'fix',
  5635 'def', 'obtain' etc. or via the explicit 'write' command, which is
  5636 similar to the 'notation' command in theory specifications.
  5637 
  5638 * Discontinued unnamed infix syntax (legacy feature for many years) --
  5639 need to specify constant name and syntax separately.  Internal ML
  5640 datatype constructors have been renamed from InfixName to Infix etc.
  5641 Minor INCOMPATIBILITY.
  5642 
  5643 * Schematic theorem statements need to be explicitly markup as such,
  5644 via commands 'schematic_lemma', 'schematic_theorem',
  5645 'schematic_corollary'.  Thus the relevance of the proof is made
  5646 syntactically clear, which impacts performance in a parallel or
  5647 asynchronous interactive environment.  Minor INCOMPATIBILITY.
  5648 
  5649 * Use of cumulative prems via "!" in some proof methods has been
  5650 discontinued (old legacy feature).
  5651 
  5652 * References 'trace_simp' and 'debug_simp' have been replaced by
  5653 configuration options stored in the context. Enabling tracing (the
  5654 case of debugging is similar) in proofs works via
  5655 
  5656   using [[trace_simp = true]]
  5657 
  5658 Tracing is then active for all invocations of the simplifier in
  5659 subsequent goal refinement steps. Tracing may also still be enabled or
  5660 disabled via the ProofGeneral settings menu.
  5661 
  5662 * Separate commands 'hide_class', 'hide_type', 'hide_const',
  5663 'hide_fact' replace the former 'hide' KIND command.  Minor
  5664 INCOMPATIBILITY.
  5665 
  5666 * Improved parallelism of proof term normalization: usedir -p2 -q0 is
  5667 more efficient than combinations with -q1 or -q2.
  5668 
  5669 
  5670 *** Pure ***
  5671 
  5672 * Proofterms record type-class reasoning explicitly, using the
  5673 "unconstrain" operation internally.  This eliminates all sort
  5674 constraints from a theorem and proof, introducing explicit
  5675 OFCLASS-premises.  On the proof term level, this operation is
  5676 automatically applied at theorem boundaries, such that closed proofs
  5677 are always free of sort constraints.  INCOMPATIBILITY for tools that
  5678 inspect proof terms.
  5679 
  5680 * Local theory specifications may depend on extra type variables that
  5681 are not present in the result type -- arguments TYPE('a) :: 'a itself
  5682 are added internally.  For example:
  5683 
  5684   definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
  5685 
  5686 * Predicates of locales introduced by classes carry a mandatory
  5687 "class" prefix.  INCOMPATIBILITY.
  5688 
  5689 * Vacuous class specifications observe default sort.  INCOMPATIBILITY.
  5690 
  5691 * Old 'axclass' command has been discontinued.  INCOMPATIBILITY, use
  5692 'class' instead.
  5693 
  5694 * Command 'code_reflect' allows to incorporate generated ML code into
  5695 runtime environment; replaces immature code_datatype antiquotation.
  5696 INCOMPATIBILITY.
  5697 
  5698 * Code generator: simple concept for abstract datatypes obeying
  5699 invariants.
  5700 
  5701 * Code generator: details of internal data cache have no impact on the
  5702 user space functionality any longer.
  5703 
  5704 * Methods "unfold_locales" and "intro_locales" ignore non-locale
  5705 subgoals.  This is more appropriate for interpretations with 'where'.
  5706 INCOMPATIBILITY.
  5707 
  5708 * Command 'example_proof' opens an empty proof body.  This allows to
  5709 experiment with Isar, without producing any persistent result.
  5710 
  5711 * Commands 'type_notation' and 'no_type_notation' declare type syntax
  5712 within a local theory context, with explicit checking of the
  5713 constructors involved (in contrast to the raw 'syntax' versions).
  5714 
  5715 * Commands 'types' and 'typedecl' now work within a local theory
  5716 context -- without introducing dependencies on parameters or
  5717 assumptions, which is not possible in Isabelle/Pure.
  5718 
  5719 * Command 'defaultsort' has been renamed to 'default_sort', it works
  5720 within a local theory context.  Minor INCOMPATIBILITY.
  5721 
  5722 
  5723 *** HOL ***
  5724 
  5725 * Command 'typedef' now works within a local theory context -- without
  5726 introducing dependencies on parameters or assumptions, which is not
  5727 possible in Isabelle/Pure/HOL.  Note that the logical environment may
  5728 contain multiple interpretations of local typedefs (with different
  5729 non-emptiness proofs), even in a global theory context.
  5730 
  5731 * New package for quotient types.  Commands 'quotient_type' and
  5732 'quotient_definition' may be used for defining types and constants by
  5733 quotient constructions.  An example is the type of integers created by
  5734 quotienting pairs of natural numbers:
  5735 
  5736   fun
  5737     intrel :: "(nat * nat) => (nat * nat) => bool"
  5738   where
  5739     "intrel (x, y) (u, v) = (x + v = u + y)"
  5740 
  5741   quotient_type int = "nat * nat" / intrel
  5742     by (auto simp add: equivp_def expand_fun_eq)
  5743 
  5744   quotient_definition
  5745     "0::int" is "(0::nat, 0::nat)"
  5746 
  5747 The method "lifting" can be used to lift of theorems from the
  5748 underlying "raw" type to the quotient type.  The example
  5749 src/HOL/Quotient_Examples/FSet.thy includes such a quotient
  5750 construction and provides a reasoning infrastructure for finite sets.
  5751 
  5752 * Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid
  5753 clash with new theory Quotient in Main HOL.
  5754 
  5755 * Moved the SMT binding into the main HOL session, eliminating
  5756 separate HOL-SMT session.
  5757 
  5758 * List membership infix mem operation is only an input abbreviation.
  5759 INCOMPATIBILITY.
  5760 
  5761 * Theory Library/Word.thy has been removed.  Use library Word/Word.thy
  5762 for future developements; former Library/Word.thy is still present in
  5763 the AFP entry RSAPPS.
  5764 
  5765 * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no
  5766 longer shadowed.  INCOMPATIBILITY.
  5767 
  5768 * Dropped theorem duplicate comp_arith; use semiring_norm instead.
  5769 INCOMPATIBILITY.
  5770 
  5771 * Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
  5772 INCOMPATIBILITY.
  5773 
  5774 * Dropped normalizing_semiring etc; use the facts in semiring classes
  5775 instead.  INCOMPATIBILITY.
  5776 
  5777 * Dropped several real-specific versions of lemmas about floor and
  5778 ceiling; use the generic lemmas from theory "Archimedean_Field"
  5779 instead.  INCOMPATIBILITY.
  5780 
  5781   floor_number_of_eq         ~> floor_number_of
  5782   le_floor_eq_number_of      ~> number_of_le_floor
  5783   le_floor_eq_zero           ~> zero_le_floor
  5784   le_floor_eq_one            ~> one_le_floor
  5785   floor_less_eq_number_of    ~> floor_less_number_of
  5786   floor_less_eq_zero         ~> floor_less_zero
  5787   floor_less_eq_one          ~> floor_less_one
  5788   less_floor_eq_number_of    ~> number_of_less_floor
  5789   less_floor_eq_zero         ~> zero_less_floor
  5790   less_floor_eq_one          ~> one_less_floor
  5791   floor_le_eq_number_of      ~> floor_le_number_of
  5792   floor_le_eq_zero           ~> floor_le_zero
  5793   floor_le_eq_one            ~> floor_le_one
  5794   floor_subtract_number_of   ~> floor_diff_number_of
  5795   floor_subtract_one         ~> floor_diff_one
  5796   ceiling_number_of_eq       ~> ceiling_number_of
  5797   ceiling_le_eq_number_of    ~> ceiling_le_number_of
  5798   ceiling_le_zero_eq         ~> ceiling_le_zero
  5799   ceiling_le_eq_one          ~> ceiling_le_one
  5800   less_ceiling_eq_number_of  ~> number_of_less_ceiling
  5801   less_ceiling_eq_zero       ~> zero_less_ceiling
  5802   less_ceiling_eq_one        ~> one_less_ceiling
  5803   ceiling_less_eq_number_of  ~> ceiling_less_number_of
  5804   ceiling_less_eq_zero       ~> ceiling_less_zero
  5805   ceiling_less_eq_one        ~> ceiling_less_one
  5806   le_ceiling_eq_number_of    ~> number_of_le_ceiling
  5807   le_ceiling_eq_zero         ~> zero_le_ceiling
  5808   le_ceiling_eq_one          ~> one_le_ceiling
  5809   ceiling_subtract_number_of ~> ceiling_diff_number_of
  5810   ceiling_subtract_one       ~> ceiling_diff_one
  5811 
  5812 * Theory "Finite_Set": various folding_XXX locales facilitate the
  5813 application of the various fold combinators on finite sets.
  5814 
  5815 * Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"
  5816 provides abstract red-black tree type which is backed by "RBT_Impl" as
  5817 implementation.  INCOMPATIBILITY.
  5818 
  5819 * Theory Library/Coinductive_List has been removed -- superseded by
  5820 AFP/thys/Coinductive.
  5821 
  5822 * Theory PReal, including the type "preal" and related operations, has
  5823 been removed.  INCOMPATIBILITY.
  5824 
  5825 * Real: new development using Cauchy Sequences.
  5826 
  5827 * Split off theory "Big_Operators" containing setsum, setprod,
  5828 Inf_fin, Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.
  5829 
  5830 * Theory "Rational" renamed to "Rat", for consistency with "Nat",
  5831 "Int" etc.  INCOMPATIBILITY.
  5832 
  5833 * Constant Rat.normalize needs to be qualified.  INCOMPATIBILITY.
  5834 
  5835 * New set of rules "ac_simps" provides combined assoc / commute
  5836 rewrites for all interpretations of the appropriate generic locales.
  5837 
  5838 * Renamed theory "OrderedGroup" to "Groups" and split theory
  5839 "Ring_and_Field" into theories "Rings" and "Fields"; for more
  5840 appropriate and more consistent names suitable for name prefixes
  5841 within the HOL theories.  INCOMPATIBILITY.
  5842 
  5843 * Some generic constants have been put to appropriate theories:
  5844   - less_eq, less: Orderings
  5845   - zero, one, plus, minus, uminus, times, abs, sgn: Groups
  5846   - inverse, divide: Rings
  5847 INCOMPATIBILITY.
  5848 
  5849 * More consistent naming of type classes involving orderings (and
  5850 lattices):
  5851 
  5852     lower_semilattice                   ~> semilattice_inf
  5853     upper_semilattice                   ~> semilattice_sup
  5854 
  5855     dense_linear_order                  ~> dense_linorder
  5856 
  5857     pordered_ab_group_add               ~> ordered_ab_group_add
  5858     pordered_ab_group_add_abs           ~> ordered_ab_group_add_abs
  5859     pordered_ab_semigroup_add           ~> ordered_ab_semigroup_add
  5860     pordered_ab_semigroup_add_imp_le    ~> ordered_ab_semigroup_add_imp_le
  5861     pordered_cancel_ab_semigroup_add    ~> ordered_cancel_ab_semigroup_add
  5862     pordered_cancel_comm_semiring       ~> ordered_cancel_comm_semiring
  5863     pordered_cancel_semiring            ~> ordered_cancel_semiring
  5864     pordered_comm_monoid_add            ~> ordered_comm_monoid_add
  5865     pordered_comm_ring                  ~> ordered_comm_ring
  5866     pordered_comm_semiring              ~> ordered_comm_semiring
  5867     pordered_ring                       ~> ordered_ring
  5868     pordered_ring_abs                   ~> ordered_ring_abs
  5869     pordered_semiring                   ~> ordered_semiring
  5870 
  5871     ordered_ab_group_add                ~> linordered_ab_group_add
  5872     ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add
  5873     ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add
  5874     ordered_comm_semiring_strict        ~> linordered_comm_semiring_strict
  5875     ordered_field                       ~> linordered_field
  5876     ordered_field_no_lb                 ~> linordered_field_no_lb
  5877     ordered_field_no_ub                 ~> linordered_field_no_ub
  5878     ordered_field_dense_linear_order    ~> dense_linordered_field
  5879     ordered_idom                        ~> linordered_idom
  5880     ordered_ring                        ~> linordered_ring
  5881     ordered_ring_le_cancel_factor       ~> linordered_ring_le_cancel_factor
  5882     ordered_ring_less_cancel_factor     ~> linordered_ring_less_cancel_factor
  5883     ordered_ring_strict                 ~> linordered_ring_strict
  5884     ordered_semidom                     ~> linordered_semidom
  5885     ordered_semiring                    ~> linordered_semiring
  5886     ordered_semiring_1                  ~> linordered_semiring_1
  5887     ordered_semiring_1_strict           ~> linordered_semiring_1_strict
  5888     ordered_semiring_strict             ~> linordered_semiring_strict
  5889 
  5890   The following slightly odd type classes have been moved to a
  5891   separate theory Library/Lattice_Algebras:
  5892 
  5893     lordered_ab_group_add               ~> lattice_ab_group_add
  5894     lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
  5895     lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
  5896     lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
  5897     lordered_ring                       ~> lattice_ring
  5898 
  5899 INCOMPATIBILITY.
  5900 
  5901 * Refined field classes:
  5902   - classes division_ring_inverse_zero, field_inverse_zero,
  5903     linordered_field_inverse_zero include rule inverse 0 = 0 --
  5904     subsumes former division_by_zero class;
  5905   - numerous lemmas have been ported from field to division_ring.
  5906 INCOMPATIBILITY.
  5907 
  5908 * Refined algebra theorem collections:
  5909   - dropped theorem group group_simps, use algebra_simps instead;
  5910   - dropped theorem group ring_simps, use field_simps instead;
  5911   - proper theorem collection field_simps subsumes former theorem
  5912     groups field_eq_simps and field_simps;
  5913   - dropped lemma eq_minus_self_iff which is a duplicate for
  5914     equal_neg_zero.
  5915 INCOMPATIBILITY.
  5916 
  5917 * Theory Finite_Set and List: some lemmas have been generalized from
  5918 sets to lattices:
  5919 
  5920   fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf
  5921   fun_left_comm_idem_union      ~> fun_left_comm_idem_sup
  5922   inter_Inter_fold_inter        ~> inf_Inf_fold_inf
  5923   union_Union_fold_union        ~> sup_Sup_fold_sup
  5924   Inter_fold_inter              ~> Inf_fold_inf
  5925   Union_fold_union              ~> Sup_fold_sup
  5926   inter_INTER_fold_inter        ~> inf_INFI_fold_inf
  5927   union_UNION_fold_union        ~> sup_SUPR_fold_sup
  5928   INTER_fold_inter              ~> INFI_fold_inf
  5929   UNION_fold_union              ~> SUPR_fold_sup
  5930 
  5931 * Theory "Complete_Lattice": lemmas top_def and bot_def have been
  5932 replaced by the more convenient lemmas Inf_empty and Sup_empty.
  5933 Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
  5934 by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace
  5935 former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right
  5936 subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.
  5937 
  5938 * Reorganized theory Multiset: swapped notation of pointwise and
  5939 multiset order:
  5940 
  5941   - pointwise ordering is instance of class order with standard syntax
  5942     <= and <;
  5943   - multiset ordering has syntax <=# and <#; partial order properties
  5944     are provided by means of interpretation with prefix
  5945     multiset_order;
  5946   - less duplication, less historical organization of sections,
  5947     conversion from associations lists to multisets, rudimentary code
  5948     generation;
  5949   - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,
  5950     if needed.
  5951 
  5952 Renamed:
  5953 
  5954   multiset_eq_conv_count_eq  ~>  multiset_ext_iff
  5955   multi_count_ext  ~>  multiset_ext
  5956   diff_union_inverse2  ~>  diff_union_cancelR
  5957 
  5958 INCOMPATIBILITY.
  5959 
  5960 * Theory Permutation: replaced local "remove" by List.remove1.
  5961 
  5962 * Code generation: ML and OCaml code is decorated with signatures.
  5963 
  5964 * Theory List: added transpose.
  5965 
  5966 * Library/Nat_Bijection.thy is a collection of bijective functions
  5967 between nat and other types, which supersedes the older libraries
  5968 Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy.  INCOMPATIBILITY.
  5969 
  5970   Constants:
  5971   Nat_Int_Bij.nat2_to_nat         ~> prod_encode
  5972   Nat_Int_Bij.nat_to_nat2         ~> prod_decode
  5973   Nat_Int_Bij.int_to_nat_bij      ~> int_encode
  5974   Nat_Int_Bij.nat_to_int_bij      ~> int_decode
  5975   Countable.pair_encode           ~> prod_encode
  5976   NatIso.prod2nat                 ~> prod_encode
  5977   NatIso.nat2prod                 ~> prod_decode
  5978   NatIso.sum2nat                  ~> sum_encode
  5979   NatIso.nat2sum                  ~> sum_decode
  5980   NatIso.list2nat                 ~> list_encode
  5981   NatIso.nat2list                 ~> list_decode
  5982   NatIso.set2nat                  ~> set_encode
  5983   NatIso.nat2set                  ~> set_decode
  5984 
  5985   Lemmas:
  5986   Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_decode
  5987   Nat_Int_Bij.nat2_to_nat_inj     ~> inj_prod_encode
  5988   Nat_Int_Bij.nat2_to_nat_surj    ~> surj_prod_encode
  5989   Nat_Int_Bij.nat_to_nat2_inj     ~> inj_prod_decode
  5990   Nat_Int_Bij.nat_to_nat2_surj    ~> surj_prod_decode
  5991   Nat_Int_Bij.i2n_n2i_id          ~> int_encode_inverse
  5992   Nat_Int_Bij.n2i_i2n_id          ~> int_decode_inverse
  5993   Nat_Int_Bij.surj_nat_to_int_bij ~> surj_int_encode
  5994   Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode
  5995   Nat_Int_Bij.inj_nat_to_int_bij  ~> inj_int_encode
  5996   Nat_Int_Bij.inj_int_to_nat_bij  ~> inj_int_decode
  5997   Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode
  5998   Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode
  5999 
  6000 * Sledgehammer:
  6001   - Renamed ATP commands:
  6002     atp_info     ~> sledgehammer running_atps
  6003     atp_kill     ~> sledgehammer kill_atps
  6004     atp_messages ~> sledgehammer messages
  6005     atp_minimize ~> sledgehammer minimize
  6006     print_atps   ~> sledgehammer available_atps
  6007     INCOMPATIBILITY.
  6008   - Added user's manual ("isabelle doc sledgehammer").
  6009   - Added option syntax and "sledgehammer_params" to customize
  6010     Sledgehammer's behavior.  See the manual for details.
  6011   - Modified the Isar proof reconstruction code so that it produces
  6012     direct proofs rather than proofs by contradiction.  (This feature
  6013     is still experimental.)
  6014   - Made Isar proof reconstruction work for SPASS, remote ATPs, and in
  6015     full-typed mode.
  6016   - Added support for TPTP syntax for SPASS via the "spass_tptp" ATP.
  6017 
  6018 * Nitpick:
  6019   - Added and implemented "binary_ints" and "bits" options.
  6020   - Added "std" option and implemented support for nonstandard models.
  6021   - Added and implemented "finitize" option to improve the precision
  6022     of infinite datatypes based on a monotonicity analysis.
  6023   - Added support for quotient types.
  6024   - Added support for "specification" and "ax_specification"
  6025     constructs.
  6026   - Added support for local definitions (for "function" and
  6027     "termination" proofs).
  6028   - Added support for term postprocessors.
  6029   - Optimized "Multiset.multiset" and "FinFun.finfun".
  6030   - Improved efficiency of "destroy_constrs" optimization.
  6031   - Fixed soundness bugs related to "destroy_constrs" optimization and
  6032     record getters.
  6033   - Fixed soundness bug related to higher-order constructors.
  6034   - Fixed soundness bug when "full_descrs" is enabled.
  6035   - Improved precision of set constructs.
  6036   - Added "atoms" option.
  6037   - Added cache to speed up repeated Kodkod invocations on the same
  6038     problems.
  6039   - Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and
  6040     "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and
  6041     "SAT4J_Light".  INCOMPATIBILITY.
  6042   - Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
  6043     "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.
  6044   - Removed "nitpick_intro" attribute.  INCOMPATIBILITY.
  6045 
  6046 * Method "induct" now takes instantiations of the form t, where t is not
  6047   a variable, as a shorthand for "x == t", where x is a fresh variable.
  6048   If this is not intended, t has to be enclosed in parentheses.
  6049   By default, the equalities generated by definitional instantiations
  6050   are pre-simplified, which may cause parameters of inductive cases
  6051   to disappear, or may even delete some of the inductive cases.
  6052   Use "induct (no_simp)" instead of "induct" to restore the old
  6053   behaviour. The (no_simp) option is also understood by the "cases"
  6054   and "nominal_induct" methods, which now perform pre-simplification, too.
  6055   INCOMPATIBILITY.
  6056 
  6057 
  6058 *** HOLCF ***
  6059 
  6060 * Variable names in lemmas generated by the domain package have
  6061 changed; the naming scheme is now consistent with the HOL datatype
  6062 package.  Some proof scripts may be affected, INCOMPATIBILITY.
  6063 
  6064 * The domain package no longer defines the function "foo_copy" for
  6065 recursive domain "foo".  The reach lemma is now stated directly in
  6066 terms of "foo_take".  Lemmas and proofs that mention "foo_copy" must
  6067 be reformulated in terms of "foo_take", INCOMPATIBILITY.
  6068 
  6069 * Most definedness lemmas generated by the domain package (previously
  6070 of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form
  6071 like "foo$x = UU <-> x = UU", which works better as a simp rule.
  6072 Proofs that used definedness lemmas as intro rules may break,
  6073 potential INCOMPATIBILITY.
  6074 
  6075 * Induction and casedist rules generated by the domain package now
  6076 declare proper case_names (one called "bottom", and one named for each
  6077 constructor).  INCOMPATIBILITY.
  6078 
  6079 * For mutually-recursive domains, separate "reach" and "take_lemma"
  6080 rules are generated for each domain, INCOMPATIBILITY.
  6081 
  6082   foo_bar.reach       ~> foo.reach  bar.reach
  6083   foo_bar.take_lemmas ~> foo.take_lemma  bar.take_lemma
  6084 
  6085 * Some lemmas generated by the domain package have been renamed for
  6086 consistency with the datatype package, INCOMPATIBILITY.
  6087 
  6088   foo.ind        ~> foo.induct
  6089   foo.finite_ind ~> foo.finite_induct
  6090   foo.coind      ~> foo.coinduct
  6091   foo.casedist   ~> foo.exhaust
  6092   foo.exhaust    ~> foo.nchotomy
  6093 
  6094 * For consistency with other definition packages, the fixrec package
  6095 now generates qualified theorem names, INCOMPATIBILITY.
  6096 
  6097   foo_simps  ~> foo.simps
  6098   foo_unfold ~> foo.unfold
  6099   foo_induct ~> foo.induct
  6100 
  6101 * The "fixrec_simp" attribute has been removed.  The "fixrec_simp"
  6102 method and internal fixrec proofs now use the default simpset instead.
  6103 INCOMPATIBILITY.
  6104 
  6105 * The "contlub" predicate has been removed.  Proof scripts should use
  6106 lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.
  6107 
  6108 * The "admw" predicate has been removed, INCOMPATIBILITY.
  6109 
  6110 * The constants cpair, cfst, and csnd have been removed in favor of
  6111 Pair, fst, and snd from Isabelle/HOL, INCOMPATIBILITY.
  6112 
  6113 
  6114 *** ML ***
  6115 
  6116 * Antiquotations for basic formal entities:
  6117 
  6118     @{class NAME}         -- type class
  6119     @{class_syntax NAME}  -- syntax representation of the above
  6120 
  6121     @{type_name NAME}     -- logical type
  6122     @{type_abbrev NAME}   -- type abbreviation
  6123     @{nonterminal NAME}   -- type of concrete syntactic category
  6124     @{type_syntax NAME}   -- syntax representation of any of the above
  6125 
  6126     @{const_name NAME}    -- logical constant (INCOMPATIBILITY)
  6127     @{const_abbrev NAME}  -- abbreviated constant
  6128     @{const_syntax NAME}  -- syntax representation of any of the above
  6129 
  6130 * Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
  6131 syntax constant (cf. 'syntax' command).
  6132 
  6133 * Antiquotation @{make_string} inlines a function to print arbitrary
  6134 values similar to the ML toplevel.  The result is compiler dependent
  6135 and may fall back on "?" in certain situations.
  6136 
  6137 * Diagnostic commands 'ML_val' and 'ML_command' may refer to
  6138 antiquotations @{Isar.state} and @{Isar.goal}.  This replaces impure
  6139 Isar.state() and Isar.goal(), which belong to the old TTY loop and do
  6140 not work with the asynchronous Isar document model.
  6141 
  6142 * Configuration options now admit dynamic default values, depending on
  6143 the context or even global references.
  6144 
  6145 * SHA1.digest digests strings according to SHA-1 (see RFC 3174).  It
  6146 uses an efficient external library if available (for Poly/ML).
  6147 
  6148 * Renamed some important ML structures, while keeping the old names
  6149 for some time as aliases within the structure Legacy:
  6150 
  6151   OuterKeyword  ~>  Keyword
  6152   OuterLex      ~>  Token
  6153   OuterParse    ~>  Parse
  6154   OuterSyntax   ~>  Outer_Syntax
  6155   PrintMode     ~>  Print_Mode
  6156   SpecParse     ~>  Parse_Spec
  6157   ThyInfo       ~>  Thy_Info
  6158   ThyLoad       ~>  Thy_Load
  6159   ThyOutput     ~>  Thy_Output
  6160   TypeInfer     ~>  Type_Infer
  6161 
  6162 Note that "open Legacy" simplifies porting of sources, but forgetting
  6163 to remove it again will complicate porting again in the future.
  6164 
  6165 * Most operations that refer to a global context are named
  6166 accordingly, e.g. Simplifier.global_context or
  6167 ProofContext.init_global.  There are some situations where a global
  6168 context actually works, but under normal circumstances one needs to
  6169 pass the proper local context through the code!
  6170 
  6171 * Discontinued old TheoryDataFun with its copy/init operation -- data
  6172 needs to be pure.  Functor Theory_Data_PP retains the traditional
  6173 Pretty.pp argument to merge, which is absent in the standard
  6174 Theory_Data version.
  6175 
  6176 * Sorts.certify_sort and derived "cert" operations for types and terms
  6177 no longer minimize sorts.  Thus certification at the boundary of the
  6178 inference kernel becomes invariant under addition of class relations,
  6179 which is an important monotonicity principle.  Sorts are now minimized
  6180 in the syntax layer only, at the boundary between the end-user and the
  6181 system.  Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
  6182 explicitly in rare situations.
  6183 
  6184 * Renamed old-style Drule.standard to Drule.export_without_context, to
  6185 emphasize that this is in no way a standard operation.
  6186 INCOMPATIBILITY.
  6187 
  6188 * Subgoal.FOCUS (and variants): resulting goal state is normalized as
  6189 usual for resolution.  Rare INCOMPATIBILITY.
  6190 
  6191 * Renamed varify/unvarify operations to varify_global/unvarify_global
  6192 to emphasize that these only work in a global situation (which is
  6193 quite rare).
  6194 
  6195 * Curried take and drop in library.ML; negative length is interpreted
  6196 as infinity (as in chop).  Subtle INCOMPATIBILITY.
  6197 
  6198 * Proof terms: type substitutions on proof constants now use canonical
  6199 order of type variables.  INCOMPATIBILITY for tools working with proof
  6200 terms.
  6201 
  6202 * Raw axioms/defs may no longer carry sort constraints, and raw defs
  6203 may no longer carry premises.  User-level specifications are
  6204 transformed accordingly by Thm.add_axiom/add_def.
  6205 
  6206 
  6207 *** System ***
  6208 
  6209 * Discontinued special HOL_USEDIR_OPTIONS for the main HOL image;
  6210 ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions.  Note that
  6211 proof terms are enabled unconditionally in the new HOL-Proofs image.
  6212 
  6213 * Discontinued old ISABELLE and ISATOOL environment settings (legacy
  6214 feature since Isabelle2009).  Use ISABELLE_PROCESS and ISABELLE_TOOL,
  6215 respectively.
  6216 
  6217 * Old lib/scripts/polyml-platform is superseded by the
  6218 ISABELLE_PLATFORM setting variable, which defaults to the 32 bit
  6219 variant, even on a 64 bit machine.  The following example setting
  6220 prefers 64 bit if available:
  6221 
  6222   ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
  6223 
  6224 * The preliminary Isabelle/jEdit application demonstrates the emerging
  6225 Isabelle/Scala layer for advanced prover interaction and integration.
  6226 See src/Tools/jEdit or "isabelle jedit" provided by the properly built
  6227 component.
  6228 
  6229 * "IsabelleText" is a Unicode font derived from Bitstream Vera Mono
  6230 and Bluesky TeX fonts.  It provides the usual Isabelle symbols,
  6231 similar to the default assignment of the document preparation system
  6232 (cf. isabellesym.sty).  The Isabelle/Scala class Isabelle_System
  6233 provides some operations for direct access to the font without asking
  6234 the user for manual installation.
  6235 
  6236 
  6237 
  6238 New in Isabelle2009-1 (December 2009)
  6239 -------------------------------------
  6240 
  6241 *** General ***
  6242 
  6243 * Discontinued old form of "escaped symbols" such as \\<forall>.  Only
  6244 one backslash should be used, even in ML sources.
  6245 
  6246 
  6247 *** Pure ***
  6248 
  6249 * Locale interpretation propagates mixins along the locale hierarchy.
  6250 The currently only available mixins are the equations used to map
  6251 local definitions to terms of the target domain of an interpretation.
  6252 
  6253 * Reactivated diagnostic command 'print_interps'.  Use "print_interps
  6254 loc" to print all interpretations of locale "loc" in the theory.
  6255 Interpretations in proofs are not shown.
  6256 
  6257 * Thoroughly revised locales tutorial.  New section on conditional
  6258 interpretation.
  6259 
  6260 * On instantiation of classes, remaining undefined class parameters
  6261 are formally declared.  INCOMPATIBILITY.
  6262 
  6263 
  6264 *** Document preparation ***
  6265 
  6266 * New generalized style concept for printing terms: @{foo (style) ...}
  6267 instead of @{foo_style style ...}  (old form is still retained for
  6268 backward compatibility).  Styles can be also applied for
  6269 antiquotations prop, term_type and typeof.
  6270 
  6271 
  6272 *** HOL ***
  6273 
  6274 * New proof method "smt" for a combination of first-order logic with
  6275 equality, linear and nonlinear (natural/integer/real) arithmetic, and
  6276 fixed-size bitvectors; there is also basic support for higher-order
  6277 features (esp. lambda abstractions).  It is an incomplete decision
  6278 procedure based on external SMT solvers using the oracle mechanism;
  6279 for the SMT solver Z3, this method is proof-producing.  Certificates
  6280 are provided to avoid calling the external solvers solely for