NEWS
author boehmes
Mon Nov 08 12:13:44 2010 +0100 (2010-11-08)
changeset 40424 7550b2cba1cb
parent 40388 cb9fd7dd641c
child 40580 0592d3a39c08
permissions -rw-r--r--
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
wenzelm@5363
     1
Isabelle NEWS -- history user-relevant changes
wenzelm@5363
     2
==============================================
wenzelm@2553
     3
wenzelm@37383
     4
New in this Isabelle version
wenzelm@37383
     5
----------------------------
wenzelm@37383
     6
wenzelm@37536
     7
*** General ***
wenzelm@37536
     8
wenzelm@40387
     9
* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
wenzelm@40387
    10
(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
wenzelm@40387
    11
while the default heap location within that directory lacks that extra
wenzelm@40387
    12
suffix.  This isolates multiple Isabelle installations from each
wenzelm@40387
    13
other, avoiding problems with old settings in new versions.
wenzelm@40387
    14
INCOMPATIBILITY, need to copy/upgrade old user settings manually.
wenzelm@40387
    15
wenzelm@40127
    16
* Significantly improved Isabelle/Isar implementation manual.
wenzelm@40127
    17
wenzelm@37536
    18
* Explicit treatment of UTF8 sequences as Isabelle symbols, such that
wenzelm@37536
    19
a Unicode character is treated as a single symbol, not a sequence of
wenzelm@37536
    20
non-ASCII bytes as before.  Since Isabelle/ML string literals may
wenzelm@37536
    21
contain symbols without further backslash escapes, Unicode can now be
wenzelm@37536
    22
used here as well.  Recall that Symbol.explode in ML provides a
wenzelm@37536
    23
consistent view on symbols, while raw explode (or String.explode)
wenzelm@37536
    24
merely give a byte-oriented representation.
wenzelm@37536
    25
wenzelm@38135
    26
* Theory loading: only the master source file is looked-up in the
wenzelm@38135
    27
implicit load path, all other files are addressed relatively to its
wenzelm@38135
    28
directory.  Minor INCOMPATIBILITY, subtle change in semantics.
wenzelm@38135
    29
wenzelm@37939
    30
* Special treatment of ML file names has been discontinued.
wenzelm@37939
    31
Historically, optional extensions .ML or .sml were added on demand --
wenzelm@37939
    32
at the cost of clarity of file dependencies.  Recall that Isabelle/ML
wenzelm@37939
    33
files exclusively use the .ML extension.  Minor INCOMPATIBILTY.
wenzelm@37939
    34
wenzelm@38980
    35
* Various options that affect pretty printing etc. are now properly
wenzelm@38767
    36
handled within the context via configuration options, instead of
wenzelm@38767
    37
unsynchronized references.  There are both ML Config.T entities and
wenzelm@38767
    38
Isar declaration attributes to access these.
wenzelm@38767
    39
wenzelm@39125
    40
  ML (Config.T)                 Isar (attribute)
wenzelm@39125
    41
wenzelm@39128
    42
  eta_contract                  eta_contract
wenzelm@39137
    43
  show_brackets                 show_brackets
wenzelm@39134
    44
  show_sorts                    show_sorts
wenzelm@39134
    45
  show_types                    show_types
wenzelm@39126
    46
  show_question_marks           show_question_marks
wenzelm@39126
    47
  show_consts                   show_consts
wenzelm@39126
    48
wenzelm@39126
    49
  Syntax.ambiguity_level        syntax_ambiguity_level
wenzelm@39126
    50
wenzelm@39126
    51
  Goal_Display.goals_limit      goals_limit
wenzelm@39126
    52
  Goal_Display.show_main_goal   show_main_goal
wenzelm@39126
    53
wenzelm@39125
    54
  Thy_Output.display            thy_output_display
wenzelm@39125
    55
  Thy_Output.quotes             thy_output_quotes
wenzelm@39125
    56
  Thy_Output.indent             thy_output_indent
wenzelm@39125
    57
  Thy_Output.source             thy_output_source
wenzelm@39125
    58
  Thy_Output.break              thy_output_break
wenzelm@39125
    59
wenzelm@39125
    60
Note that corresponding "..._default" references in ML may be only
wenzelm@38767
    61
changed globally at the ROOT session setup, but *not* within a theory.
wenzelm@38767
    62
wenzelm@37536
    63
ballarin@38110
    64
*** Pure ***
ballarin@38110
    65
wenzelm@40291
    66
* Support for real valued configuration options, using simplistic
wenzelm@40291
    67
floating-point notation that coincides with the inner syntax for
wenzelm@40291
    68
float_token.
wenzelm@40291
    69
wenzelm@40292
    70
* Support for real valued preferences (with approximative PGIP type).
wenzelm@40292
    71
ballarin@38110
    72
* Interpretation command 'interpret' accepts a list of equations like
ballarin@38110
    73
'interpretation' does.
ballarin@38110
    74
ballarin@38110
    75
* Diagnostic command 'print_interps' prints interpretations in proofs
ballarin@38110
    76
in addition to interpretations in theories.
ballarin@38110
    77
wenzelm@38708
    78
* Discontinued obsolete 'global' and 'local' commands to manipulate
wenzelm@38708
    79
the theory name space.  Rare INCOMPATIBILITY.  The ML functions
wenzelm@38708
    80
Sign.root_path and Sign.local_path may be applied directly where this
wenzelm@38708
    81
feature is still required for historical reasons.
wenzelm@38708
    82
haftmann@39215
    83
* Discontinued ancient 'constdefs' command.  INCOMPATIBILITY, use
haftmann@39215
    84
'definition' instead.
haftmann@39215
    85
wenzelm@39689
    86
* Document antiquotations @{class} and @{type} for printing classes
haftmann@39305
    87
and type constructors.
haftmann@39305
    88
ballarin@38110
    89
haftmann@37387
    90
*** HOL ***
haftmann@37387
    91
haftmann@40348
    92
* Theory Multiset provides stable quicksort implementation of sort_key.
haftmann@40348
    93
bulwahn@40247
    94
* Quickcheck now has a configurable time limit which is set to 30 seconds
bulwahn@40247
    95
by default. This can be changed by adding [timeout = n] to the quickcheck
bulwahn@40247
    96
command. The time limit for auto quickcheck is still set independently,
bulwahn@40247
    97
by default to 5 seconds.
bulwahn@40247
    98
krauss@40183
    99
* New command 'partial_function' provides basic support for recursive
krauss@40194
   100
function definitions over complete partial orders. Concrete instances
krauss@40183
   101
are provided for i) the option type, ii) tail recursion on arbitrary
krauss@40183
   102
types, and iii) the heap monad of Imperative_HOL. See
krauss@40183
   103
HOL/ex/Fundefs.thy and HOL/Imperative_HOL/ex/Linked_Lists.thy for
krauss@40183
   104
examples.
krauss@40183
   105
haftmann@39916
   106
* Predicates `distinct` and `sorted` now defined inductively, with nice
haftmann@39916
   107
induction rules.  INCOMPATIBILITY: former distinct.simps and sorted.simps
haftmann@39916
   108
now named distinct_simps and sorted_simps.
haftmann@39916
   109
haftmann@39910
   110
* Constant `contents` renamed to `the_elem`, to free the generic name
haftmann@39910
   111
contents for other uses.  INCOMPATIBILITY.
haftmann@39910
   112
haftmann@39771
   113
* Dropped old primrec package.  INCOMPATIBILITY.
haftmann@39771
   114
haftmann@39644
   115
* Improved infrastructure for term evaluation using code generator
haftmann@39644
   116
techniques, in particular static evaluation conversions.
haftmann@39644
   117
haftmann@39771
   118
* String.literal is a type, but not a datatype.  INCOMPATIBILITY.
bulwahn@39250
   119
 
nipkow@39302
   120
* Renamed lemmas:
nipkow@39302
   121
  expand_fun_eq -> fun_eq_iff
nipkow@39302
   122
  expand_set_eq -> set_eq_iff
nipkow@39302
   123
  set_ext -> set_eqI
haftmann@39644
   124
 INCOMPATIBILITY.
nipkow@39199
   125
nipkow@40078
   126
* Renamed lemma list: nat_number -> eval_nat_numeral
nipkow@40078
   127
haftmann@38857
   128
* Renamed class eq and constant eq (for code generation) to class equal
haftmann@38857
   129
and constant equal, plus renaming of related facts and various tuning.
haftmann@38857
   130
INCOMPATIBILITY.
haftmann@38857
   131
haftmann@38814
   132
* Scala (2.8 or higher) has been added to the target languages of
haftmann@38814
   133
the code generator.
haftmann@38814
   134
haftmann@38642
   135
* Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.
haftmann@38642
   136
krauss@39993
   137
* Removed output syntax "'a ~=> 'b" for "'a => 'b option". INCOMPATIBILITY.
krauss@39993
   138
haftmann@38622
   139
* Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
haftmann@38622
   140
canonical names for instance definitions for functions; various improvements.
haftmann@38622
   141
INCOMPATIBILITY.
haftmann@38622
   142
haftmann@38545
   143
* Records: logical foundation type for records do not carry a '_type' suffix
haftmann@38545
   144
any longer.  INCOMPATIBILITY.
haftmann@38545
   145
haftmann@38535
   146
* Code generation for records: more idiomatic representation of record types.
haftmann@38535
   147
Warning: records are not covered by ancient SML code generation any longer.
haftmann@38537
   148
INCOMPATIBILITY.  In cases of need, a suitable rep_datatype declaration
haftmann@38537
   149
helps to succeed then:
haftmann@38537
   150
haftmann@38537
   151
  record 'a foo = ...
haftmann@38537
   152
  ...
haftmann@38537
   153
  rep_datatype foo_ext ...
haftmann@38535
   154
haftmann@38461
   155
* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
haftmann@38461
   156
INCOMPATIBILITY.
haftmann@38461
   157
haftmann@38461
   158
* Quickcheck in locales considers interpretations of that locale for
haftmann@38461
   159
counter example search.
haftmann@38461
   160
haftmann@38347
   161
* Theory Library/Monad_Syntax provides do-syntax for monad types.  Syntax
haftmann@38347
   162
in Library/State_Monad has been changed to avoid ambiguities.
haftmann@38347
   163
INCOMPATIBILITY.
haftmann@38347
   164
haftmann@38461
   165
* Code generator: export_code without explicit file declaration prints
haftmann@37820
   166
to standard output.  INCOMPATIBILITY.
haftmann@37820
   167
haftmann@37679
   168
* Abolished symbol type names:  "prod" and "sum" replace "*" and "+"
haftmann@37681
   169
respectively.  INCOMPATIBILITY.
haftmann@37679
   170
nipkow@40294
   171
* Name "Plus" of disjoint sum operator "<+>" is now hidden.
nipkow@40294
   172
  Write Sum_Type.Plus.
nipkow@40294
   173
haftmann@37591
   174
* Constant "split" has been merged with constant "prod_case";  names
haftmann@37591
   175
of ML functions, facts etc. involving split have been retained so far,
haftmann@37591
   176
though.  INCOMPATIBILITY.
haftmann@37591
   177
haftmann@37595
   178
* Dropped old infix syntax "mem" for List.member;  use "in set"
haftmann@37595
   179
instead.  INCOMPATIBILITY.
haftmann@37595
   180
haftmann@37595
   181
* Refactoring of code-generation specific operations in List.thy
haftmann@37595
   182
haftmann@37595
   183
  constants
haftmann@37595
   184
    null ~> List.null
haftmann@37595
   185
haftmann@37595
   186
  facts
haftmann@37595
   187
    mem_iff ~> member_def
haftmann@37595
   188
    null_empty ~> null_def
haftmann@37595
   189
haftmann@37595
   190
INCOMPATIBILITY.  Note that these were not suppossed to be used
haftmann@37595
   191
regularly unless for striking reasons;  their main purpose was code
haftmann@37595
   192
generation.
haftmann@37595
   193
haftmann@37387
   194
* Some previously unqualified names have been qualified:
haftmann@37387
   195
haftmann@37387
   196
  types
haftmann@38556
   197
    bool ~> HOL.bool
haftmann@37387
   198
    nat ~> Nat.nat
haftmann@37387
   199
haftmann@37387
   200
  constants
haftmann@38556
   201
    Trueprop ~> HOL.Trueprop
haftmann@38556
   202
    True ~> HOL.True
haftmann@38556
   203
    False ~> HOL.False
haftmann@38795
   204
    op & ~> HOL.conj
haftmann@38795
   205
    op | ~> HOL.disj
haftmann@38788
   206
    op --> ~> HOL.implies
haftmann@38864
   207
    op = ~> HOL.eq
haftmann@38556
   208
    Not ~> HOL.Not
haftmann@38556
   209
    The ~> HOL.The
haftmann@38556
   210
    All ~> HOL.All
haftmann@38556
   211
    Ex ~> HOL.Ex
haftmann@38556
   212
    Ex1 ~> HOL.Ex1
haftmann@38524
   213
    Let ~> HOL.Let
haftmann@38524
   214
    If ~> HOL.If
haftmann@37387
   215
    Ball ~> Set.Ball
haftmann@37387
   216
    Bex ~> Set.Bex
haftmann@37387
   217
    Suc ~> Nat.Suc
haftmann@37389
   218
    Pair ~> Product_Type.Pair
haftmann@37389
   219
    fst ~> Product_Type.fst
haftmann@37389
   220
    snd ~> Product_Type.snd
haftmann@37387
   221
    curry ~> Product_Type.curry
haftmann@37679
   222
    op : ~> Set.member
haftmann@37679
   223
    Collect ~> Set.Collect
haftmann@37387
   224
haftmann@37387
   225
INCOMPATIBILITY.
wenzelm@37383
   226
haftmann@37411
   227
* Removed simplifier congruence rule of "prod_case", as has for long
haftmann@38524
   228
been the case with "split".  INCOMPATIBILITY.
haftmann@37411
   229
haftmann@37423
   230
* Datatype package: theorems generated for executable equality
haftmann@37423
   231
(class eq) carry proper names and are treated as default code
haftmann@37423
   232
equations.
haftmann@37423
   233
krauss@39150
   234
* Removed lemma Option.is_none_none (Duplicate of is_none_def).
krauss@39150
   235
INCOMPATIBILITY.
krauss@39150
   236
haftmann@37423
   237
* List.thy: use various operations from the Haskell prelude when
haftmann@37423
   238
generating Haskell code.
haftmann@37423
   239
nipkow@39301
   240
* Multiset.thy: renamed empty_idemp -> empty_neutral
nipkow@39301
   241
haftmann@38524
   242
* code_simp.ML and method code_simp: simplification with rules determined
haftmann@38524
   243
by code generator.
haftmann@37442
   244
haftmann@37442
   245
* code generator: do not print function definitions for case
haftmann@37442
   246
combinators any longer.
haftmann@37442
   247
hoelzl@37666
   248
* Multivariate Analysis: Introduced a type class for euclidean space. Most
hoelzl@37666
   249
theorems are now stated in terms of euclidean spaces instead of finite
hoelzl@37666
   250
cartesian products.
hoelzl@37666
   251
hoelzl@37666
   252
  types
hoelzl@37666
   253
    real ^ 'n ~>  'a::real_vector
hoelzl@37666
   254
              ~>  'a::euclidean_space
hoelzl@37666
   255
              ~>  'a::ordered_euclidean_space
hoelzl@37666
   256
        (depends on your needs)
hoelzl@37666
   257
hoelzl@37666
   258
  constants
hoelzl@37666
   259
     _ $ _        ~> _ $$ _
hoelzl@37666
   260
     \<chi> x. _  ~> \<chi>\<chi> x. _
hoelzl@37666
   261
     CARD('n)     ~> DIM('a)
hoelzl@37666
   262
hoelzl@37666
   263
Also note that the indices are now natural numbers and not from some finite
hoelzl@37666
   264
type. Finite cartesian products of euclidean spaces, products of euclidean
hoelzl@37666
   265
spaces the real and complex numbers are instantiated to be euclidean_spaces.
hoelzl@37666
   266
hoelzl@37666
   267
INCOMPATIBILITY.
wenzelm@37383
   268
hoelzl@38656
   269
* Probability: Introduced pinfreal as real numbers with infinity. Use pinfreal
hoelzl@38656
   270
as value for measures. Introduces Lebesgue Measure based on the integral in
hoelzl@38656
   271
Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure
hoelzl@38656
   272
spaces.
hoelzl@38656
   273
hoelzl@38656
   274
 INCOMPATIBILITY.
hoelzl@38656
   275
bulwahn@37735
   276
* Inductive package: offers new command "inductive_simps" to automatically
haftmann@38461
   277
derive instantiated and simplified equations for inductive predicates,
haftmann@38461
   278
similar to inductive_cases.
bulwahn@37735
   279
hoelzl@39077
   280
* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a
hoelzl@39077
   281
generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
hoelzl@39077
   282
The theorems bij_def and surj_def are unchanged.
wenzelm@37383
   283
krauss@39754
   284
* Function package: .psimps rules are no longer implicitly declared [simp].
krauss@39754
   285
INCOMPATIBILITY.
krauss@39754
   286
blanchet@39957
   287
* Weaker versions of the "meson" and "metis" proof methods are now available in
blanchet@39957
   288
  "HOL-Plain", without dependency on "Hilbert_Choice". The proof methods become
blanchet@39957
   289
  more powerful after "Hilbert_Choice" is loaded in "HOL-Main".
blanchet@39957
   290
blanchet@39957
   291
* MESON: Renamed lemmas:
blanchet@39957
   292
  meson_not_conjD ~> Meson.not_conjD
blanchet@39957
   293
  meson_not_disjD ~> Meson.not_disjD
blanchet@39957
   294
  meson_not_notD ~> Meson.not_notD
blanchet@39957
   295
  meson_not_allD ~> Meson.not_allD
blanchet@39957
   296
  meson_not_exD ~> Meson.not_exD
blanchet@39957
   297
  meson_imp_to_disjD ~> Meson.imp_to_disjD
blanchet@39957
   298
  meson_not_impD ~> Meson.not_impD
blanchet@39957
   299
  meson_iff_to_disjD ~> Meson.iff_to_disjD
blanchet@39957
   300
  meson_not_iffD ~> Meson.not_iffD
blanchet@39957
   301
  meson_not_refl_disj_D ~> Meson.not_refl_disj_D
blanchet@39957
   302
  meson_conj_exD1 ~> Meson.conj_exD1
blanchet@39957
   303
  meson_conj_exD2 ~> Meson.conj_exD2
blanchet@39957
   304
  meson_disj_exD ~> Meson.disj_exD
blanchet@39957
   305
  meson_disj_exD1 ~> Meson.disj_exD1
blanchet@39957
   306
  meson_disj_exD2 ~> Meson.disj_exD2
blanchet@39957
   307
  meson_disj_assoc ~> Meson.disj_assoc
blanchet@39957
   308
  meson_disj_comm ~> Meson.disj_comm
blanchet@39957
   309
  meson_disj_FalseD1 ~> Meson.disj_FalseD1
blanchet@39957
   310
  meson_disj_FalseD2 ~> Meson.disj_FalseD2
blanchet@39957
   311
INCOMPATIBILITY.
blanchet@39957
   312
blanchet@40116
   313
* Auto Solve: Renamed "Auto Solve Direct". The tool is now available manually as
blanchet@40116
   314
  "solve_direct".
blanchet@40116
   315
blanchet@40059
   316
* Sledgehammer:
blanchet@40059
   317
  - Renamed lemmas:
blanchet@40059
   318
    COMBI_def ~> Meson.COMBI_def
blanchet@40059
   319
    COMBK_def ~> Meson.COMBK_def
blanchet@40059
   320
    COMBB_def ~> Meson.COMBB_def
blanchet@40059
   321
    COMBC_def ~> Meson.COMBC_def
blanchet@40059
   322
    COMBS_def ~> Meson.COMBS_def
blanchet@40059
   323
    abs_I ~> Meson.abs_I
blanchet@40059
   324
    abs_K ~> Meson.abs_K
blanchet@40059
   325
    abs_B ~> Meson.abs_B
blanchet@40059
   326
    abs_C ~> Meson.abs_C
blanchet@40059
   327
    abs_S ~> Meson.abs_S
blanchet@40059
   328
    INCOMPATIBILITY.
blanchet@40059
   329
  - Renamed commands:
blanchet@40059
   330
    sledgehammer atp_info ~> sledgehammer running_provers
blanchet@40059
   331
    sledgehammer atp_kill ~> sledgehammer kill_provers
blanchet@40059
   332
    sledgehammer available_atps ~> sledgehammer available_provers
blanchet@40059
   333
    INCOMPATIBILITY.
blanchet@40059
   334
  - Renamed options:
blanchet@40059
   335
    sledgehammer [atps = ...] ~> sledgehammer [provers = ...]
blanchet@40062
   336
    sledgehammer [atp = ...] ~> sledgehammer [prover = ...]
blanchet@40341
   337
    sledgehammer [timeout = 77 s] ~> sledgehammer [timeout = 77]
blanchet@40341
   338
    (and "ms" and "min" are no longer supported)
blanchet@40341
   339
    INCOMPATIBILITY.
blanchet@40341
   340
blanchet@40341
   341
* Nitpick:
blanchet@40341
   342
  - Renamed options:
blanchet@40341
   343
    nitpick [timeout = 77 s] ~> nitpick [timeout = 77]
blanchet@40341
   344
    nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]
blanchet@40059
   345
    INCOMPATIBILITY.
blanchet@39957
   346
boehmes@40162
   347
* Changed SMT configuration options:
boehmes@40162
   348
  - Renamed:
boehmes@40162
   349
    z3_proofs ~> smt_oracle (with swapped semantics)
boehmes@40162
   350
    z3_trace_assms ~> smt_trace_used_facts
boehmes@40162
   351
    INCOMPATIBILITY.
boehmes@40162
   352
  - Added:
boehmes@40424
   353
    smt_verbose
boehmes@40424
   354
    smt_datatypes
boehmes@40162
   355
    cvc3_options
boehmes@40162
   356
    yices_options
blanchet@39957
   357
krauss@40388
   358
* Removed [split_format ... and ... and ...] version of
krauss@40388
   359
[split_format].  Potential INCOMPATIBILITY.
krauss@40388
   360
haftmann@38522
   361
*** FOL ***
haftmann@38522
   362
haftmann@38522
   363
* All constant names are now qualified.  INCOMPATIBILITY.
haftmann@38522
   364
haftmann@38522
   365
haftmann@38522
   366
*** ZF ***
haftmann@38522
   367
haftmann@38522
   368
* All constant names are now qualified.  INCOMPATIBILITY.
haftmann@38522
   369
haftmann@38522
   370
wenzelm@37868
   371
*** ML ***
wenzelm@37868
   372
wenzelm@40318
   373
* Discontinued obsolete function sys_error and exception SYS_ERROR.
wenzelm@40318
   374
See implementation manual for further details on exceptions in
wenzelm@40318
   375
Isabelle/ML.
wenzelm@40318
   376
wenzelm@40110
   377
* Antiquotation @{assert} inlines a function bool -> unit that raises
wenzelm@40110
   378
Fail if the argument is false.  Due to inlining the source position of
wenzelm@40110
   379
failed assertions is included in the error output.
wenzelm@40110
   380
wenzelm@40241
   381
* Discontinued antiquotation @{theory_ref}, which is obsolete since ML
wenzelm@40241
   382
text is in practice always evaluated with a stable theory checkpoint.
wenzelm@40241
   383
Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.
wenzelm@40241
   384
wenzelm@39616
   385
* Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
wenzelm@39616
   386
meaning.
wenzelm@39616
   387
wenzelm@39557
   388
* Renamed structure PureThy to Pure_Thy and moved most of its
wenzelm@39557
   389
operations to structure Global_Theory, to emphasize that this is
wenzelm@39557
   390
rarely-used global-only stuff.
wenzelm@39557
   391
wenzelm@39513
   392
* Discontinued Output.debug.  Minor INCOMPATIBILITY, use plain writeln
wenzelm@39513
   393
instead (or tracing for high-volume output).
wenzelm@39513
   394
wenzelm@38980
   395
* Configuration option show_question_marks only affects regular pretty
wenzelm@38980
   396
printing of types and terms, not raw Term.string_of_vname.
wenzelm@38980
   397
wenzelm@39164
   398
* ML_Context.thm and ML_Context.thms are no longer pervasive.  Rare
wenzelm@39164
   399
INCOMPATIBILITY, superseded by static antiquotations @{thm} and
wenzelm@39164
   400
@{thms} for most purposes.
wenzelm@39164
   401
wenzelm@38980
   402
* ML structure Unsynchronized never opened, not even in Isar
wenzelm@38980
   403
interaction mode as before.  Old Unsynchronized.set etc. have been
wenzelm@38980
   404
discontinued -- use plain := instead.  This should be *rare* anyway,
wenzelm@38980
   405
since modern tools always work via official context data, notably
wenzelm@38980
   406
configuration options.
wenzelm@38980
   407
wenzelm@37868
   408
* ML antiquotations @{theory} and @{theory_ref} refer to named
wenzelm@37868
   409
theories from the ancestry of the current context, not any accidental
wenzelm@37868
   410
theory loader state as before.  Potential INCOMPATIBILITY, subtle
wenzelm@37868
   411
change in semantics.
wenzelm@37868
   412
wenzelm@39239
   413
* Parallel and asynchronous execution requires special care concerning
wenzelm@39239
   414
interrupts.  Structure Exn provides some convenience functions that
wenzelm@39239
   415
avoid working directly with raw Interrupt.  User code must not absorb
wenzelm@39239
   416
interrupts -- intermediate handling (for cleanup etc.) needs to be
wenzelm@39239
   417
followed by re-raising of the original exception.  Another common
wenzelm@39239
   418
source of mistakes are "handle _" patterns, which make the meaning of
wenzelm@39239
   419
the program subject to physical effects of the environment.
wenzelm@39239
   420
wenzelm@37868
   421
wenzelm@38470
   422
*** System ***
wenzelm@38470
   423
wenzelm@38470
   424
* Discontinued support for Poly/ML 5.0 and 5.1 versions.
wenzelm@38470
   425
wenzelm@38470
   426
wenzelm@37868
   427
wenzelm@37144
   428
New in Isabelle2009-2 (June 2010)
wenzelm@37144
   429
---------------------------------
haftmann@33993
   430
wenzelm@35260
   431
*** General ***
wenzelm@35260
   432
wenzelm@35436
   433
* Authentic syntax for *all* logical entities (type classes, type
wenzelm@35436
   434
constructors, term constants): provides simple and robust
wenzelm@35436
   435
correspondence between formal entities and concrete syntax.  Within
wenzelm@35436
   436
the parse tree / AST representations, "constants" are decorated by
wenzelm@35436
   437
their category (class, type, const) and spelled out explicitly with
wenzelm@35436
   438
their full internal name.
wenzelm@35436
   439
wenzelm@35436
   440
Substantial INCOMPATIBILITY concerning low-level syntax declarations
wenzelm@35436
   441
and translations (translation rules and translation functions in ML).
wenzelm@35436
   442
Some hints on upgrading:
wenzelm@35260
   443
wenzelm@35260
   444
  - Many existing uses of 'syntax' and 'translations' can be replaced
wenzelm@35436
   445
    by more modern 'type_notation', 'notation' and 'abbreviation',
wenzelm@35436
   446
    which are independent of this issue.
wenzelm@35260
   447
wenzelm@35260
   448
  - 'translations' require markup within the AST; the term syntax
wenzelm@35260
   449
    provides the following special forms:
wenzelm@35260
   450
wenzelm@35260
   451
      CONST c   -- produces syntax version of constant c from context
wenzelm@35261
   452
      XCONST c  -- literally c, checked as constant from context
wenzelm@35261
   453
      c         -- literally c, if declared by 'syntax'
wenzelm@35261
   454
wenzelm@35261
   455
    Plain identifiers are treated as AST variables -- occasionally the
wenzelm@35261
   456
    system indicates accidental variables via the error "rhs contains
wenzelm@35261
   457
    extra variables".
wenzelm@35260
   458
wenzelm@35436
   459
    Type classes and type constructors are marked according to their
wenzelm@35436
   460
    concrete syntax.  Some old translations rules need to be written
wenzelm@35436
   461
    for the "type" category, using type constructor application
wenzelm@35436
   462
    instead of pseudo-term application of the default category
wenzelm@35436
   463
    "logic".
wenzelm@35436
   464
wenzelm@35260
   465
  - 'parse_translation' etc. in ML may use the following
wenzelm@35260
   466
    antiquotations:
wenzelm@35260
   467
wenzelm@35436
   468
      @{class_syntax c}   -- type class c within parse tree / AST
wenzelm@35436
   469
      @{term_syntax c}    -- type constructor c within parse tree / AST
wenzelm@35260
   470
      @{const_syntax c}   -- ML version of "CONST c" above
wenzelm@35260
   471
      @{syntax_const c}   -- literally c (checked wrt. 'syntax' declarations)
wenzelm@35260
   472
wenzelm@35436
   473
  - Literal types within 'typed_print_translations', i.e. those *not*
wenzelm@35436
   474
    represented as pseudo-terms are represented verbatim.  Use @{class
wenzelm@35436
   475
    c} or @{type_name c} here instead of the above syntax
wenzelm@35436
   476
    antiquotations.
wenzelm@35436
   477
wenzelm@35260
   478
Note that old non-authentic syntax was based on unqualified base
wenzelm@35436
   479
names, so all of the above "constant" names would coincide.  Recall
wenzelm@35436
   480
that 'print_syntax' and ML_command "set Syntax.trace_ast" help to
wenzelm@35436
   481
diagnose syntax problems.
wenzelm@35260
   482
wenzelm@35351
   483
* Type constructors admit general mixfix syntax, not just infix.
wenzelm@35351
   484
wenzelm@36508
   485
* Concrete syntax may be attached to local entities without a proof
wenzelm@36508
   486
body, too.  This works via regular mixfix annotations for 'fix',
wenzelm@36508
   487
'def', 'obtain' etc. or via the explicit 'write' command, which is
wenzelm@36508
   488
similar to the 'notation' command in theory specifications.
wenzelm@36508
   489
wenzelm@37351
   490
* Discontinued unnamed infix syntax (legacy feature for many years) --
wenzelm@37351
   491
need to specify constant name and syntax separately.  Internal ML
wenzelm@37351
   492
datatype constructors have been renamed from InfixName to Infix etc.
wenzelm@37351
   493
Minor INCOMPATIBILITY.
wenzelm@37351
   494
wenzelm@37351
   495
* Schematic theorem statements need to be explicitly markup as such,
wenzelm@37351
   496
via commands 'schematic_lemma', 'schematic_theorem',
wenzelm@37351
   497
'schematic_corollary'.  Thus the relevance of the proof is made
wenzelm@37351
   498
syntactically clear, which impacts performance in a parallel or
wenzelm@37351
   499
asynchronous interactive environment.  Minor INCOMPATIBILITY.
wenzelm@37351
   500
wenzelm@35613
   501
* Use of cumulative prems via "!" in some proof methods has been
wenzelm@37351
   502
discontinued (old legacy feature).
wenzelm@35613
   503
boehmes@35979
   504
* References 'trace_simp' and 'debug_simp' have been replaced by
wenzelm@36857
   505
configuration options stored in the context. Enabling tracing (the
wenzelm@36857
   506
case of debugging is similar) in proofs works via
wenzelm@36857
   507
wenzelm@36857
   508
  using [[trace_simp = true]]
wenzelm@36857
   509
wenzelm@36857
   510
Tracing is then active for all invocations of the simplifier in
wenzelm@36857
   511
subsequent goal refinement steps. Tracing may also still be enabled or
wenzelm@36857
   512
disabled via the ProofGeneral settings menu.
boehmes@35979
   513
wenzelm@36177
   514
* Separate commands 'hide_class', 'hide_type', 'hide_const',
wenzelm@36177
   515
'hide_fact' replace the former 'hide' KIND command.  Minor
wenzelm@36177
   516
INCOMPATIBILITY.
wenzelm@36177
   517
wenzelm@37298
   518
* Improved parallelism of proof term normalization: usedir -p2 -q0 is
wenzelm@37298
   519
more efficient than combinations with -q1 or -q2.
wenzelm@37298
   520
wenzelm@35260
   521
haftmann@34170
   522
*** Pure ***
haftmann@34170
   523
wenzelm@37351
   524
* Proofterms record type-class reasoning explicitly, using the
wenzelm@37351
   525
"unconstrain" operation internally.  This eliminates all sort
wenzelm@37351
   526
constraints from a theorem and proof, introducing explicit
wenzelm@37351
   527
OFCLASS-premises.  On the proof term level, this operation is
wenzelm@37351
   528
automatically applied at theorem boundaries, such that closed proofs
wenzelm@37351
   529
are always free of sort constraints.  INCOMPATIBILITY for tools that
wenzelm@37351
   530
inspect proof terms.
haftmann@36147
   531
wenzelm@35765
   532
* Local theory specifications may depend on extra type variables that
wenzelm@35765
   533
are not present in the result type -- arguments TYPE('a) :: 'a itself
wenzelm@35765
   534
are added internally.  For example:
wenzelm@35765
   535
wenzelm@35765
   536
  definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
wenzelm@35765
   537
wenzelm@37351
   538
* Predicates of locales introduced by classes carry a mandatory
wenzelm@37351
   539
"class" prefix.  INCOMPATIBILITY.
wenzelm@37351
   540
wenzelm@37351
   541
* Vacuous class specifications observe default sort.  INCOMPATIBILITY.
wenzelm@37351
   542
wenzelm@37351
   543
* Old 'axclass' command has been discontinued.  INCOMPATIBILITY, use
wenzelm@37351
   544
'class' instead.
wenzelm@37351
   545
wenzelm@37351
   546
* Command 'code_reflect' allows to incorporate generated ML code into
wenzelm@37351
   547
runtime environment; replaces immature code_datatype antiquotation.
wenzelm@37351
   548
INCOMPATIBILITY.
wenzelm@37351
   549
wenzelm@37351
   550
* Code generator: simple concept for abstract datatypes obeying
wenzelm@37351
   551
invariants.
wenzelm@37351
   552
wenzelm@36857
   553
* Code generator: details of internal data cache have no impact on the
wenzelm@36857
   554
user space functionality any longer.
wenzelm@36857
   555
wenzelm@37351
   556
* Methods "unfold_locales" and "intro_locales" ignore non-locale
wenzelm@37351
   557
subgoals.  This is more appropriate for interpretations with 'where'.
wenzelm@36857
   558
INCOMPATIBILITY.
haftmann@34170
   559
wenzelm@36356
   560
* Command 'example_proof' opens an empty proof body.  This allows to
wenzelm@36356
   561
experiment with Isar, without producing any persistent result.
wenzelm@36356
   562
wenzelm@35413
   563
* Commands 'type_notation' and 'no_type_notation' declare type syntax
wenzelm@35413
   564
within a local theory context, with explicit checking of the
wenzelm@35413
   565
constructors involved (in contrast to the raw 'syntax' versions).
wenzelm@35413
   566
wenzelm@36178
   567
* Commands 'types' and 'typedecl' now work within a local theory
wenzelm@36178
   568
context -- without introducing dependencies on parameters or
wenzelm@36178
   569
assumptions, which is not possible in Isabelle/Pure.
wenzelm@35681
   570
wenzelm@36857
   571
* Command 'defaultsort' has been renamed to 'default_sort', it works
wenzelm@36857
   572
within a local theory context.  Minor INCOMPATIBILITY.
wenzelm@36454
   573
haftmann@34170
   574
haftmann@33993
   575
*** HOL ***
haftmann@33993
   576
wenzelm@37351
   577
* Command 'typedef' now works within a local theory context -- without
wenzelm@37351
   578
introducing dependencies on parameters or assumptions, which is not
wenzelm@37351
   579
possible in Isabelle/Pure/HOL.  Note that the logical environment may
wenzelm@37351
   580
contain multiple interpretations of local typedefs (with different
wenzelm@37351
   581
non-emptiness proofs), even in a global theory context.
wenzelm@37351
   582
wenzelm@37351
   583
* New package for quotient types.  Commands 'quotient_type' and
wenzelm@37351
   584
'quotient_definition' may be used for defining types and constants by
wenzelm@37351
   585
quotient constructions.  An example is the type of integers created by
wenzelm@37351
   586
quotienting pairs of natural numbers:
wenzelm@37380
   587
wenzelm@37351
   588
  fun
wenzelm@37380
   589
    intrel :: "(nat * nat) => (nat * nat) => bool"
wenzelm@37351
   590
  where
wenzelm@37351
   591
    "intrel (x, y) (u, v) = (x + v = u + y)"
wenzelm@37351
   592
wenzelm@37380
   593
  quotient_type int = "nat * nat" / intrel
wenzelm@37351
   594
    by (auto simp add: equivp_def expand_fun_eq)
wenzelm@37380
   595
wenzelm@37351
   596
  quotient_definition
wenzelm@37351
   597
    "0::int" is "(0::nat, 0::nat)"
wenzelm@37351
   598
wenzelm@37351
   599
The method "lifting" can be used to lift of theorems from the
wenzelm@37351
   600
underlying "raw" type to the quotient type.  The example
wenzelm@37351
   601
src/HOL/Quotient_Examples/FSet.thy includes such a quotient
wenzelm@37351
   602
construction and provides a reasoning infrastructure for finite sets.
wenzelm@37351
   603
wenzelm@37351
   604
* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid
wenzelm@37351
   605
clash with new theory Quotient in Main HOL.
wenzelm@37351
   606
wenzelm@37351
   607
* Moved the SMT binding into the main HOL session, eliminating
wenzelm@37351
   608
separate HOL-SMT session.
wenzelm@37351
   609
haftmann@37020
   610
* List membership infix mem operation is only an input abbreviation.
haftmann@37020
   611
INCOMPATIBILITY.
haftmann@37020
   612
wenzelm@37144
   613
* Theory Library/Word.thy has been removed.  Use library Word/Word.thy
wenzelm@37144
   614
for future developements; former Library/Word.thy is still present in
wenzelm@37144
   615
the AFP entry RSAPPS.
haftmann@36963
   616
wenzelm@36857
   617
* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no
wenzelm@36857
   618
longer shadowed.  INCOMPATIBILITY.
haftmann@36808
   619
huffman@36836
   620
* Dropped theorem duplicate comp_arith; use semiring_norm instead.
huffman@36836
   621
INCOMPATIBILITY.
huffman@36836
   622
huffman@36836
   623
* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
huffman@36836
   624
INCOMPATIBILITY.
haftmann@36714
   625
wenzelm@36857
   626
* Dropped normalizing_semiring etc; use the facts in semiring classes
wenzelm@36857
   627
instead.  INCOMPATIBILITY.
wenzelm@36857
   628
huffman@36979
   629
* Dropped several real-specific versions of lemmas about floor and
wenzelm@37351
   630
ceiling; use the generic lemmas from theory "Archimedean_Field"
wenzelm@37351
   631
instead.  INCOMPATIBILITY.
huffman@36979
   632
huffman@36979
   633
  floor_number_of_eq         ~> floor_number_of
huffman@36979
   634
  le_floor_eq_number_of      ~> number_of_le_floor
huffman@36979
   635
  le_floor_eq_zero           ~> zero_le_floor
huffman@36979
   636
  le_floor_eq_one            ~> one_le_floor
huffman@36979
   637
  floor_less_eq_number_of    ~> floor_less_number_of
huffman@36979
   638
  floor_less_eq_zero         ~> floor_less_zero
huffman@36979
   639
  floor_less_eq_one          ~> floor_less_one
huffman@36979
   640
  less_floor_eq_number_of    ~> number_of_less_floor
huffman@36979
   641
  less_floor_eq_zero         ~> zero_less_floor
huffman@36979
   642
  less_floor_eq_one          ~> one_less_floor
huffman@36979
   643
  floor_le_eq_number_of      ~> floor_le_number_of
huffman@36979
   644
  floor_le_eq_zero           ~> floor_le_zero
huffman@36979
   645
  floor_le_eq_one            ~> floor_le_one
huffman@36979
   646
  floor_subtract_number_of   ~> floor_diff_number_of
huffman@36979
   647
  floor_subtract_one         ~> floor_diff_one
huffman@36979
   648
  ceiling_number_of_eq       ~> ceiling_number_of
huffman@36979
   649
  ceiling_le_eq_number_of    ~> ceiling_le_number_of
huffman@36979
   650
  ceiling_le_zero_eq         ~> ceiling_le_zero
huffman@36979
   651
  ceiling_le_eq_one          ~> ceiling_le_one
huffman@36979
   652
  less_ceiling_eq_number_of  ~> number_of_less_ceiling
huffman@36979
   653
  less_ceiling_eq_zero       ~> zero_less_ceiling
huffman@36979
   654
  less_ceiling_eq_one        ~> one_less_ceiling
huffman@36979
   655
  ceiling_less_eq_number_of  ~> ceiling_less_number_of
huffman@36979
   656
  ceiling_less_eq_zero       ~> ceiling_less_zero
huffman@36979
   657
  ceiling_less_eq_one        ~> ceiling_less_one
huffman@36979
   658
  le_ceiling_eq_number_of    ~> number_of_le_ceiling
huffman@36979
   659
  le_ceiling_eq_zero         ~> zero_le_ceiling
huffman@36979
   660
  le_ceiling_eq_one          ~> one_le_ceiling
huffman@36979
   661
  ceiling_subtract_number_of ~> ceiling_diff_number_of
huffman@36979
   662
  ceiling_subtract_one       ~> ceiling_diff_one
huffman@36979
   663
wenzelm@37144
   664
* Theory "Finite_Set": various folding_XXX locales facilitate the
wenzelm@36857
   665
application of the various fold combinators on finite sets.
wenzelm@36857
   666
wenzelm@36857
   667
* Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"
wenzelm@36857
   668
provides abstract red-black tree type which is backed by "RBT_Impl" as
wenzelm@36857
   669
implementation.  INCOMPATIBILTY.
haftmann@36147
   670
huffman@36830
   671
* Theory Library/Coinductive_List has been removed -- superseded by
wenzelm@35763
   672
AFP/thys/Coinductive.
wenzelm@35763
   673
huffman@36829
   674
* Theory PReal, including the type "preal" and related operations, has
huffman@36829
   675
been removed.  INCOMPATIBILITY.
huffman@36829
   676
wenzelm@37380
   677
* Real: new development using Cauchy Sequences.
wenzelm@37380
   678
wenzelm@37351
   679
* Split off theory "Big_Operators" containing setsum, setprod,
wenzelm@37351
   680
Inf_fin, Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.
wenzelm@36857
   681
wenzelm@36857
   682
* Theory "Rational" renamed to "Rat", for consistency with "Nat",
wenzelm@36857
   683
"Int" etc.  INCOMPATIBILITY.
wenzelm@36857
   684
wenzelm@37351
   685
* Constant Rat.normalize needs to be qualified.  INCOMPATIBILITY.
wenzelm@37143
   686
wenzelm@36857
   687
* New set of rules "ac_simps" provides combined assoc / commute
wenzelm@36857
   688
rewrites for all interpretations of the appropriate generic locales.
wenzelm@36857
   689
wenzelm@36857
   690
* Renamed theory "OrderedGroup" to "Groups" and split theory
wenzelm@36857
   691
"Ring_and_Field" into theories "Rings" and "Fields"; for more
wenzelm@36857
   692
appropriate and more consistent names suitable for name prefixes
wenzelm@36857
   693
within the HOL theories.  INCOMPATIBILITY.
haftmann@35050
   694
haftmann@35084
   695
* Some generic constants have been put to appropriate theories:
wenzelm@36857
   696
  - less_eq, less: Orderings
wenzelm@36857
   697
  - zero, one, plus, minus, uminus, times, abs, sgn: Groups
wenzelm@36857
   698
  - inverse, divide: Rings
haftmann@35084
   699
INCOMPATIBILITY.
haftmann@35084
   700
wenzelm@36857
   701
* More consistent naming of type classes involving orderings (and
wenzelm@36857
   702
lattices):
haftmann@35027
   703
haftmann@35027
   704
    lower_semilattice                   ~> semilattice_inf
haftmann@35027
   705
    upper_semilattice                   ~> semilattice_sup
haftmann@35027
   706
haftmann@35027
   707
    dense_linear_order                  ~> dense_linorder
haftmann@35027
   708
haftmann@35027
   709
    pordered_ab_group_add               ~> ordered_ab_group_add
haftmann@35027
   710
    pordered_ab_group_add_abs           ~> ordered_ab_group_add_abs
haftmann@35027
   711
    pordered_ab_semigroup_add           ~> ordered_ab_semigroup_add
haftmann@35027
   712
    pordered_ab_semigroup_add_imp_le    ~> ordered_ab_semigroup_add_imp_le
haftmann@35027
   713
    pordered_cancel_ab_semigroup_add    ~> ordered_cancel_ab_semigroup_add
haftmann@35027
   714
    pordered_cancel_comm_semiring       ~> ordered_cancel_comm_semiring
haftmann@35027
   715
    pordered_cancel_semiring            ~> ordered_cancel_semiring
haftmann@35027
   716
    pordered_comm_monoid_add            ~> ordered_comm_monoid_add
haftmann@35027
   717
    pordered_comm_ring                  ~> ordered_comm_ring
haftmann@35027
   718
    pordered_comm_semiring              ~> ordered_comm_semiring
haftmann@35027
   719
    pordered_ring                       ~> ordered_ring
haftmann@35027
   720
    pordered_ring_abs                   ~> ordered_ring_abs
haftmann@35027
   721
    pordered_semiring                   ~> ordered_semiring
haftmann@35027
   722
haftmann@35027
   723
    ordered_ab_group_add                ~> linordered_ab_group_add
haftmann@35027
   724
    ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add
haftmann@35027
   725
    ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add
haftmann@35027
   726
    ordered_comm_semiring_strict        ~> linordered_comm_semiring_strict
haftmann@35027
   727
    ordered_field                       ~> linordered_field
haftmann@35027
   728
    ordered_field_no_lb                 ~> linordered_field_no_lb
haftmann@35027
   729
    ordered_field_no_ub                 ~> linordered_field_no_ub
haftmann@35027
   730
    ordered_field_dense_linear_order    ~> dense_linordered_field
haftmann@35027
   731
    ordered_idom                        ~> linordered_idom
haftmann@35027
   732
    ordered_ring                        ~> linordered_ring
haftmann@35027
   733
    ordered_ring_le_cancel_factor       ~> linordered_ring_le_cancel_factor
haftmann@35027
   734
    ordered_ring_less_cancel_factor     ~> linordered_ring_less_cancel_factor
haftmann@35027
   735
    ordered_ring_strict                 ~> linordered_ring_strict
haftmann@35027
   736
    ordered_semidom                     ~> linordered_semidom
haftmann@35027
   737
    ordered_semiring                    ~> linordered_semiring
haftmann@35027
   738
    ordered_semiring_1                  ~> linordered_semiring_1
haftmann@35027
   739
    ordered_semiring_1_strict           ~> linordered_semiring_1_strict
haftmann@35027
   740
    ordered_semiring_strict             ~> linordered_semiring_strict
haftmann@35027
   741
wenzelm@36857
   742
  The following slightly odd type classes have been moved to a
wenzelm@37351
   743
  separate theory Library/Lattice_Algebras:
haftmann@35032
   744
haftmann@35032
   745
    lordered_ab_group_add               ~> lattice_ab_group_add
haftmann@35032
   746
    lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
haftmann@35032
   747
    lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
haftmann@35032
   748
    lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
haftmann@35032
   749
    lordered_ring                       ~> lattice_ring
haftmann@35032
   750
haftmann@35027
   751
INCOMPATIBILITY.
haftmann@35027
   752
haftmann@36416
   753
* Refined field classes:
wenzelm@36857
   754
  - classes division_ring_inverse_zero, field_inverse_zero,
wenzelm@36857
   755
    linordered_field_inverse_zero include rule inverse 0 = 0 --
wenzelm@36857
   756
    subsumes former division_by_zero class;
wenzelm@36857
   757
  - numerous lemmas have been ported from field to division_ring.
wenzelm@36857
   758
INCOMPATIBILITY.
haftmann@36416
   759
haftmann@36416
   760
* Refined algebra theorem collections:
wenzelm@36857
   761
  - dropped theorem group group_simps, use algebra_simps instead;
wenzelm@36857
   762
  - dropped theorem group ring_simps, use field_simps instead;
wenzelm@36857
   763
  - proper theorem collection field_simps subsumes former theorem
wenzelm@36857
   764
    groups field_eq_simps and field_simps;
wenzelm@36857
   765
  - dropped lemma eq_minus_self_iff which is a duplicate for
wenzelm@36857
   766
    equal_neg_zero.
wenzelm@36857
   767
INCOMPATIBILITY.
wenzelm@35009
   768
wenzelm@35009
   769
* Theory Finite_Set and List: some lemmas have been generalized from
wenzelm@34076
   770
sets to lattices:
wenzelm@34076
   771
haftmann@34007
   772
  fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf
haftmann@34007
   773
  fun_left_comm_idem_union      ~> fun_left_comm_idem_sup
haftmann@34007
   774
  inter_Inter_fold_inter        ~> inf_Inf_fold_inf
haftmann@34007
   775
  union_Union_fold_union        ~> sup_Sup_fold_sup
haftmann@34007
   776
  Inter_fold_inter              ~> Inf_fold_inf
haftmann@34007
   777
  Union_fold_union              ~> Sup_fold_sup
haftmann@34007
   778
  inter_INTER_fold_inter        ~> inf_INFI_fold_inf
haftmann@34007
   779
  union_UNION_fold_union        ~> sup_SUPR_fold_sup
haftmann@34007
   780
  INTER_fold_inter              ~> INFI_fold_inf
haftmann@34007
   781
  UNION_fold_union              ~> SUPR_fold_sup
haftmann@34007
   782
wenzelm@37351
   783
* Theory "Complete_Lattice": lemmas top_def and bot_def have been
haftmann@36416
   784
replaced by the more convenient lemmas Inf_empty and Sup_empty.
haftmann@36416
   785
Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
haftmann@36416
   786
by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace
haftmann@36416
   787
former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right
haftmann@36416
   788
subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.
haftmann@36416
   789
wenzelm@36857
   790
* Reorganized theory Multiset: swapped notation of pointwise and
wenzelm@36857
   791
multiset order:
wenzelm@37351
   792
wenzelm@36857
   793
  - pointwise ordering is instance of class order with standard syntax
wenzelm@36857
   794
    <= and <;
wenzelm@36857
   795
  - multiset ordering has syntax <=# and <#; partial order properties
wenzelm@36857
   796
    are provided by means of interpretation with prefix
wenzelm@36857
   797
    multiset_order;
wenzelm@36857
   798
  - less duplication, less historical organization of sections,
wenzelm@36857
   799
    conversion from associations lists to multisets, rudimentary code
wenzelm@36857
   800
    generation;
wenzelm@36857
   801
  - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,
wenzelm@36857
   802
    if needed.
wenzelm@37351
   803
nipkow@36903
   804
Renamed:
wenzelm@37351
   805
wenzelm@37351
   806
  multiset_eq_conv_count_eq  ~>  multiset_ext_iff
wenzelm@37351
   807
  multi_count_ext  ~>  multiset_ext
wenzelm@37351
   808
  diff_union_inverse2  ~>  diff_union_cancelR
wenzelm@37351
   809
wenzelm@36857
   810
INCOMPATIBILITY.
haftmann@36416
   811
nipkow@36903
   812
* Theory Permutation: replaced local "remove" by List.remove1.
nipkow@36903
   813
haftmann@36416
   814
* Code generation: ML and OCaml code is decorated with signatures.
haftmann@36416
   815
wenzelm@35009
   816
* Theory List: added transpose.
wenzelm@35009
   817
huffman@35810
   818
* Library/Nat_Bijection.thy is a collection of bijective functions
huffman@35810
   819
between nat and other types, which supersedes the older libraries
huffman@35810
   820
Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy.  INCOMPATIBILITY.
huffman@35810
   821
huffman@35810
   822
  Constants:
huffman@35810
   823
  Nat_Int_Bij.nat2_to_nat         ~> prod_encode
huffman@35810
   824
  Nat_Int_Bij.nat_to_nat2         ~> prod_decode
huffman@35810
   825
  Nat_Int_Bij.int_to_nat_bij      ~> int_encode
huffman@35810
   826
  Nat_Int_Bij.nat_to_int_bij      ~> int_decode
huffman@35810
   827
  Countable.pair_encode           ~> prod_encode
huffman@35810
   828
  NatIso.prod2nat                 ~> prod_encode
huffman@35810
   829
  NatIso.nat2prod                 ~> prod_decode
huffman@35810
   830
  NatIso.sum2nat                  ~> sum_encode
huffman@35810
   831
  NatIso.nat2sum                  ~> sum_decode
huffman@35810
   832
  NatIso.list2nat                 ~> list_encode
huffman@35810
   833
  NatIso.nat2list                 ~> list_decode
huffman@35810
   834
  NatIso.set2nat                  ~> set_encode
huffman@35810
   835
  NatIso.nat2set                  ~> set_decode
huffman@35810
   836
huffman@35810
   837
  Lemmas:
huffman@35810
   838
  Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_decode
huffman@35810
   839
  Nat_Int_Bij.nat2_to_nat_inj     ~> inj_prod_encode
huffman@35810
   840
  Nat_Int_Bij.nat2_to_nat_surj    ~> surj_prod_encode
huffman@35810
   841
  Nat_Int_Bij.nat_to_nat2_inj     ~> inj_prod_decode
huffman@35810
   842
  Nat_Int_Bij.nat_to_nat2_surj    ~> surj_prod_decode
huffman@35810
   843
  Nat_Int_Bij.i2n_n2i_id          ~> int_encode_inverse
huffman@35810
   844
  Nat_Int_Bij.n2i_i2n_id          ~> int_decode_inverse
huffman@35810
   845
  Nat_Int_Bij.surj_nat_to_int_bij ~> surj_int_encode
huffman@35810
   846
  Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode
huffman@35810
   847
  Nat_Int_Bij.inj_nat_to_int_bij  ~> inj_int_encode
huffman@35810
   848
  Nat_Int_Bij.inj_int_to_nat_bij  ~> inj_int_decode
huffman@35810
   849
  Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode
huffman@35810
   850
  Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode
huffman@35810
   851
blanchet@36929
   852
* Sledgehammer:
blanchet@36929
   853
  - Renamed ATP commands:
blanchet@36929
   854
    atp_info     ~> sledgehammer running_atps
blanchet@36929
   855
    atp_kill     ~> sledgehammer kill_atps
blanchet@36929
   856
    atp_messages ~> sledgehammer messages
blanchet@36929
   857
    atp_minimize ~> sledgehammer minimize
blanchet@36929
   858
    print_atps   ~> sledgehammer available_atps
blanchet@36929
   859
    INCOMPATIBILITY.
blanchet@36929
   860
  - Added user's manual ("isabelle doc sledgehammer").
blanchet@36929
   861
  - Added option syntax and "sledgehammer_params" to customize
blanchet@36929
   862
    Sledgehammer's behavior.  See the manual for details.
blanchet@36929
   863
  - Modified the Isar proof reconstruction code so that it produces
blanchet@36929
   864
    direct proofs rather than proofs by contradiction.  (This feature
blanchet@36929
   865
    is still experimental.)
blanchet@36929
   866
  - Made Isar proof reconstruction work for SPASS, remote ATPs, and in
blanchet@36929
   867
    full-typed mode.
blanchet@36929
   868
  - Added support for TPTP syntax for SPASS via the "spass_tptp" ATP.
blanchet@36929
   869
blanchet@36928
   870
* Nitpick:
blanchet@36928
   871
  - Added and implemented "binary_ints" and "bits" options.
blanchet@36928
   872
  - Added "std" option and implemented support for nonstandard models.
blanchet@36928
   873
  - Added and implemented "finitize" option to improve the precision
blanchet@36928
   874
    of infinite datatypes based on a monotonicity analysis.
blanchet@36928
   875
  - Added support for quotient types.
blanchet@36928
   876
  - Added support for "specification" and "ax_specification"
blanchet@36928
   877
    constructs.
blanchet@36928
   878
  - Added support for local definitions (for "function" and
blanchet@36928
   879
    "termination" proofs).
blanchet@36928
   880
  - Added support for term postprocessors.
blanchet@36928
   881
  - Optimized "Multiset.multiset" and "FinFun.finfun".
blanchet@36928
   882
  - Improved efficiency of "destroy_constrs" optimization.
blanchet@36928
   883
  - Fixed soundness bugs related to "destroy_constrs" optimization and
blanchet@36928
   884
    record getters.
blanchet@37272
   885
  - Fixed soundness bug related to higher-order constructors.
blanchet@37272
   886
  - Fixed soundness bug when "full_descrs" is enabled.
blanchet@36928
   887
  - Improved precision of set constructs.
blanchet@37260
   888
  - Added "atoms" option.
blanchet@36928
   889
  - Added cache to speed up repeated Kodkod invocations on the same
blanchet@36928
   890
    problems.
blanchet@36928
   891
  - Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and
blanchet@36928
   892
    "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and
blanchet@36928
   893
    "SAT4J_Light".  INCOMPATIBILITY.
blanchet@36928
   894
  - Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
blanchet@36928
   895
    "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.
blanchet@37264
   896
  - Removed "nitpick_intro" attribute.  INCOMPATIBILITY.
blanchet@36928
   897
berghofe@37361
   898
* Method "induct" now takes instantiations of the form t, where t is not
berghofe@37361
   899
  a variable, as a shorthand for "x == t", where x is a fresh variable.
berghofe@37361
   900
  If this is not intended, t has to be enclosed in parentheses.
berghofe@37361
   901
  By default, the equalities generated by definitional instantiations
berghofe@37361
   902
  are pre-simplified, which may cause parameters of inductive cases
berghofe@37361
   903
  to disappear, or may even delete some of the inductive cases.
berghofe@37361
   904
  Use "induct (no_simp)" instead of "induct" to restore the old
berghofe@37361
   905
  behaviour. The (no_simp) option is also understood by the "cases"
berghofe@37361
   906
  and "nominal_induct" methods, which now perform pre-simplification, too.
berghofe@37361
   907
  INCOMPATIBILITY.
berghofe@37361
   908
haftmann@33993
   909
huffman@36828
   910
*** HOLCF ***
huffman@36828
   911
huffman@36828
   912
* Variable names in lemmas generated by the domain package have
huffman@36828
   913
changed; the naming scheme is now consistent with the HOL datatype
huffman@36828
   914
package.  Some proof scripts may be affected, INCOMPATIBILITY.
huffman@36828
   915
huffman@36828
   916
* The domain package no longer defines the function "foo_copy" for
huffman@36828
   917
recursive domain "foo".  The reach lemma is now stated directly in
huffman@36828
   918
terms of "foo_take".  Lemmas and proofs that mention "foo_copy" must
huffman@36828
   919
be reformulated in terms of "foo_take", INCOMPATIBILITY.
huffman@36828
   920
huffman@36828
   921
* Most definedness lemmas generated by the domain package (previously
huffman@36828
   922
of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form
huffman@36828
   923
like "foo$x = UU <-> x = UU", which works better as a simp rule.
wenzelm@37351
   924
Proofs that used definedness lemmas as intro rules may break,
huffman@36828
   925
potential INCOMPATIBILITY.
huffman@36828
   926
huffman@36828
   927
* Induction and casedist rules generated by the domain package now
huffman@36828
   928
declare proper case_names (one called "bottom", and one named for each
huffman@36828
   929
constructor).  INCOMPATIBILITY.
huffman@36828
   930
huffman@36828
   931
* For mutually-recursive domains, separate "reach" and "take_lemma"
huffman@36828
   932
rules are generated for each domain, INCOMPATIBILITY.
huffman@36828
   933
huffman@36828
   934
  foo_bar.reach       ~> foo.reach  bar.reach
huffman@36828
   935
  foo_bar.take_lemmas ~> foo.take_lemma  bar.take_lemma
huffman@36828
   936
huffman@36828
   937
* Some lemmas generated by the domain package have been renamed for
huffman@36828
   938
consistency with the datatype package, INCOMPATIBILITY.
huffman@36828
   939
huffman@36828
   940
  foo.ind        ~> foo.induct
huffman@36828
   941
  foo.finite_ind ~> foo.finite_induct
huffman@36828
   942
  foo.coind      ~> foo.coinduct
huffman@36828
   943
  foo.casedist   ~> foo.exhaust
huffman@36828
   944
  foo.exhaust    ~> foo.nchotomy
huffman@36828
   945
huffman@36828
   946
* For consistency with other definition packages, the fixrec package
huffman@36828
   947
now generates qualified theorem names, INCOMPATIBILITY.
huffman@36828
   948
huffman@36828
   949
  foo_simps  ~> foo.simps
huffman@36828
   950
  foo_unfold ~> foo.unfold
huffman@36828
   951
  foo_induct ~> foo.induct
huffman@36828
   952
huffman@37087
   953
* The "fixrec_simp" attribute has been removed.  The "fixrec_simp"
huffman@37087
   954
method and internal fixrec proofs now use the default simpset instead.
huffman@37087
   955
INCOMPATIBILITY.
huffman@37087
   956
huffman@36828
   957
* The "contlub" predicate has been removed.  Proof scripts should use
huffman@36828
   958
lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.
huffman@36828
   959
huffman@36828
   960
* The "admw" predicate has been removed, INCOMPATIBILITY.
huffman@36828
   961
huffman@36828
   962
* The constants cpair, cfst, and csnd have been removed in favor of
huffman@36828
   963
Pair, fst, and snd from Isabelle/HOL, INCOMPATIBILITY.
huffman@36828
   964
huffman@36828
   965
haftmann@33993
   966
*** ML ***
haftmann@33993
   967
wenzelm@37351
   968
* Antiquotations for basic formal entities:
wenzelm@37351
   969
wenzelm@37351
   970
    @{class NAME}         -- type class
wenzelm@37351
   971
    @{class_syntax NAME}  -- syntax representation of the above
wenzelm@37351
   972
wenzelm@37351
   973
    @{type_name NAME}     -- logical type
wenzelm@37351
   974
    @{type_abbrev NAME}   -- type abbreviation
wenzelm@37351
   975
    @{nonterminal NAME}   -- type of concrete syntactic category
wenzelm@37351
   976
    @{type_syntax NAME}   -- syntax representation of any of the above
wenzelm@37351
   977
wenzelm@37351
   978
    @{const_name NAME}    -- logical constant (INCOMPATIBILITY)
wenzelm@37351
   979
    @{const_abbrev NAME}  -- abbreviated constant
wenzelm@37351
   980
    @{const_syntax NAME}  -- syntax representation of any of the above
wenzelm@37351
   981
wenzelm@37351
   982
* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
wenzelm@37351
   983
syntax constant (cf. 'syntax' command).
wenzelm@37351
   984
wenzelm@37351
   985
* Antiquotation @{make_string} inlines a function to print arbitrary
wenzelm@37351
   986
values similar to the ML toplevel.  The result is compiler dependent
wenzelm@37351
   987
and may fall back on "?" in certain situations.
wenzelm@37351
   988
wenzelm@37351
   989
* Diagnostic commands 'ML_val' and 'ML_command' may refer to
wenzelm@37351
   990
antiquotations @{Isar.state} and @{Isar.goal}.  This replaces impure
wenzelm@37351
   991
Isar.state() and Isar.goal(), which belong to the old TTY loop and do
wenzelm@37351
   992
not work with the asynchronous Isar document model.
wenzelm@37351
   993
wenzelm@37351
   994
* Configuration options now admit dynamic default values, depending on
wenzelm@37351
   995
the context or even global references.
wenzelm@37351
   996
wenzelm@37351
   997
* SHA1.digest digests strings according to SHA-1 (see RFC 3174).  It
wenzelm@37351
   998
uses an efficient external library if available (for Poly/ML).
wenzelm@37351
   999
wenzelm@37144
  1000
* Renamed some important ML structures, while keeping the old names
wenzelm@37144
  1001
for some time as aliases within the structure Legacy:
wenzelm@37144
  1002
wenzelm@37144
  1003
  OuterKeyword  ~>  Keyword
wenzelm@37144
  1004
  OuterLex      ~>  Token
wenzelm@37144
  1005
  OuterParse    ~>  Parse
wenzelm@37144
  1006
  OuterSyntax   ~>  Outer_Syntax
wenzelm@37216
  1007
  PrintMode     ~>  Print_Mode
wenzelm@37144
  1008
  SpecParse     ~>  Parse_Spec
wenzelm@37216
  1009
  ThyInfo       ~>  Thy_Info
wenzelm@37216
  1010
  ThyLoad       ~>  Thy_Load
wenzelm@37216
  1011
  ThyOutput     ~>  Thy_Output
wenzelm@37145
  1012
  TypeInfer     ~>  Type_Infer
wenzelm@37144
  1013
wenzelm@37144
  1014
Note that "open Legacy" simplifies porting of sources, but forgetting
wenzelm@37144
  1015
to remove it again will complicate porting again in the future.
wenzelm@37144
  1016
wenzelm@37144
  1017
* Most operations that refer to a global context are named
wenzelm@37144
  1018
accordingly, e.g. Simplifier.global_context or
wenzelm@37144
  1019
ProofContext.init_global.  There are some situations where a global
wenzelm@37144
  1020
context actually works, but under normal circumstances one needs to
wenzelm@37144
  1021
pass the proper local context through the code!
wenzelm@37144
  1022
wenzelm@37144
  1023
* Discontinued old TheoryDataFun with its copy/init operation -- data
wenzelm@37144
  1024
needs to be pure.  Functor Theory_Data_PP retains the traditional
wenzelm@37144
  1025
Pretty.pp argument to merge, which is absent in the standard
wenzelm@37144
  1026
Theory_Data version.
wenzelm@36429
  1027
wenzelm@37144
  1028
* Sorts.certify_sort and derived "cert" operations for types and terms
wenzelm@37144
  1029
no longer minimize sorts.  Thus certification at the boundary of the
wenzelm@37144
  1030
inference kernel becomes invariant under addition of class relations,
wenzelm@37144
  1031
which is an important monotonicity principle.  Sorts are now minimized
wenzelm@37144
  1032
in the syntax layer only, at the boundary between the end-user and the
wenzelm@37144
  1033
system.  Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
wenzelm@37144
  1034
explicitly in rare situations.
wenzelm@37144
  1035
wenzelm@35021
  1036
* Renamed old-style Drule.standard to Drule.export_without_context, to
wenzelm@35021
  1037
emphasize that this is in no way a standard operation.
wenzelm@35021
  1038
INCOMPATIBILITY.
wenzelm@35021
  1039
wenzelm@34076
  1040
* Subgoal.FOCUS (and variants): resulting goal state is normalized as
wenzelm@34076
  1041
usual for resolution.  Rare INCOMPATIBILITY.
wenzelm@34076
  1042
wenzelm@35845
  1043
* Renamed varify/unvarify operations to varify_global/unvarify_global
wenzelm@35845
  1044
to emphasize that these only work in a global situation (which is
wenzelm@35845
  1045
quite rare).
wenzelm@35845
  1046
wenzelm@37144
  1047
* Curried take and drop in library.ML; negative length is interpreted
wenzelm@37144
  1048
as infinity (as in chop).  Subtle INCOMPATIBILITY.
wenzelm@36961
  1049
wenzelm@37351
  1050
* Proof terms: type substitutions on proof constants now use canonical
wenzelm@37351
  1051
order of type variables.  INCOMPATIBILITY for tools working with proof
wenzelm@37351
  1052
terms.
wenzelm@37351
  1053
wenzelm@37351
  1054
* Raw axioms/defs may no longer carry sort constraints, and raw defs
wenzelm@37351
  1055
may no longer carry premises.  User-level specifications are
wenzelm@37351
  1056
transformed accordingly by Thm.add_axiom/add_def.
wenzelm@37351
  1057
haftmann@33993
  1058
wenzelm@34238
  1059
*** System ***
wenzelm@34238
  1060
wenzelm@34238
  1061
* Discontinued special HOL_USEDIR_OPTIONS for the main HOL image;
wenzelm@34238
  1062
ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions.  Note that
wenzelm@34238
  1063
proof terms are enabled unconditionally in the new HOL-Proofs image.
wenzelm@34238
  1064
wenzelm@34255
  1065
* Discontinued old ISABELLE and ISATOOL environment settings (legacy
wenzelm@34255
  1066
feature since Isabelle2009).  Use ISABELLE_PROCESS and ISABELLE_TOOL,
wenzelm@34255
  1067
respectively.
wenzelm@34255
  1068
wenzelm@36201
  1069
* Old lib/scripts/polyml-platform is superseded by the
wenzelm@36201
  1070
ISABELLE_PLATFORM setting variable, which defaults to the 32 bit
wenzelm@36201
  1071
variant, even on a 64 bit machine.  The following example setting
wenzelm@36201
  1072
prefers 64 bit if available:
wenzelm@36201
  1073
wenzelm@36201
  1074
  ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
wenzelm@36201
  1075
wenzelm@37218
  1076
* The preliminary Isabelle/jEdit application demonstrates the emerging
wenzelm@37218
  1077
Isabelle/Scala layer for advanced prover interaction and integration.
wenzelm@37218
  1078
See src/Tools/jEdit or "isabelle jedit" provided by the properly built
wenzelm@37218
  1079
component.
wenzelm@37218
  1080
wenzelm@37375
  1081
* "IsabelleText" is a Unicode font derived from Bitstream Vera Mono
wenzelm@37375
  1082
and Bluesky TeX fonts.  It provides the usual Isabelle symbols,
wenzelm@37375
  1083
similar to the default assignment of the document preparation system
wenzelm@37375
  1084
(cf. isabellesym.sty).  The Isabelle/Scala class Isabelle_System
wenzelm@37375
  1085
provides some operations for direct access to the font without asking
wenzelm@37375
  1086
the user for manual installation.
wenzelm@37375
  1087
wenzelm@34238
  1088
haftmann@33993
  1089
wenzelm@33842
  1090
New in Isabelle2009-1 (December 2009)
wenzelm@33842
  1091
-------------------------------------
wenzelm@30904
  1092
wenzelm@31547
  1093
*** General ***
wenzelm@31547
  1094
wenzelm@31547
  1095
* Discontinued old form of "escaped symbols" such as \\<forall>.  Only
wenzelm@31547
  1096
one backslash should be used, even in ML sources.
wenzelm@31547
  1097
wenzelm@31547
  1098
haftmann@30951
  1099
*** Pure ***
haftmann@30951
  1100
ballarin@32846
  1101
* Locale interpretation propagates mixins along the locale hierarchy.
ballarin@32846
  1102
The currently only available mixins are the equations used to map
ballarin@32846
  1103
local definitions to terms of the target domain of an interpretation.
ballarin@32846
  1104
wenzelm@33842
  1105
* Reactivated diagnostic command 'print_interps'.  Use "print_interps
wenzelm@33842
  1106
loc" to print all interpretations of locale "loc" in the theory.
wenzelm@33842
  1107
Interpretations in proofs are not shown.
ballarin@32846
  1108
ballarin@32983
  1109
* Thoroughly revised locales tutorial.  New section on conditional
ballarin@32983
  1110
interpretation.
ballarin@32983
  1111
wenzelm@33843
  1112
* On instantiation of classes, remaining undefined class parameters
wenzelm@33843
  1113
are formally declared.  INCOMPATIBILITY.
wenzelm@33843
  1114
haftmann@30951
  1115
wenzelm@33842
  1116
*** Document preparation ***
wenzelm@33842
  1117
wenzelm@33842
  1118
* New generalized style concept for printing terms: @{foo (style) ...}
wenzelm@33842
  1119
instead of @{foo_style style ...}  (old form is still retained for
wenzelm@33842
  1120
backward compatibility).  Styles can be also applied for
wenzelm@33842
  1121
antiquotations prop, term_type and typeof.
haftmann@32891
  1122
haftmann@32891
  1123
haftmann@30930
  1124
*** HOL ***
haftmann@30930
  1125
wenzelm@33842
  1126
* New proof method "smt" for a combination of first-order logic with
wenzelm@33842
  1127
equality, linear and nonlinear (natural/integer/real) arithmetic, and
wenzelm@33842
  1128
fixed-size bitvectors; there is also basic support for higher-order
wenzelm@33842
  1129
features (esp. lambda abstractions).  It is an incomplete decision
wenzelm@33842
  1130
procedure based on external SMT solvers using the oracle mechanism;
wenzelm@33842
  1131
for the SMT solver Z3, this method is proof-producing.  Certificates
wenzelm@33842
  1132
are provided to avoid calling the external solvers solely for
wenzelm@33842
  1133
re-checking proofs.  Due to a remote SMT service there is no need for
wenzelm@33842
  1134
installing SMT solvers locally.  See src/HOL/SMT.
wenzelm@33842
  1135
wenzelm@33842
  1136
* New commands to load and prove verification conditions generated by
wenzelm@33842
  1137
the Boogie program verifier or derived systems (e.g. the Verifying C
wenzelm@33842
  1138
Compiler (VCC) or Spec#).  See src/HOL/Boogie.
wenzelm@33842
  1139
wenzelm@33842
  1140
* New counterexample generator tool 'nitpick' based on the Kodkod
wenzelm@33842
  1141
relational model finder.  See src/HOL/Tools/Nitpick and
wenzelm@33842
  1142
src/HOL/Nitpick_Examples.
wenzelm@33842
  1143
haftmann@33860
  1144
* New commands 'code_pred' and 'values' to invoke the predicate
haftmann@33860
  1145
compiler and to enumerate values of inductive predicates.
haftmann@33860
  1146
haftmann@33860
  1147
* A tabled implementation of the reflexive transitive closure.
haftmann@33860
  1148
haftmann@33860
  1149
* New implementation of quickcheck uses generic code generator;
haftmann@33860
  1150
default generators are provided for all suitable HOL types, records
haftmann@33860
  1151
and datatypes.  Old quickcheck can be re-activated importing theory
haftmann@33860
  1152
Library/SML_Quickcheck.
haftmann@33860
  1153
wenzelm@33843
  1154
* New testing tool Mirabelle for automated proof tools.  Applies
wenzelm@33843
  1155
several tools and tactics like sledgehammer, metis, or quickcheck, to
wenzelm@33843
  1156
every proof step in a theory.  To be used in batch mode via the
wenzelm@33843
  1157
"mirabelle" utility.
wenzelm@33843
  1158
wenzelm@33843
  1159
* New proof method "sos" (sum of squares) for nonlinear real
wenzelm@33843
  1160
arithmetic (originally due to John Harison). It requires theory
wenzelm@33843
  1161
Library/Sum_Of_Squares.  It is not a complete decision procedure but
wenzelm@33843
  1162
works well in practice on quantifier-free real arithmetic with +, -,
wenzelm@33843
  1163
*, ^, =, <= and <, i.e. boolean combinations of equalities and
wenzelm@33843
  1164
inequalities between polynomials.  It makes use of external
wenzelm@33843
  1165
semidefinite programming solvers.  Method "sos" generates a
wenzelm@33843
  1166
certificate that can be pasted into the proof thus avoiding the need
wenzelm@33843
  1167
to call an external tool every time the proof is checked.  See
wenzelm@33843
  1168
src/HOL/Library/Sum_Of_Squares.
wenzelm@33843
  1169
wenzelm@33843
  1170
* New method "linarith" invokes existing linear arithmetic decision
wenzelm@33843
  1171
procedure only.
wenzelm@33843
  1172
wenzelm@33843
  1173
* New command 'atp_minimal' reduces result produced by Sledgehammer.
wenzelm@33843
  1174
wenzelm@33843
  1175
* New Sledgehammer option "Full Types" in Proof General settings menu.
wenzelm@33843
  1176
Causes full type information to be output to the ATPs.  This slows
wenzelm@33843
  1177
ATPs down considerably but eliminates a source of unsound "proofs"
wenzelm@33843
  1178
that fail later.
wenzelm@33843
  1179
wenzelm@33843
  1180
* New method "metisFT": A version of metis that uses full type
wenzelm@33843
  1181
information in order to avoid failures of proof reconstruction.
wenzelm@33843
  1182
wenzelm@33843
  1183
* New evaluator "approximate" approximates an real valued term using
wenzelm@33843
  1184
the same method as the approximation method.
wenzelm@33843
  1185
wenzelm@33843
  1186
* Method "approximate" now supports arithmetic expressions as
wenzelm@33843
  1187
boundaries of intervals and implements interval splitting and Taylor
wenzelm@33843
  1188
series expansion.
wenzelm@33843
  1189
wenzelm@33843
  1190
* ML antiquotation @{code_datatype} inserts definition of a datatype
wenzelm@33843
  1191
generated by the code generator; e.g. see src/HOL/Predicate.thy.
wenzelm@33843
  1192
haftmann@33860
  1193
* New theory SupInf of the supremum and infimum operators for sets of
haftmann@33860
  1194
reals.
haftmann@33860
  1195
haftmann@33860
  1196
* New theory Probability, which contains a development of measure
haftmann@33860
  1197
theory, eventually leading to Lebesgue integration and probability.
haftmann@33860
  1198
haftmann@33860
  1199
* Extended Multivariate Analysis to include derivation and Brouwer's
haftmann@33860
  1200
fixpoint theorem.
wenzelm@33843
  1201
wenzelm@33842
  1202
* Reorganization of number theory, INCOMPATIBILITY:
wenzelm@33873
  1203
  - new number theory development for nat and int, in theories Divides
wenzelm@33873
  1204
    and GCD as well as in new session Number_Theory
wenzelm@33873
  1205
  - some constants and facts now suffixed with _nat and _int
wenzelm@33873
  1206
    accordingly
wenzelm@33873
  1207
  - former session NumberTheory now named Old_Number_Theory, including
wenzelm@33873
  1208
    theories Legacy_GCD and Primes (prefer Number_Theory if possible)
wenzelm@33842
  1209
  - moved theory Pocklington from src/HOL/Library to
wenzelm@33842
  1210
    src/HOL/Old_Number_Theory
haftmann@32479
  1211
wenzelm@33873
  1212
* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and
wenzelm@33873
  1213
lcm of finite and infinite sets. It is shown that they form a complete
haftmann@32600
  1214
lattice.
haftmann@32600
  1215
haftmann@32600
  1216
* Class semiring_div requires superclass no_zero_divisors and proof of
haftmann@32600
  1217
div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
haftmann@32600
  1218
div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
haftmann@32600
  1219
generalized to class semiring_div, subsuming former theorems
haftmann@32600
  1220
zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
haftmann@32600
  1221
zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
haftmann@32600
  1222
INCOMPATIBILITY.
haftmann@32600
  1223
haftmann@32588
  1224
* Refinements to lattice classes and sets:
haftmann@32064
  1225
  - less default intro/elim rules in locale variant, more default
haftmann@32064
  1226
    intro/elim rules in class variant: more uniformity
wenzelm@33842
  1227
  - lemma ge_sup_conv renamed to le_sup_iff, in accordance with
wenzelm@33842
  1228
    le_inf_iff
wenzelm@33842
  1229
  - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and
wenzelm@33842
  1230
    sup_aci)
haftmann@32064
  1231
  - renamed ACI to inf_sup_aci
haftmann@32600
  1232
  - new class "boolean_algebra"
wenzelm@33842
  1233
  - class "complete_lattice" moved to separate theory
haftmann@33860
  1234
    "Complete_Lattice"; corresponding constants (and abbreviations)
wenzelm@33842
  1235
    renamed and with authentic syntax:
haftmann@33860
  1236
    Set.Inf ~>    Complete_Lattice.Inf
haftmann@33860
  1237
    Set.Sup ~>    Complete_Lattice.Sup
haftmann@33860
  1238
    Set.INFI ~>   Complete_Lattice.INFI
haftmann@33860
  1239
    Set.SUPR ~>   Complete_Lattice.SUPR
haftmann@33860
  1240
    Set.Inter ~>  Complete_Lattice.Inter
haftmann@33860
  1241
    Set.Union ~>  Complete_Lattice.Union
haftmann@33860
  1242
    Set.INTER ~>  Complete_Lattice.INTER
haftmann@33860
  1243
    Set.UNION ~>  Complete_Lattice.UNION
haftmann@32600
  1244
  - authentic syntax for
haftmann@32600
  1245
    Set.Pow
haftmann@32600
  1246
    Set.image
haftmann@32588
  1247
  - mere abbreviations:
haftmann@32588
  1248
    Set.empty               (for bot)
haftmann@32588
  1249
    Set.UNIV                (for top)
haftmann@33860
  1250
    Set.inter               (for inf, formerly Set.Int)
haftmann@33860
  1251
    Set.union               (for sup, formerly Set.Un)
haftmann@32588
  1252
    Complete_Lattice.Inter  (for Inf)
haftmann@32588
  1253
    Complete_Lattice.Union  (for Sup)
haftmann@32606
  1254
    Complete_Lattice.INTER  (for INFI)
haftmann@32606
  1255
    Complete_Lattice.UNION  (for SUPR)
haftmann@32600
  1256
  - object-logic definitions as far as appropriate
haftmann@32217
  1257
haftmann@32691
  1258
INCOMPATIBILITY.  Care is required when theorems Int_subset_iff or
wenzelm@33842
  1259
Un_subset_iff are explicitly deleted as default simp rules; then also
wenzelm@33842
  1260
their lattice counterparts le_inf_iff and le_sup_iff have to be
haftmann@32691
  1261
deleted to achieve the desired effect.
haftmann@32064
  1262
wenzelm@33842
  1263
* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp
wenzelm@33842
  1264
rules by default any longer; the same applies to min_max.inf_absorb1
wenzelm@33842
  1265
etc.  INCOMPATIBILITY.
wenzelm@33842
  1266
wenzelm@33842
  1267
* Rules sup_Int_eq and sup_Un_eq are no longer declared as
wenzelm@33842
  1268
pred_set_conv by default.  INCOMPATIBILITY.
wenzelm@33842
  1269
wenzelm@33842
  1270
* Power operations on relations and functions are now one dedicated
haftmann@32706
  1271
constant "compow" with infix syntax "^^".  Power operation on
wenzelm@31547
  1272
multiplicative monoids retains syntax "^" and is now defined generic
wenzelm@31547
  1273
in class power.  INCOMPATIBILITY.
wenzelm@31547
  1274
wenzelm@33842
  1275
* Relation composition "R O S" now has a more standard argument order:
wenzelm@33842
  1276
"R O S = {(x, z). EX y. (x, y) : R & (y, z) : S}".  INCOMPATIBILITY,
wenzelm@33842
  1277
rewrite propositions with "S O R" --> "R O S". Proofs may occasionally
wenzelm@33842
  1278
break, since the O_assoc rule was not rewritten like this.  Fix using
wenzelm@33842
  1279
O_assoc[symmetric].  The same applies to the curried version "R OO S".
wenzelm@32427
  1280
nipkow@33057
  1281
* Function "Inv" is renamed to "inv_into" and function "inv" is now an
wenzelm@33842
  1282
abbreviation for "inv_into UNIV".  Lemmas are renamed accordingly.
nipkow@32988
  1283
INCOMPATIBILITY.
nipkow@32988
  1284
haftmann@33860
  1285
* Most rules produced by inductive and datatype package have mandatory
haftmann@33860
  1286
prefixes.  INCOMPATIBILITY.
nipkow@31790
  1287
wenzelm@33842
  1288
* Changed "DERIV_intros" to a dynamic fact, which can be augmented by
wenzelm@33842
  1289
the attribute of the same name.  Each of the theorems in the list
wenzelm@33842
  1290
DERIV_intros assumes composition with an additional function and
wenzelm@33842
  1291
matches a variable to the derivative, which has to be solved by the
wenzelm@33842
  1292
Simplifier.  Hence (auto intro!: DERIV_intros) computes the derivative
wenzelm@33873
  1293
of most elementary terms.  Former Maclauren.DERIV_tac and
wenzelm@33873
  1294
Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros).
wenzelm@33873
  1295
INCOMPATIBILITY.
haftmann@33860
  1296
haftmann@33860
  1297
* Code generator attributes follow the usual underscore convention:
haftmann@33860
  1298
    code_unfold     replaces    code unfold
haftmann@33860
  1299
    code_post       replaces    code post
haftmann@33860
  1300
    etc.
haftmann@33860
  1301
  INCOMPATIBILITY.
wenzelm@31900
  1302
krauss@33471
  1303
* Renamed methods:
krauss@33471
  1304
    sizechange -> size_change
krauss@33471
  1305
    induct_scheme -> induction_schema
haftmann@33860
  1306
  INCOMPATIBILITY.
nipkow@33673
  1307
wenzelm@33843
  1308
* Discontinued abbreviation "arbitrary" of constant "undefined".
wenzelm@33843
  1309
INCOMPATIBILITY, use "undefined" directly.
wenzelm@33843
  1310
haftmann@33860
  1311
* Renamed theorems:
haftmann@33860
  1312
    Suc_eq_add_numeral_1 -> Suc_eq_plus1
haftmann@33860
  1313
    Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
haftmann@33860
  1314
    Suc_plus1 -> Suc_eq_plus1
haftmann@33860
  1315
    *anti_sym -> *antisym*
haftmann@33860
  1316
    vector_less_eq_def -> vector_le_def
haftmann@33860
  1317
  INCOMPATIBILITY.
haftmann@33860
  1318
haftmann@33860
  1319
* Added theorem List.map_map as [simp].  Removed List.map_compose.
haftmann@33860
  1320
INCOMPATIBILITY.
haftmann@33860
  1321
haftmann@33860
  1322
* Removed predicate "M hassize n" (<--> card M = n & finite M).
haftmann@33860
  1323
INCOMPATIBILITY.
haftmann@33860
  1324
hoelzl@31812
  1325
huffman@33825
  1326
*** HOLCF ***
huffman@33825
  1327
wenzelm@33842
  1328
* Theory Representable defines a class "rep" of domains that are
wenzelm@33842
  1329
representable (via an ep-pair) in the universal domain type "udom".
huffman@33825
  1330
Instances are provided for all type constructors defined in HOLCF.
huffman@33825
  1331
huffman@33825
  1332
* The 'new_domain' command is a purely definitional version of the
huffman@33825
  1333
domain package, for representable domains.  Syntax is identical to the
huffman@33825
  1334
old domain package.  The 'new_domain' package also supports indirect
huffman@33825
  1335
recursion using previously-defined type constructors.  See
wenzelm@33842
  1336
src/HOLCF/ex/New_Domain.thy for examples.
wenzelm@33842
  1337
wenzelm@33842
  1338
* Method "fixrec_simp" unfolds one step of a fixrec-defined constant
huffman@33825
  1339
on the left-hand side of an equation, and then performs
huffman@33825
  1340
simplification.  Rewriting is done using rules declared with the
wenzelm@33842
  1341
"fixrec_simp" attribute.  The "fixrec_simp" method is intended as a
wenzelm@33842
  1342
replacement for "fixpat"; see src/HOLCF/ex/Fixrec_ex.thy for examples.
huffman@33825
  1343
huffman@33825
  1344
* The pattern-match compiler in 'fixrec' can now handle constructors
huffman@33825
  1345
with HOL function types.  Pattern-match combinators for the Pair
huffman@33825
  1346
constructor are pre-configured.
huffman@33825
  1347
huffman@33825
  1348
* The 'fixrec' package now produces better fixed-point induction rules
huffman@33825
  1349
for mutually-recursive definitions:  Induction rules have conclusions
huffman@33825
  1350
of the form "P foo bar" instead of "P <foo, bar>".
huffman@33825
  1351
huffman@33825
  1352
* The constant "sq_le" (with infix syntax "<<" or "\<sqsubseteq>") has
huffman@33825
  1353
been renamed to "below".  The name "below" now replaces "less" in many
wenzelm@33842
  1354
theorem names.  (Legacy theorem names using "less" are still supported
wenzelm@33842
  1355
as well.)
huffman@33825
  1356
huffman@33825
  1357
* The 'fixrec' package now supports "bottom patterns".  Bottom
huffman@33825
  1358
patterns can be used to generate strictness rules, or to make
huffman@33825
  1359
functions more strict (much like the bang-patterns supported by the
wenzelm@33873
  1360
Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for
wenzelm@33873
  1361
examples.
huffman@33825
  1362
huffman@33825
  1363
wenzelm@31304
  1364
*** ML ***
wenzelm@31304
  1365
wenzelm@33843
  1366
* Support for Poly/ML 5.3.0, with improved reporting of compiler
wenzelm@33843
  1367
errors and run-time exceptions, including detailed source positions.
wenzelm@33843
  1368
wenzelm@33843
  1369
* Structure Name_Space (formerly NameSpace) now manages uniquely
wenzelm@33843
  1370
identified entries, with some additional information such as source
wenzelm@33843
  1371
position, logical grouping etc.
wenzelm@33843
  1372
wenzelm@33524
  1373
* Theory and context data is now introduced by the simplified and
wenzelm@33524
  1374
modernized functors Theory_Data, Proof_Data, Generic_Data.  Data needs
wenzelm@33524
  1375
to be pure, but the old TheoryDataFun for mutable data (with explicit
wenzelm@33524
  1376
copy operation) is still available for some time.
wenzelm@33524
  1377
wenzelm@32742
  1378
* Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)
wenzelm@32742
  1379
provides a high-level programming interface to synchronized state
wenzelm@32742
  1380
variables with atomic update.  This works via pure function
wenzelm@32742
  1381
application within a critical section -- its runtime should be as
wenzelm@32742
  1382
short as possible; beware of deadlocks if critical code is nested,
wenzelm@32742
  1383
either directly or indirectly via other synchronized variables!
wenzelm@32742
  1384
wenzelm@32742
  1385
* Structure Unsynchronized (cf. src/Pure/ML-Systems/unsynchronized.ML)
wenzelm@32742
  1386
wraps raw ML references, explicitly indicating their non-thread-safe
wenzelm@32742
  1387
behaviour.  The Isar toplevel keeps this structure open, to
wenzelm@32742
  1388
accommodate Proof General as well as quick and dirty interactive
wenzelm@32742
  1389
experiments with references.
wenzelm@32742
  1390
wenzelm@32365
  1391
* PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for
wenzelm@32365
  1392
parallel tactical reasoning.
wenzelm@32365
  1393
wenzelm@32427
  1394
* Tacticals Subgoal.FOCUS, Subgoal.FOCUS_PREMS, Subgoal.FOCUS_PARAMS
wenzelm@32427
  1395
are similar to SUBPROOF, but are slightly more flexible: only the
wenzelm@32427
  1396
specified parts of the subgoal are imported into the context, and the
wenzelm@32427
  1397
body tactic may introduce new subgoals and schematic variables.
wenzelm@32427
  1398
wenzelm@32427
  1399
* Old tactical METAHYPS, which does not observe the proof context, has
wenzelm@32427
  1400
been renamed to Old_Goals.METAHYPS and awaits deletion.  Use SUBPROOF
wenzelm@32427
  1401
or Subgoal.FOCUS etc.
wenzelm@32216
  1402
wenzelm@31971
  1403
* Renamed functor TableFun to Table, and GraphFun to Graph.  (Since
wenzelm@31971
  1404
functors have their own ML name space there is no point to mark them
wenzelm@31971
  1405
separately.)  Minor INCOMPATIBILITY.
wenzelm@31971
  1406
wenzelm@31901
  1407
* Renamed NamedThmsFun to Named_Thms.  INCOMPATIBILITY.
wenzelm@31901
  1408
wenzelm@33842
  1409
* Renamed several structures FooBar to Foo_Bar.  Occasional,
wenzelm@33842
  1410
INCOMPATIBILITY.
wenzelm@33842
  1411
wenzelm@33843
  1412
* Operations of structure Skip_Proof no longer require quick_and_dirty
wenzelm@33843
  1413
mode, which avoids critical setmp.
wenzelm@33843
  1414
wenzelm@31306
  1415
* Eliminated old Attrib.add_attributes, Method.add_methods and related
wenzelm@33842
  1416
combinators for "args".  INCOMPATIBILITY, need to use simplified
wenzelm@31306
  1417
Attrib/Method.setup introduced in Isabelle2009.
wenzelm@31304
  1418
wenzelm@32151
  1419
* Proper context for simpset_of, claset_of, clasimpset_of.  May fall
wenzelm@32151
  1420
back on global_simpset_of, global_claset_of, global_clasimpset_of as
wenzelm@32151
  1421
last resort.  INCOMPATIBILITY.
wenzelm@32151
  1422
wenzelm@32092
  1423
* Display.pretty_thm now requires a proper context (cf. former
wenzelm@32092
  1424
ProofContext.pretty_thm).  May fall back on Display.pretty_thm_global
wenzelm@32092
  1425
or even Display.pretty_thm_without_context as last resort.
wenzelm@32092
  1426
INCOMPATIBILITY.
wenzelm@32092
  1427
wenzelm@32433
  1428
* Discontinued Display.pretty_ctyp/cterm etc.  INCOMPATIBILITY, use
wenzelm@32433
  1429
Syntax.pretty_typ/term directly, preferably with proper context
wenzelm@32433
  1430
instead of global theory.
wenzelm@32433
  1431
wenzelm@31304
  1432
wenzelm@31308
  1433
*** System ***
wenzelm@31308
  1434
wenzelm@33842
  1435
* Further fine tuning of parallel proof checking, scales up to 8 cores
wenzelm@33842
  1436
(max. speedup factor 5.0).  See also Goal.parallel_proofs in ML and
wenzelm@33842
  1437
usedir option -q.
wenzelm@33842
  1438
wenzelm@32326
  1439
* Support for additional "Isabelle components" via etc/components, see
wenzelm@32326
  1440
also the system manual.
wenzelm@32326
  1441
wenzelm@32326
  1442
* The isabelle makeall tool now operates on all components with
wenzelm@32326
  1443
IsaMakefile, not just hardwired "logics".
wenzelm@32326
  1444
wenzelm@33842
  1445
* Removed "compress" option from isabelle-process and isabelle usedir;
wenzelm@33842
  1446
this is always enabled.
kleing@33818
  1447
wenzelm@31308
  1448
* Discontinued support for Poly/ML 4.x versions.
wenzelm@31308
  1449
wenzelm@33842
  1450
* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
wenzelm@33842
  1451
on a given logic image.  This requires the lighttpd webserver and is
wenzelm@33842
  1452
currently supported on Linux only.
wenzelm@32061
  1453
wenzelm@31308
  1454
wenzelm@31304
  1455
wenzelm@30845
  1456
New in Isabelle2009 (April 2009)
wenzelm@30845
  1457
--------------------------------
haftmann@27104
  1458
wenzelm@27599
  1459
*** General ***
wenzelm@27599
  1460
wenzelm@28504
  1461
* Simplified main Isabelle executables, with less surprises on
wenzelm@28504
  1462
case-insensitive file-systems (such as Mac OS).
wenzelm@28504
  1463
wenzelm@28504
  1464
  - The main Isabelle tool wrapper is now called "isabelle" instead of
wenzelm@28504
  1465
    "isatool."
wenzelm@28504
  1466
wenzelm@28504
  1467
  - The former "isabelle" alias for "isabelle-process" has been
wenzelm@28504
  1468
    removed (should rarely occur to regular users).
wenzelm@28504
  1469
wenzelm@28915
  1470
  - The former "isabelle-interface" and its alias "Isabelle" have been
wenzelm@28915
  1471
    removed (interfaces are now regular Isabelle tools).
wenzelm@28504
  1472
wenzelm@28504
  1473
Within scripts and make files, the Isabelle environment variables
wenzelm@28504
  1474
ISABELLE_TOOL and ISABELLE_PROCESS replace old ISATOOL and ISABELLE,
wenzelm@28504
  1475
respectively.  (The latter are still available as legacy feature.)
wenzelm@28504
  1476
wenzelm@28915
  1477
The old isabelle-interface wrapper could react in confusing ways if
wenzelm@28915
  1478
the interface was uninstalled or changed otherwise.  Individual
wenzelm@28915
  1479
interface tool configuration is now more explicit, see also the
wenzelm@28915
  1480
Isabelle system manual.  In particular, Proof General is now available
wenzelm@28915
  1481
via "isabelle emacs".
wenzelm@28504
  1482
wenzelm@28504
  1483
INCOMPATIBILITY, need to adapt derivative scripts.  Users may need to
wenzelm@28504
  1484
purge installed copies of Isabelle executables and re-run "isabelle
wenzelm@28504
  1485
install -p ...", or use symlinks.
wenzelm@28504
  1486
wenzelm@28914
  1487
* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the
wenzelm@30845
  1488
old ~/isabelle, which was slightly non-standard and apt to cause
wenzelm@30845
  1489
surprises on case-insensitive file-systems (such as Mac OS).
wenzelm@28914
  1490
wenzelm@28914
  1491
INCOMPATIBILITY, need to move existing ~/isabelle/etc,
wenzelm@28914
  1492
~/isabelle/heaps, ~/isabelle/browser_info to the new place.  Special
wenzelm@28914
  1493
care is required when using older releases of Isabelle.  Note that
wenzelm@28914
  1494
ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any
wenzelm@30845
  1495
Isabelle distribution, in order to use the new ~/.isabelle uniformly.
wenzelm@28914
  1496
wenzelm@29161
  1497
* Proofs of fully specified statements are run in parallel on
wenzelm@30845
  1498
multi-core systems.  A speedup factor of 2.5 to 3.2 can be expected on
wenzelm@30845
  1499
a regular 4-core machine, if the initial heap space is made reasonably
wenzelm@30845
  1500
large (cf. Poly/ML option -H).  (Requires Poly/ML 5.2.1 or later.)
wenzelm@30845
  1501
wenzelm@30845
  1502
* The main reference manuals ("isar-ref", "implementation", and
wenzelm@30845
  1503
"system") have been updated and extended.  Formally checked references
wenzelm@30845
  1504
as hyperlinks are now available uniformly.
wenzelm@30845
  1505
wenzelm@30163
  1506
wenzelm@27599
  1507
*** Pure ***
wenzelm@27599
  1508
wenzelm@30845
  1509
* Complete re-implementation of locales.  INCOMPATIBILITY in several
wenzelm@30845
  1510
respects.  The most important changes are listed below.  See the
wenzelm@30845
  1511
Tutorial on Locales ("locales" manual) for details.
ballarin@29253
  1512
ballarin@29253
  1513
- In locale expressions, instantiation replaces renaming.  Parameters
ballarin@29253
  1514
must be declared in a for clause.  To aid compatibility with previous
ballarin@29253
  1515
parameter inheritance, in locale declarations, parameters that are not
ballarin@29253
  1516
'touched' (instantiation position "_" or omitted) are implicitly added
ballarin@29253
  1517
with their syntax at the beginning of the for clause.
ballarin@29253
  1518
ballarin@29253
  1519
- Syntax from abbreviations and definitions in locales is available in
ballarin@29253
  1520
locale expressions and context elements.  The latter is particularly
ballarin@29253
  1521
useful in locale declarations.
ballarin@29253
  1522
ballarin@29253
  1523
- More flexible mechanisms to qualify names generated by locale
ballarin@29253
  1524
expressions.  Qualifiers (prefixes) may be specified in locale
wenzelm@30728
  1525
expressions, and can be marked as mandatory (syntax: "name!:") or
wenzelm@30728
  1526
optional (syntax "name?:").  The default depends for plain "name:"
wenzelm@30728
  1527
depends on the situation where a locale expression is used: in
wenzelm@30728
  1528
commands 'locale' and 'sublocale' prefixes are optional, in
wenzelm@30845
  1529
'interpretation' and 'interpret' prefixes are mandatory.  The old
wenzelm@30728
  1530
implicit qualifiers derived from the parameter names of a locale are
wenzelm@30728
  1531
no longer generated.
wenzelm@30106
  1532
wenzelm@30845
  1533
- Command "sublocale l < e" replaces "interpretation l < e".  The
wenzelm@30106
  1534
instantiation clause in "interpretation" and "interpret" (square
wenzelm@30106
  1535
brackets) is no longer available.  Use locale expressions.
ballarin@29253
  1536
wenzelm@30845
  1537
- When converting proof scripts, mandatory qualifiers in
wenzelm@30728
  1538
'interpretation' and 'interpret' should be retained by default, even
wenzelm@30845
  1539
if this is an INCOMPATIBILITY compared to former behavior.  In the
wenzelm@30845
  1540
worst case, use the "name?:" form for non-mandatory ones.  Qualifiers
wenzelm@30845
  1541
in locale expressions range over a single locale instance only.
wenzelm@30845
  1542
wenzelm@30845
  1543
- Dropped locale element "includes".  This is a major INCOMPATIBILITY.
wenzelm@30845
  1544
In existing theorem specifications replace the includes element by the
wenzelm@30845
  1545
respective context elements of the included locale, omitting those
wenzelm@30845
  1546
that are already present in the theorem specification.  Multiple
wenzelm@30845
  1547
assume elements of a locale should be replaced by a single one
wenzelm@30845
  1548
involving the locale predicate.  In the proof body, declarations (most
wenzelm@30845
  1549
notably theorems) may be regained by interpreting the respective
wenzelm@30845
  1550
locales in the proof context as required (command "interpret").
wenzelm@30845
  1551
wenzelm@30845
  1552
If using "includes" in replacement of a target solely because the
wenzelm@30845
  1553
parameter types in the theorem are not as general as in the target,
wenzelm@30845
  1554
consider declaring a new locale with additional type constraints on
wenzelm@30845
  1555
the parameters (context element "constrains").
wenzelm@30845
  1556
wenzelm@30845
  1557
- Discontinued "locale (open)".  INCOMPATIBILITY.
wenzelm@30845
  1558
wenzelm@30845
  1559
- Locale interpretation commands no longer attempt to simplify goal.
wenzelm@30845
  1560
INCOMPATIBILITY: in rare situations the generated goal differs.  Use
wenzelm@30845
  1561
methods intro_locales and unfold_locales to clarify.
wenzelm@30845
  1562
wenzelm@30845
  1563
- Locale interpretation commands no longer accept interpretation
wenzelm@30845
  1564
attributes.  INCOMPATIBILITY.
wenzelm@30845
  1565
wenzelm@30845
  1566
* Class declaration: so-called "base sort" must not be given in import
wenzelm@30845
  1567
list any longer, but is inferred from the specification.  Particularly
wenzelm@30845
  1568
in HOL, write
wenzelm@30845
  1569
wenzelm@30845
  1570
    class foo = ...
wenzelm@30845
  1571
wenzelm@30845
  1572
instead of
wenzelm@30845
  1573
wenzelm@30845
  1574
    class foo = type + ...
wenzelm@30845
  1575
wenzelm@30845
  1576
* Class target: global versions of theorems stemming do not carry a
wenzelm@30845
  1577
parameter prefix any longer.  INCOMPATIBILITY.
wenzelm@30845
  1578
wenzelm@30845
  1579
* Class 'instance' command no longer accepts attached definitions.
wenzelm@30845
  1580
INCOMPATIBILITY, use proper 'instantiation' target instead.
wenzelm@30845
  1581
wenzelm@30845
  1582
* Recovered hiding of consts, which was accidentally broken in
wenzelm@30845
  1583
Isabelle2007.  Potential INCOMPATIBILITY, ``hide const c'' really
wenzelm@30845
  1584
makes c inaccessible; consider using ``hide (open) const c'' instead.
wenzelm@30845
  1585
wenzelm@30845
  1586
* Slightly more coherent Pure syntax, with updated documentation in
wenzelm@30845
  1587
isar-ref manual.  Removed locales meta_term_syntax and
wenzelm@30845
  1588
meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,
wenzelm@30845
  1589
INCOMPATIBILITY in rare situations.  Note that &&& should not be used
wenzelm@30845
  1590
directly in regular applications.
wenzelm@30845
  1591
wenzelm@30845
  1592
* There is a new syntactic category "float_const" for signed decimal
wenzelm@30845
  1593
fractions (e.g. 123.45 or -123.45).
wenzelm@30845
  1594
wenzelm@30845
  1595
* Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
wenzelm@30845
  1596
interface with 'setup' command instead.
wenzelm@30845
  1597
wenzelm@30845
  1598
* Command 'local_setup' is similar to 'setup', but operates on a local
wenzelm@30845
  1599
theory context.
haftmann@27104
  1600
wenzelm@28114
  1601
* The 'axiomatization' command now only works within a global theory
wenzelm@28114
  1602
context.  INCOMPATIBILITY.
wenzelm@28114
  1603
wenzelm@30845
  1604
* Goal-directed proof now enforces strict proof irrelevance wrt. sort
wenzelm@30845
  1605
hypotheses.  Sorts required in the course of reasoning need to be
wenzelm@30845
  1606
covered by the constraints in the initial statement, completed by the
wenzelm@30845
  1607
type instance information of the background theory.  Non-trivial sort
wenzelm@30845
  1608
hypotheses, which rarely occur in practice, may be specified via
wenzelm@30845
  1609
vacuous propositions of the form SORT_CONSTRAINT('a::c).  For example:
wenzelm@30845
  1610
wenzelm@30845
  1611
  lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ...
wenzelm@30845
  1612
wenzelm@30845
  1613
The result contains an implicit sort hypotheses as before --
wenzelm@30845
  1614
SORT_CONSTRAINT premises are eliminated as part of the canonical rule
wenzelm@30845
  1615
normalization.
wenzelm@30845
  1616
wenzelm@30845
  1617
* Generalized Isar history, with support for linear undo, direct state
wenzelm@30845
  1618
addressing etc.
wenzelm@30845
  1619
wenzelm@30845
  1620
* Changed defaults for unify configuration options:
wenzelm@30845
  1621
wenzelm@30845
  1622
  unify_trace_bound = 50 (formerly 25)
wenzelm@30845
  1623
  unify_search_bound = 60 (formerly 30)
wenzelm@30845
  1624
wenzelm@30845
  1625
* Different bookkeeping for code equations (INCOMPATIBILITY):
wenzelm@30845
  1626
wenzelm@30845
  1627
  a) On theory merge, the last set of code equations for a particular
wenzelm@30845
  1628
     constant is taken (in accordance with the policy applied by other
wenzelm@30845
  1629
     parts of the code generator framework).
wenzelm@30845
  1630
wenzelm@30845
  1631
  b) Code equations stemming from explicit declarations (e.g. code
wenzelm@30845
  1632
     attribute) gain priority over default code equations stemming
wenzelm@30845
  1633
     from definition, primrec, fun etc.
wenzelm@30845
  1634
wenzelm@30845
  1635
* Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
wenzelm@30845
  1636
haftmann@30965
  1637
* Unified theorem tables for both code generators.  Thus [code
wenzelm@30845
  1638
func] has disappeared and only [code] remains.  INCOMPATIBILITY.
wenzelm@30577
  1639
wenzelm@30577
  1640
* Command 'find_consts' searches for constants based on type and name
wenzelm@30577
  1641
patterns, e.g.
kleing@29883
  1642
kleing@29883
  1643
    find_consts "_ => bool"
kleing@29883
  1644
wenzelm@30106
  1645
By default, matching is against subtypes, but it may be restricted to
wenzelm@30728
  1646
the whole type.  Searching by name is possible.  Multiple queries are
wenzelm@30106
  1647
conjunctive and queries may be negated by prefixing them with a
wenzelm@30106
  1648
hyphen:
kleing@29883
  1649
kleing@29883
  1650
    find_consts strict: "_ => bool" name: "Int" -"int => int"
kleing@29861
  1651
wenzelm@30845
  1652
* New 'find_theorems' criterion "solves" matches theorems that
wenzelm@30845
  1653
directly solve the current goal (modulo higher-order unification).
wenzelm@30845
  1654
wenzelm@30845
  1655
* Auto solve feature for main theorem statements: whenever a new goal
wenzelm@30845
  1656
is stated, "find_theorems solves" is called; any theorems that could
wenzelm@30845
  1657
solve the lemma directly are listed as part of the goal state.
wenzelm@30845
  1658
Cf. associated options in Proof General Isabelle settings menu,
wenzelm@30845
  1659
enabled by default, with reasonable timeout for pathological cases of
wenzelm@30845
  1660
higher-order unification.
webertj@30415
  1661
haftmann@27104
  1662
wenzelm@27381
  1663
*** Document preparation ***
wenzelm@27381
  1664
wenzelm@27381
  1665
* Antiquotation @{lemma} now imitates a regular terminal proof,
wenzelm@27392
  1666
demanding keyword 'by' and supporting the full method expression
wenzelm@27519
  1667
syntax just like the Isar command 'by'.
wenzelm@27381
  1668
wenzelm@27381
  1669
haftmann@27104
  1670
*** HOL ***
haftmann@27104
  1671
wenzelm@30845
  1672
* Integrated main parts of former image HOL-Complex with HOL.  Entry
wenzelm@30845
  1673
points Main and Complex_Main remain as before.
wenzelm@30845
  1674
wenzelm@30845
  1675
* Logic image HOL-Plain provides a minimal HOL with the most important
wenzelm@30845
  1676
tools available (inductive, datatype, primrec, ...).  This facilitates
wenzelm@30845
  1677
experimentation and tool development.  Note that user applications
wenzelm@30845
  1678
(and library theories) should never refer to anything below theory
wenzelm@30845
  1679
Main, as before.
wenzelm@30845
  1680
wenzelm@30845
  1681
* Logic image HOL-Main stops at theory Main, and thus facilitates
wenzelm@30845
  1682
experimentation due to shorter build times.
wenzelm@30845
  1683
wenzelm@30845
  1684
* Logic image HOL-NSA contains theories of nonstandard analysis which
wenzelm@30845
  1685
were previously part of former HOL-Complex.  Entry point Hyperreal
wenzelm@30845
  1686
remains valid, but theories formerly using Complex_Main should now use
wenzelm@30845
  1687
new entry point Hypercomplex.
wenzelm@30845
  1688
wenzelm@30845
  1689
* Generic ATP manager for Sledgehammer, based on ML threads instead of
wenzelm@30845
  1690
Posix processes.  Avoids potentially expensive forking of the ML
wenzelm@30845
  1691
process.  New thread-based implementation also works on non-Unix
wenzelm@30845
  1692
platforms (Cygwin).  Provers are no longer hardwired, but defined
wenzelm@30845
  1693
within the theory via plain ML wrapper functions.  Basic Sledgehammer
wenzelm@30845
  1694
commands are covered in the isar-ref manual.
wenzelm@30845
  1695
wenzelm@30845
  1696
* Wrapper scripts for remote SystemOnTPTP service allows to use
wenzelm@30845
  1697
sledgehammer without local ATP installation (Vampire etc.). Other
wenzelm@30845
  1698
provers may be included via suitable ML wrappers, see also
wenzelm@30845
  1699
src/HOL/ATP_Linkup.thy.
wenzelm@30845
  1700
wenzelm@30845
  1701
* ATP selection (E/Vampire/Spass) is now via Proof General's settings
wenzelm@30845
  1702
menu.
wenzelm@30845
  1703
wenzelm@30845
  1704
* The metis method no longer fails because the theorem is too trivial
wenzelm@30845
  1705
(contains the empty clause).
wenzelm@30845
  1706
wenzelm@30845
  1707
* The metis method now fails in the usual manner, rather than raising
wenzelm@30845
  1708
an exception, if it determines that it cannot prove the theorem.
wenzelm@30845
  1709
wenzelm@30845
  1710
* Method "coherent" implements a prover for coherent logic (see also
wenzelm@30845
  1711
src/Tools/coherent.ML).
wenzelm@30845
  1712
wenzelm@30845
  1713
* Constants "undefined" and "default" replace "arbitrary".  Usually
wenzelm@30845
  1714
"undefined" is the right choice to replace "arbitrary", though
wenzelm@30845
  1715
logically there is no difference.  INCOMPATIBILITY.
wenzelm@30845
  1716
wenzelm@30845
  1717
* Command "value" now integrates different evaluation mechanisms.  The
wenzelm@30845
  1718
result of the first successful evaluation mechanism is printed.  In
wenzelm@30845
  1719
square brackets a particular named evaluation mechanisms may be
wenzelm@30845
  1720
specified (currently, [SML], [code] or [nbe]).  See further
wenzelm@30845
  1721
src/HOL/ex/Eval_Examples.thy.
wenzelm@30845
  1722
wenzelm@30845
  1723
* Normalization by evaluation now allows non-leftlinear equations.
wenzelm@30845
  1724
Declare with attribute [code nbe].
wenzelm@30845
  1725
wenzelm@30845
  1726
* Methods "case_tac" and "induct_tac" now refer to the very same rules
wenzelm@30845
  1727
as the structured Isar versions "cases" and "induct", cf. the
wenzelm@30845
  1728
corresponding "cases" and "induct" attributes.  Mutual induction rules
wenzelm@30845
  1729
are now presented as a list of individual projections
wenzelm@30845
  1730
(e.g. foo_bar.inducts for types foo and bar); the old format with
wenzelm@30845
  1731
explicit HOL conjunction is no longer supported.  INCOMPATIBILITY, in
wenzelm@30845
  1732
rare situations a different rule is selected --- notably nested tuple
wenzelm@30845
  1733
elimination instead of former prod.exhaust: use explicit (case_tac t
wenzelm@30845
  1734
rule: prod.exhaust) here.
wenzelm@30845
  1735
wenzelm@30845
  1736
* Attributes "cases", "induct", "coinduct" support "del" option.
wenzelm@30845
  1737
wenzelm@30845
  1738
* Removed fact "case_split_thm", which duplicates "case_split".
wenzelm@30845
  1739
wenzelm@30845
  1740
* The option datatype has been moved to a new theory Option.  Renamed
wenzelm@30845
  1741
option_map to Option.map, and o2s to Option.set, INCOMPATIBILITY.
wenzelm@30845
  1742
wenzelm@30845
  1743
* New predicate "strict_mono" classifies strict functions on partial
wenzelm@30845
  1744
orders.  With strict functions on linear orders, reasoning about
wenzelm@30845
  1745
(in)equalities is facilitated by theorems "strict_mono_eq",
wenzelm@30845
  1746
"strict_mono_less_eq" and "strict_mono_less".
wenzelm@30845
  1747
wenzelm@30845
  1748
* Some set operations are now proper qualified constants with
wenzelm@30845
  1749
authentic syntax.  INCOMPATIBILITY:
haftmann@30304
  1750
haftmann@30304
  1751
    op Int ~>   Set.Int
haftmann@30304
  1752
    op Un ~>    Set.Un
haftmann@30304
  1753
    INTER ~>    Set.INTER
haftmann@30304
  1754
    UNION ~>    Set.UNION
haftmann@30304
  1755
    Inter ~>    Set.Inter
haftmann@30304
  1756
    Union ~>    Set.Union
haftmann@30304
  1757
    {} ~>       Set.empty
haftmann@30304
  1758
    UNIV ~>     Set.UNIV
haftmann@30304
  1759
wenzelm@30845
  1760
* Class complete_lattice with operations Inf, Sup, INFI, SUPR now in
wenzelm@30845
  1761
theory Set.
wenzelm@30845
  1762
wenzelm@30845
  1763
* Auxiliary class "itself" has disappeared -- classes without any
wenzelm@30845
  1764
parameter are treated as expected by the 'class' command.
haftmann@29797
  1765
haftmann@29823
  1766
* Leibnitz's Series for Pi and the arcus tangens and logarithm series.
haftmann@29823
  1767
wenzelm@30845
  1768
* Common decision procedures (Cooper, MIR, Ferrack, Approximation,
wenzelm@30845
  1769
Dense_Linear_Order) are now in directory HOL/Decision_Procs.
wenzelm@30845
  1770
wenzelm@30845
  1771
* Theory src/HOL/Decision_Procs/Approximation provides the new proof
wenzelm@30845
  1772
method "approximation".  It proves formulas on real values by using
wenzelm@30845
  1773
interval arithmetic.  In the formulas are also the transcendental
wenzelm@30845
  1774
functions sin, cos, tan, atan, ln, exp and the constant pi are
wenzelm@30845
  1775
allowed. For examples see
wenzelm@30845
  1776
src/HOL/Descision_Procs/ex/Approximation_Ex.thy.
haftmann@29823
  1777
haftmann@29823
  1778
* Theory "Reflection" now resides in HOL/Library.
haftmann@29650
  1779
wenzelm@30845
  1780
* Entry point to Word library now simply named "Word".
wenzelm@30845
  1781
INCOMPATIBILITY.
haftmann@29628
  1782
haftmann@29197
  1783
* Made source layout more coherent with logical distribution
haftmann@29197
  1784
structure:
haftmann@28952
  1785
haftmann@28952
  1786
    src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy
haftmann@28952
  1787
    src/HOL/Library/Code_Message.thy ~> src/HOL/
haftmann@28952
  1788
    src/HOL/Library/GCD.thy ~> src/HOL/
haftmann@28952
  1789
    src/HOL/Library/Order_Relation.thy ~> src/HOL/
haftmann@28952
  1790
    src/HOL/Library/Parity.thy ~> src/HOL/
haftmann@28952
  1791
    src/HOL/Library/Univ_Poly.thy ~> src/HOL/
huffman@30176
  1792
    src/HOL/Real/ContNotDenum.thy ~> src/HOL/Library/
haftmann@28952
  1793
    src/HOL/Real/Lubs.thy ~> src/HOL/
haftmann@28952
  1794
    src/HOL/Real/PReal.thy ~> src/HOL/
haftmann@28952
  1795
    src/HOL/Real/Rational.thy ~> src/HOL/
haftmann@28952
  1796
    src/HOL/Real/RComplete.thy ~> src/HOL/
haftmann@28952
  1797
    src/HOL/Real/RealDef.thy ~> src/HOL/
haftmann@28952
  1798
    src/HOL/Real/RealPow.thy ~> src/HOL/
haftmann@28952
  1799
    src/HOL/Real/Real.thy ~> src/HOL/
haftmann@28952
  1800
    src/HOL/Complex/Complex_Main.thy ~> src/HOL/
haftmann@28952
  1801
    src/HOL/Complex/Complex.thy ~> src/HOL/
huffman@30176
  1802
    src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/Library/
huffman@30176
  1803
    src/HOL/Complex/Fundamental_Theorem_Algebra.thy ~> src/HOL/Library/
haftmann@28952
  1804
    src/HOL/Hyperreal/Deriv.thy ~> src/HOL/
haftmann@28952
  1805
    src/HOL/Hyperreal/Fact.thy ~> src/HOL/
haftmann@28952
  1806
    src/HOL/Hyperreal/Integration.thy ~> src/HOL/
haftmann@28952
  1807
    src/HOL/Hyperreal/Lim.thy ~> src/HOL/
haftmann@28952
  1808
    src/HOL/Hyperreal/Ln.thy ~> src/HOL/
haftmann@28952
  1809
    src/HOL/Hyperreal/Log.thy ~> src/HOL/
haftmann@28952
  1810
    src/HOL/Hyperreal/MacLaurin.thy ~> src/HOL/
haftmann@28952
  1811
    src/HOL/Hyperreal/NthRoot.thy ~> src/HOL/
haftmann@28952
  1812
    src/HOL/Hyperreal/Series.thy ~> src/HOL/
haftmann@29197
  1813
    src/HOL/Hyperreal/SEQ.thy ~> src/HOL/
haftmann@28952
  1814
    src/HOL/Hyperreal/Taylor.thy ~> src/HOL/
haftmann@28952
  1815
    src/HOL/Hyperreal/Transcendental.thy ~> src/HOL/
haftmann@28952
  1816
    src/HOL/Real/Float ~> src/HOL/Library/
haftmann@29197
  1817
    src/HOL/Real/HahnBanach ~> src/HOL/HahnBanach
haftmann@29197
  1818
    src/HOL/Real/RealVector.thy ~> src/HOL/
haftmann@28952
  1819
haftmann@28952
  1820
    src/HOL/arith_data.ML ~> src/HOL/Tools
haftmann@28952
  1821
    src/HOL/hologic.ML ~> src/HOL/Tools
haftmann@28952
  1822
    src/HOL/simpdata.ML ~> src/HOL/Tools
haftmann@28952
  1823
    src/HOL/int_arith1.ML ~> src/HOL/Tools/int_arith.ML
haftmann@28952
  1824
    src/HOL/int_factor_simprocs.ML ~> src/HOL/Tools
haftmann@28952
  1825
    src/HOL/nat_simprocs.ML ~> src/HOL/Tools
haftmann@28952
  1826
    src/HOL/Real/float_arith.ML ~> src/HOL/Tools
haftmann@28952
  1827
    src/HOL/Real/float_syntax.ML ~> src/HOL/Tools
haftmann@28952
  1828
    src/HOL/Real/rat_arith.ML ~> src/HOL/Tools
haftmann@28952
  1829
    src/HOL/Real/real_arith.ML ~> src/HOL/Tools
haftmann@28952
  1830
haftmann@29398
  1831
    src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL
haftmann@29398
  1832
    src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL
haftmann@29398
  1833
    src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL
haftmann@29398
  1834
    src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL
haftmann@29398
  1835
    src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL
haftmann@29398
  1836
    src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL
haftmann@29398
  1837
wenzelm@30845
  1838
* If methods "eval" and "evaluation" encounter a structured proof
wenzelm@30845
  1839
state with !!/==>, only the conclusion is evaluated to True (if
wenzelm@30845
  1840
possible), avoiding strange error messages.
wenzelm@30845
  1841
wenzelm@30845
  1842
* Method "sizechange" automates termination proofs using (a
wenzelm@30845
  1843
modification of) the size-change principle.  Requires SAT solver.  See
wenzelm@30845
  1844
src/HOL/ex/Termination.thy for examples.
wenzelm@30845
  1845
wenzelm@30845
  1846
* Simplifier: simproc for let expressions now unfolds if bound
wenzelm@30845
  1847
variable occurs at most once in let expression body.  INCOMPATIBILITY.
wenzelm@30845
  1848
wenzelm@30845
  1849
* Method "arith": Linear arithmetic now ignores all inequalities when
wenzelm@30845
  1850
fast_arith_neq_limit is exceeded, instead of giving up entirely.
wenzelm@30845
  1851
wenzelm@30845
  1852
* New attribute "arith" for facts that should always be used
wenzelm@30845
  1853
automatically by arithmetic. It is intended to be used locally in
wenzelm@30845
  1854
proofs, e.g.
wenzelm@30845
  1855
wenzelm@30845
  1856
  assumes [arith]: "x > 0"
wenzelm@30845
  1857
nipkow@30706
  1858
Global usage is discouraged because of possible performance impact.
nipkow@30706
  1859
wenzelm@30845
  1860
* New classes "top" and "bot" with corresponding operations "top" and
wenzelm@30845
  1861
"bot" in theory Orderings; instantiation of class "complete_lattice"
wenzelm@30845
  1862
requires instantiation of classes "top" and "bot".  INCOMPATIBILITY.
wenzelm@30845
  1863
wenzelm@30845
  1864
* Changed definition lemma "less_fun_def" in order to provide an
wenzelm@30845
  1865
instance for preorders on functions; use lemma "less_le" instead.
wenzelm@30845
  1866
INCOMPATIBILITY.
wenzelm@30845
  1867
wenzelm@30845
  1868
* Theory Orderings: class "wellorder" moved here, with explicit
wenzelm@30845
  1869
induction rule "less_induct" as assumption.  For instantiation of
wenzelm@30845
  1870
"wellorder" by means of predicate "wf", use rule wf_wellorderI.
wenzelm@30845
  1871
INCOMPATIBILITY.
wenzelm@30845
  1872
wenzelm@30845
  1873
* Theory Orderings: added class "preorder" as superclass of "order".
wenzelm@27793
  1874
INCOMPATIBILITY: Instantiation proofs for order, linorder
wenzelm@27793
  1875
etc. slightly changed.  Some theorems named order_class.* now named
wenzelm@27793
  1876
preorder_class.*.
wenzelm@27793
  1877
wenzelm@30845
  1878
* Theory Relation: renamed "refl" to "refl_on", "reflexive" to "refl,
wenzelm@30845
  1879
"diag" to "Id_on".
wenzelm@30845
  1880
wenzelm@30845
  1881
* Theory Finite_Set: added a new fold combinator of type
wenzelm@30845
  1882
nipkow@28855
  1883
  ('a => 'b => 'b) => 'b => 'a set => 'b
wenzelm@30845
  1884
wenzelm@30845
  1885
Occasionally this is more convenient than the old fold combinator
wenzelm@30845
  1886
which is now defined in terms of the new one and renamed to
wenzelm@30845
  1887
fold_image.
wenzelm@30845
  1888
wenzelm@30845
  1889
* Theories Ring_and_Field and OrderedGroup: The lemmas "group_simps"
wenzelm@30845
  1890
and "ring_simps" have been replaced by "algebra_simps" (which can be
wenzelm@30845
  1891
extended with further lemmas!).  At the moment both still exist but
wenzelm@30845
  1892
the former will disappear at some point.
wenzelm@30845
  1893
wenzelm@30845
  1894
* Theory Power: Lemma power_Suc is now declared as a simp rule in
wenzelm@30845
  1895
class recpower.  Type-specific simp rules for various recpower types
wenzelm@30845
  1896
have been removed.  INCOMPATIBILITY, rename old lemmas as follows:
huffman@30273
  1897
huffman@30273
  1898
rat_power_0    -> power_0
huffman@30273
  1899
rat_power_Suc  -> power_Suc
huffman@30273
  1900
realpow_0      -> power_0
huffman@30273
  1901
realpow_Suc    -> power_Suc
huffman@30273
  1902
complexpow_0   -> power_0
huffman@30273
  1903
complexpow_Suc -> power_Suc
huffman@30273
  1904
power_poly_0   -> power_0
huffman@30273
  1905
power_poly_Suc -> power_Suc
huffman@30273
  1906
wenzelm@30845
  1907
* Theories Ring_and_Field and Divides: Definition of "op dvd" has been
wenzelm@27793
  1908
moved to separate class dvd in Ring_and_Field; a couple of lemmas on
wenzelm@27793
  1909
dvd has been generalized to class comm_semiring_1.  Likewise a bunch
wenzelm@27793
  1910
of lemmas from Divides has been generalized from nat to class
wenzelm@27793
  1911
semiring_div.  INCOMPATIBILITY.  This involves the following theorem
wenzelm@27793
  1912
renames resulting from duplicate elimination:
haftmann@27651
  1913
haftmann@27651
  1914
    dvd_def_mod ~>          dvd_eq_mod_eq_0
haftmann@27651
  1915
    zero_dvd_iff ~>         dvd_0_left_iff
haftmann@28559
  1916
    dvd_0 ~>                dvd_0_right
haftmann@27651
  1917
    DIVISION_BY_ZERO_DIV ~> div_by_0
haftmann@27651
  1918
    DIVISION_BY_ZERO_MOD ~> mod_by_0
haftmann@27651
  1919
    mult_div ~>             div_mult_self2_is_id
haftmann@27651
  1920
    mult_mod ~>             mod_mult_self2_is_0
haftmann@27651
  1921
wenzelm@30845
  1922
* Theory IntDiv: removed many lemmas that are instances of class-based
wenzelm@30845
  1923
generalizations (from Divides and Ring_and_Field).  INCOMPATIBILITY,
wenzelm@30845
  1924
rename old lemmas as follows:
nipkow@30044
  1925
nipkow@30044
  1926
dvd_diff               -> nat_dvd_diff
nipkow@30044
  1927
dvd_zminus_iff         -> dvd_minus_iff
nipkow@30224
  1928
mod_add1_eq            -> mod_add_eq
nipkow@30224
  1929
mod_mult1_eq           -> mod_mult_right_eq
nipkow@30224
  1930
mod_mult1_eq'          -> mod_mult_left_eq
nipkow@30224
  1931
mod_mult_distrib_mod   -> mod_mult_eq
nipkow@30044
  1932
nat_mod_add_left_eq    -> mod_add_left_eq
nipkow@30044
  1933
nat_mod_add_right_eq   -> mod_add_right_eq
nipkow@30044
  1934
nat_mod_div_trivial    -> mod_div_trivial
nipkow@30044
  1935
nat_mod_mod_trivial    -> mod_mod_trivial
nipkow@30044
  1936
zdiv_zadd_self1        -> div_add_self1
nipkow@30044
  1937
zdiv_zadd_self2        -> div_add_self2
nipkow@30181
  1938
zdiv_zmult_self1       -> div_mult_self2_is_id
nipkow@30044
  1939
zdiv_zmult_self2       -> div_mult_self1_is_id
nipkow@30044
  1940
zdvd_triv_left         -> dvd_triv_left
nipkow@30044
  1941
zdvd_triv_right        -> dvd_triv_right
nipkow@30044
  1942
zdvd_zmult_cancel_disj -> dvd_mult_cancel_left
nipkow@30085
  1943
zmod_eq0_zdvd_iff      -> dvd_eq_mod_eq_0[symmetric]
nipkow@30044
  1944
zmod_zadd_left_eq      -> mod_add_left_eq
nipkow@30044
  1945
zmod_zadd_right_eq     -> mod_add_right_eq
nipkow@30044
  1946
zmod_zadd_self1        -> mod_add_self1
nipkow@30044
  1947
zmod_zadd_self2        -> mod_add_self2
nipkow@30224
  1948
zmod_zadd1_eq          -> mod_add_eq
nipkow@30044
  1949
zmod_zdiff1_eq         -> mod_diff_eq
nipkow@30044
  1950
zmod_zdvd_zmod         -> mod_mod_cancel
nipkow@30044
  1951
zmod_zmod_cancel       -> mod_mod_cancel
nipkow@30044
  1952
zmod_zmult_self1       -> mod_mult_self2_is_0
nipkow@30044
  1953
zmod_zmult_self2       -> mod_mult_self1_is_0
nipkow@30044
  1954
zmod_1                 -> mod_by_1
nipkow@30044
  1955
zdiv_1                 -> div_by_1
nipkow@30044
  1956
zdvd_abs1              -> abs_dvd_iff
nipkow@30044
  1957
zdvd_abs2              -> dvd_abs_iff
nipkow@30044
  1958
zdvd_refl              -> dvd_refl
nipkow@30044
  1959
zdvd_trans             -> dvd_trans
nipkow@30044
  1960
zdvd_zadd              -> dvd_add
nipkow@30044
  1961
zdvd_zdiff             -> dvd_diff
nipkow@30044
  1962
zdvd_zminus_iff        -> dvd_minus_iff
nipkow@30044
  1963
zdvd_zminus2_iff       -> minus_dvd_iff
nipkow@30044
  1964
zdvd_zmultD            -> dvd_mult_right
nipkow@30044
  1965
zdvd_zmultD2           -> dvd_mult_left
nipkow@30044
  1966
zdvd_zmult_mono        -> mult_dvd_mono
nipkow@30044
  1967
zdvd_0_right           -> dvd_0_right
nipkow@30044
  1968
zdvd_0_left            -> dvd_0_left_iff
nipkow@30044
  1969
zdvd_1_left            -> one_dvd
nipkow@30044
  1970
zminus_dvd_iff         -> minus_dvd_iff
nipkow@30044
  1971
wenzelm@30845
  1972
* Theory Rational: 'Fract k 0' now equals '0'.  INCOMPATIBILITY.
wenzelm@30845
  1973
wenzelm@30845
  1974
* The real numbers offer decimal input syntax: 12.34 is translated
wenzelm@30845
  1975
into 1234/10^2. This translation is not reversed upon output.
wenzelm@30845
  1976
wenzelm@30845
  1977
* Theory Library/Polynomial defines an abstract type 'a poly of
wenzelm@30845
  1978
univariate polynomials with coefficients of type 'a.  In addition to
wenzelm@30845
  1979
the standard ring operations, it also supports div and mod.  Code
wenzelm@30845
  1980
generation is also supported, using list-style constructors.
wenzelm@30845
  1981
wenzelm@30845
  1982
* Theory Library/Inner_Product defines a class of real_inner for real
wenzelm@30845
  1983
inner product spaces, with an overloaded operation inner :: 'a => 'a
wenzelm@30845
  1984
=> real.  Class real_inner is a subclass of real_normed_vector from
wenzelm@30845
  1985
theory RealVector.
wenzelm@30845
  1986
wenzelm@30845
  1987
* Theory Library/Product_Vector provides instances for the product
wenzelm@30845
  1988
type 'a * 'b of several classes from RealVector and Inner_Product.
wenzelm@30845
  1989
Definitions of addition, subtraction, scalar multiplication, norms,
wenzelm@30845
  1990
and inner products are included.
wenzelm@30845
  1991
wenzelm@30845
  1992
* Theory Library/Bit defines the field "bit" of integers modulo 2.  In
wenzelm@30845
  1993
addition to the field operations, numerals and case syntax are also
wenzelm@30845
  1994
supported.
wenzelm@30845
  1995
wenzelm@30845
  1996
* Theory Library/Diagonalize provides constructive version of Cantor's
wenzelm@30845
  1997
first diagonalization argument.
wenzelm@30845
  1998
wenzelm@30845
  1999
* Theory Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,
wenzelm@27599
  2000
zlcm (for int); carried together from various gcd/lcm developements in
wenzelm@30845
  2001
the HOL Distribution.  Constants zgcd and zlcm replace former igcd and
wenzelm@30845
  2002
ilcm; corresponding theorems renamed accordingly.  INCOMPATIBILITY,
wenzelm@30845
  2003
may recover tupled syntax as follows:
haftmann@27556
  2004
haftmann@27556
  2005
    hide (open) const gcd
haftmann@27556
  2006
    abbreviation gcd where
haftmann@27556
  2007
      "gcd == (%(a, b). GCD.gcd a b)"
haftmann@27556
  2008
    notation (output)
haftmann@27556
  2009
      GCD.gcd ("gcd '(_, _')")
haftmann@27556
  2010
wenzelm@30845
  2011
The same works for lcm, zgcd, zlcm.
wenzelm@30845
  2012
wenzelm@30845
  2013
* Theory Library/Nat_Infinity: added addition, numeral syntax and more
wenzelm@30845
  2014
instantiations for algebraic structures.  Removed some duplicate
wenzelm@30845
  2015
theorems.  Changes in simp rules.  INCOMPATIBILITY.
wenzelm@30845
  2016
wenzelm@30845
  2017
* ML antiquotation @{code} takes a constant as argument and generates
haftmann@27651
  2018
corresponding code in background and inserts name of the corresponding
haftmann@27651
  2019
resulting ML value/function/datatype constructor binding in place.
haftmann@27651
  2020
All occurrences of @{code} with a single ML block are generated
haftmann@27651
  2021
simultaneously.  Provides a generic and safe interface for
wenzelm@30845
  2022
instrumentalizing code generation.  See
wenzelm@30845
  2023
src/HOL/Decision_Procs/Ferrack.thy for a more ambitious application.
wenzelm@30845
  2024
In future you ought to refrain from ad-hoc compiling generated SML
wenzelm@30845
  2025
code on the ML toplevel.  Note that (for technical reasons) @{code}
wenzelm@30845
  2026
cannot refer to constants for which user-defined serializations are
wenzelm@30845
  2027
set.  Refer to the corresponding ML counterpart directly in that
wenzelm@30845
  2028
cases.
wenzelm@27122
  2029
wenzelm@27122
  2030
* Command 'rep_datatype': instead of theorem names the command now
wenzelm@27122
  2031
takes a list of terms denoting the constructors of the type to be
wenzelm@27122
  2032
represented as datatype.  The characteristic theorems have to be
wenzelm@27122
  2033
proven.  INCOMPATIBILITY.  Also observe that the following theorems
wenzelm@27122
  2034
have disappeared in favour of existing ones:
wenzelm@27122
  2035
haftmann@27104
  2036
    unit_induct                 ~> unit.induct
haftmann@27104
  2037
    prod_induct                 ~> prod.induct
haftmann@27104
  2038
    sum_induct                  ~> sum.induct
haftmann@27104
  2039
    Suc_Suc_eq                  ~> nat.inject
haftmann@27104
  2040
    Suc_not_Zero Zero_not_Suc   ~> nat.distinct
haftmann@27104
  2041
haftmann@27104
  2042
ballarin@27696
  2043
*** HOL-Algebra ***
ballarin@27696
  2044
ballarin@27713
  2045
* New locales for orders and lattices where the equivalence relation
wenzelm@30106
  2046
is not restricted to equality.  INCOMPATIBILITY: all order and lattice
wenzelm@30106
  2047
locales use a record structure with field eq for the equivalence.
ballarin@27713
  2048
ballarin@27713
  2049
* New theory of factorial domains.
ballarin@27713
  2050
wenzelm@30845
  2051
* Units_l_inv and Units_r_inv are now simp rules by default.
ballarin@27696
  2052
INCOMPATIBILITY.  Simplifier proof that require deletion of l_inv
ballarin@27696
  2053
and/or r_inv will now also require deletion of these lemmas.
ballarin@27696
  2054
wenzelm@30845
  2055
* Renamed the following theorems, INCOMPATIBILITY:
wenzelm@30845
  2056
ballarin@27696
  2057
UpperD ~> Upper_memD
ballarin@27696
  2058
LowerD ~> Lower_memD
ballarin@27696
  2059
least_carrier ~> least_closed
ballarin@27696
  2060
greatest_carrier ~> greatest_closed
ballarin@27696
  2061
greatest_Lower_above ~> greatest_Lower_below
ballarin@27717
  2062
one_zero ~> carrier_one_zero
ballarin@27717
  2063
one_not_zero ~> carrier_one_not_zero  (collision with assumption)
ballarin@27696
  2064
wenzelm@27793
  2065
wenzelm@30849
  2066
*** HOL-Nominal ***
wenzelm@30849
  2067
wenzelm@30855
  2068
* Nominal datatypes can now contain type-variables.
wenzelm@30855
  2069
wenzelm@30855
  2070
* Commands 'nominal_inductive' and 'equivariance' work with local
wenzelm@30855
  2071
theory targets.
wenzelm@30855
  2072
wenzelm@30855
  2073
* Nominal primrec can now works with local theory targets and its
wenzelm@30855
  2074
specification syntax now conforms to the general format as seen in
wenzelm@30855
  2075
'inductive' etc.
wenzelm@30855
  2076
wenzelm@30855
  2077
* Method "perm_simp" honours the standard simplifier attributes
wenzelm@30855
  2078
(no_asm), (no_asm_use) etc.
wenzelm@30855
  2079
wenzelm@30855
  2080
* The new predicate #* is defined like freshness, except that on the
wenzelm@30855
  2081
left hand side can be a set or list of atoms.
wenzelm@30855
  2082
wenzelm@30855
  2083
* Experimental command 'nominal_inductive2' derives strong induction
wenzelm@30855
  2084
principles for inductive definitions.  In contrast to
wenzelm@30855
  2085
'nominal_inductive', which can only deal with a fixed number of
wenzelm@30855
  2086
binders, it can deal with arbitrary expressions standing for sets of
wenzelm@30855
  2087
atoms to be avoided.  The only inductive definition we have at the
wenzelm@30855
  2088
moment that needs this generalisation is the typing rule for Lets in
wenzelm@30855
  2089
the algorithm W:
wenzelm@30855
  2090
wenzelm@30855
  2091
 Gamma |- t1 : T1   (x,close Gamma T1)::Gamma |- t2 : T2   x#Gamma
wenzelm@30855
  2092
 -----------------------------------------------------------------
wenzelm@30855
  2093
         Gamma |- Let x be t1 in t2 : T2
wenzelm@30855
  2094
wenzelm@30855
  2095
In this rule one wants to avoid all the binders that are introduced by
wenzelm@30855
  2096
"close Gamma T1".  We are looking for other examples where this
wenzelm@30855
  2097
feature might be useful.  Please let us know.
wenzelm@30849
  2098
wenzelm@30849
  2099
huffman@30176
  2100
*** HOLCF ***
huffman@30176
  2101
huffman@30176
  2102
* Reimplemented the simplification procedure for proving continuity
huffman@30176
  2103
subgoals.  The new simproc is extensible; users can declare additional
huffman@30176
  2104
continuity introduction rules with the attribute [cont2cont].
huffman@30176
  2105
huffman@30176
  2106
* The continuity simproc now uses a different introduction rule for
huffman@30176
  2107
solving continuity subgoals on terms with lambda abstractions.  In
huffman@30176
  2108
some rare cases the new simproc may fail to solve subgoals that the
huffman@30176
  2109
old one could solve, and "simp add: cont2cont_LAM" may be necessary.
huffman@30176
  2110
Potential INCOMPATIBILITY.
huffman@30176
  2111
wenzelm@30847
  2112
* Command 'fixrec': specification syntax now conforms to the general
wenzelm@30855
  2113
format as seen in 'inductive' etc.  See src/HOLCF/ex/Fixrec_ex.thy for
wenzelm@30855
  2114
examples.  INCOMPATIBILITY.
wenzelm@30845
  2115
wenzelm@30845
  2116
wenzelm@30845
  2117
*** ZF ***
wenzelm@30845
  2118
wenzelm@30845
  2119
* Proof of Zorn's Lemma for partial orders.
huffman@30176
  2120
huffman@30176
  2121
wenzelm@27246
  2122
*** ML ***
wenzelm@28088
  2123
wenzelm@30845
  2124
* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for
wenzelm@30845
  2125
Poly/ML 5.2.1 or later.  Important note: the TimeLimit facility
wenzelm@30845
  2126
depends on multithreading, so timouts will not work before Poly/ML
wenzelm@30845
  2127
5.2.1!
wenzelm@30845
  2128
wenzelm@29161
  2129
* High-level support for concurrent ML programming, see
wenzelm@29161
  2130
src/Pure/Cuncurrent.  The data-oriented model of "future values" is
wenzelm@29161
  2131
particularly convenient to organize independent functional
wenzelm@29161
  2132
computations.  The concept of "synchronized variables" provides a
wenzelm@29161
  2133
higher-order interface for components with shared state, avoiding the
wenzelm@30845
  2134
delicate details of mutexes and condition variables.  (Requires
wenzelm@30845
  2135
Poly/ML 5.2.1 or later.)
wenzelm@30845
  2136
wenzelm@30845
  2137
* ML bindings produced via Isar commands are stored within the Isar
wenzelm@30845
  2138
context (theory or proof).  Consequently, commands like 'use' and 'ML'
wenzelm@30845
  2139
become thread-safe and work with undo as expected (concerning
wenzelm@30845
  2140
top-level bindings, not side-effects on global references).
wenzelm@30845
  2141
INCOMPATIBILITY, need to provide proper Isar context when invoking the
wenzelm@30845
  2142
compiler at runtime; really global bindings need to be given outside a
wenzelm@30845
  2143
theory.  (Requires Poly/ML 5.2 or later.)
wenzelm@30845
  2144
wenzelm@30845
  2145
* Command 'ML_prf' is analogous to 'ML' but works within a proof
wenzelm@30845
  2146
context.  Top-level ML bindings are stored within the proof context in
wenzelm@30845
  2147
a purely sequential fashion, disregarding the nested proof structure.
wenzelm@30845
  2148
ML bindings introduced by 'ML_prf' are discarded at the end of the
wenzelm@30845
  2149
proof.  (Requires Poly/ML 5.2 or later.)
wenzelm@29161
  2150
wenzelm@30530
  2151
* Simplified ML attribute and method setup, cf. functions Attrib.setup
wenzelm@30845
  2152
and Method.setup, as well as Isar commands 'attribute_setup' and
wenzelm@30547
  2153
'method_setup'.  INCOMPATIBILITY for 'method_setup', need to simplify
wenzelm@30547
  2154
existing code accordingly, or use plain 'setup' together with old
wenzelm@30547
  2155
Method.add_method.
wenzelm@30530
  2156
wenzelm@28294
  2157
* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
wenzelm@28294
  2158
to 'a -> thm, while results are always tagged with an authentic oracle
wenzelm@28294
  2159
name.  The Isar command 'oracle' is now polymorphic, no argument type
wenzelm@28294
  2160
is specified.  INCOMPATIBILITY, need to simplify existing oracle code
wenzelm@28294
  2161
accordingly.  Note that extra performance may be gained by producing
wenzelm@28294
  2162
the cterm carefully, avoiding slow Thm.cterm_of.
wenzelm@28294
  2163
wenzelm@30845
  2164
* Simplified interface for defining document antiquotations via
wenzelm@30845
  2165
ThyOutput.antiquotation, ThyOutput.output, and optionally
wenzelm@30845
  2166
ThyOutput.maybe_pretty_source.  INCOMPATIBILITY, need to simplify user
wenzelm@30845
  2167
antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common
wenzelm@30845
  2168
examples.
wenzelm@28099
  2169
wenzelm@30395
  2170
* More systematic treatment of long names, abstract name bindings, and
wenzelm@30395
  2171
name space operations.  Basic operations on qualified names have been
wenzelm@30399
  2172
move from structure NameSpace to Long_Name, e.g. Long_Name.base_name,
wenzelm@30395
  2173
Long_Name.append.  Old type bstring has been mostly replaced by
wenzelm@30395
  2174
abstract type binding (see structure Binding), which supports precise
wenzelm@30845
  2175
qualification by packages and local theory targets, as well as proper
wenzelm@30845
  2176
tracking of source positions.  INCOMPATIBILITY, need to wrap old
wenzelm@30845
  2177
bstring values into Binding.name, or better pass through abstract
wenzelm@30399
  2178
bindings everywhere.  See further src/Pure/General/long_name.ML,
wenzelm@30395
  2179
src/Pure/General/binding.ML and src/Pure/General/name_space.ML
wenzelm@30395
  2180
wenzelm@28089
  2181
* Result facts (from PureThy.note_thms, ProofContext.note_thms,
wenzelm@28089
  2182
LocalTheory.note etc.) now refer to the *full* internal name, not the
wenzelm@28089
  2183
bstring as before.  INCOMPATIBILITY, not detected by ML type-checking!
wenzelm@28089
  2184
wenzelm@27287
  2185
* Disposed old type and term read functions (Sign.read_def_typ,
wenzelm@27287
  2186
Sign.read_typ, Sign.read_def_terms, Sign.read_term,
wenzelm@27287
  2187
Thm.read_def_cterms, Thm.read_cterm etc.).  INCOMPATIBILITY, should
wenzelm@27287
  2188
use regular Syntax.read_typ, Syntax.read_term, Syntax.read_typ_global,
wenzelm@27269
  2189
Syntax.read_term_global etc.; see also OldGoals.read_term as last
wenzelm@27269
  2190
resort for legacy applications.
wenzelm@27269
  2191
wenzelm@30609
  2192
* Disposed old declarations, tactics, tactic combinators that refer to
wenzelm@30609
  2193
the simpset or claset of an implicit theory (such as Addsimps,
wenzelm@30609
  2194
Simp_tac, SIMPSET).  INCOMPATIBILITY, should use @{simpset} etc. in
wenzelm@30609
  2195
embedded ML text, or local_simpset_of with a proper context passed as
wenzelm@30609
  2196
explicit runtime argument.
wenzelm@30609
  2197
wenzelm@30845
  2198
* Rules and tactics that read instantiations (read_instantiate,
wenzelm@30845
  2199
res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
wenzelm@30845
  2200
context, which is required for parsing and type-checking.  Moreover,
wenzelm@30845
  2201
the variables are specified as plain indexnames, not string encodings
wenzelm@30845
  2202
thereof.  INCOMPATIBILITY.
wenzelm@30845
  2203
wenzelm@30845
  2204
* Generic Toplevel.add_hook interface allows to analyze the result of
wenzelm@30845
  2205
transactions.  E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML
wenzelm@30845
  2206
for theorem dependency output of transactions resulting in a new
wenzelm@30845
  2207
theory state.
wenzelm@30845
  2208
wenzelm@30845
  2209
* ML antiquotations: block-structured compilation context indicated by
wenzelm@27391
  2210
\<lbrace> ... \<rbrace>; additional antiquotation forms:
wenzelm@27391
  2211
wenzelm@30845
  2212
  @{binding name}                         - basic name binding
wenzelm@27519
  2213
  @{let ?pat = term}                      - term abbreviation (HO matching)
wenzelm@27519
  2214
  @{note name = fact}                     - fact abbreviation
wenzelm@27519
  2215
  @{thm fact}                             - singleton fact (with attributes)
wenzelm@27519
  2216
  @{thms fact}                            - general fact (with attributes)
wenzelm@27519
  2217
  @{lemma prop by method}                 - singleton goal
wenzelm@27519
  2218
  @{lemma prop by meth1 meth2}            - singleton goal
wenzelm@27519
  2219
  @{lemma prop1 ... propN by method}      - general goal
wenzelm@27519
  2220
  @{lemma prop1 ... propN by meth1 meth2} - general goal
wenzelm@27519
  2221
  @{lemma (open) ...}                     - open derivation
wenzelm@27380
  2222
wenzelm@27246
  2223
wenzelm@27979
  2224
*** System ***
wenzelm@27979
  2225
wenzelm@28248
  2226
* The Isabelle "emacs" tool provides a specific interface to invoke
wenzelm@28248
  2227
Proof General / Emacs, with more explicit failure if that is not
wenzelm@28248
  2228
installed (the old isabelle-interface script silently falls back on
wenzelm@28248
  2229
isabelle-process).  The PROOFGENERAL_HOME setting determines the
wenzelm@28248
  2230
installation location of the Proof General distribution.
wenzelm@28248
  2231
wenzelm@27979
  2232
* Isabelle/lib/classes/Pure.jar provides basic support to integrate
wenzelm@27979
  2233
the Isabelle process into a JVM/Scala application.  See
wenzelm@27979
  2234
Isabelle/lib/jedit/plugin for a minimal example.  (The obsolete Java
wenzelm@27979
  2235
process wrapper has been discontinued.)
wenzelm@27979
  2236
wenzelm@30845
  2237
* Added homegrown Isabelle font with unicode layout, see lib/fonts.
wenzelm@30845
  2238
wenzelm@30845
  2239
* Various status messages (with exact source position information) are
wenzelm@27979
  2240
emitted, if proper markup print mode is enabled.  This allows
wenzelm@27979
  2241
user-interface components to provide detailed feedback on internal
wenzelm@27979
  2242
prover operations.
wenzelm@27979
  2243
wenzelm@27979
  2244
wenzelm@27143
  2245
wenzelm@27008
  2246
New in Isabelle2008 (June 2008)
wenzelm@27008
  2247
-------------------------------
wenzelm@25464
  2248
wenzelm@25522
  2249
*** General ***
wenzelm@25522
  2250
wenzelm@27061
  2251
* The Isabelle/Isar Reference Manual (isar-ref) has been reorganized
wenzelm@27061
  2252
and updated, with formally checked references as hyperlinks.
wenzelm@27061
  2253
wenzelm@25994
  2254
* Theory loader: use_thy (and similar operations) no longer set the
wenzelm@25994
  2255
implicit ML context, which was occasionally hard to predict and in
wenzelm@25994
  2256
conflict with concurrency.  INCOMPATIBILITY, use ML within Isar which
wenzelm@25994
  2257
provides a proper context already.
wenzelm@25994
  2258
wenzelm@26323
  2259
* Theory loader: old-style ML proof scripts being *attached* to a thy
wenzelm@26323
  2260
file are no longer supported.  INCOMPATIBILITY, regular 'uses' and
wenzelm@26323
  2261
'use' within a theory file will do the job.
wenzelm@26323
  2262
wenzelm@26650
  2263
* Name space merge now observes canonical order, i.e. the second space
wenzelm@26650
  2264
is inserted into the first one, while existing entries in the first
wenzelm@26659
  2265
space take precedence.  INCOMPATIBILITY in rare situations, may try to
wenzelm@26650
  2266
swap theory imports.
wenzelm@26650
  2267
wenzelm@27067
  2268
* Syntax: symbol \<chi> is now considered a letter.  Potential
wenzelm@27067
  2269
INCOMPATIBILITY in identifier syntax etc.
wenzelm@27067
  2270
wenzelm@27067
  2271
* Outer syntax: string tokens no longer admit escaped white space,
wenzelm@27067
  2272
which was an accidental (undocumented) feature.  INCOMPATIBILITY, use
wenzelm@27067
  2273
white space without escapes.
wenzelm@27067
  2274
wenzelm@27067
  2275
* Outer syntax: string tokens may contain arbitrary character codes
wenzelm@27067
  2276
specified via 3 decimal digits (as in SML).  E.g. "foo\095bar" for
wenzelm@27067
  2277
"foo_bar".
wenzelm@27067
  2278
wenzelm@25522
  2279
haftmann@25502
  2280
*** Pure ***
haftmann@25502
  2281
wenzelm@26718
  2282
* Context-dependent token translations.  Default setup reverts locally
wenzelm@26718
  2283
fixed variables, and adds hilite markup for undeclared frees.
wenzelm@26718
  2284
berghofe@26681
  2285
* Unused theorems can be found using the new command 'unused_thms'.
berghofe@26681
  2286
There are three ways of invoking it:
berghofe@26681
  2287
berghofe@26681
  2288
(1) unused_thms
berghofe@26681
  2289
     Only finds unused theorems in the current theory.
berghofe@26681
  2290
berghofe@26681
  2291
(2) unused_thms thy_1 ... thy_n -
berghofe@26681
  2292
     Finds unused theorems in the current theory and all of its ancestors,
berghofe@26681
  2293
     excluding the theories thy_1 ... thy_n and all of their ancestors.
berghofe@26681
  2294
berghofe@26681
  2295
(3) unused_thms thy_1 ... thy_n - thy'_1 ... thy'_m
berghofe@26681
  2296
     Finds unused theorems in the theories thy'_1 ... thy'_m and all of
berghofe@26681
  2297
     their ancestors, excluding the theories thy_1 ... thy_n and all of
berghofe@26681
  2298
     their ancestors.
berghofe@26681
  2299
wenzelm@26718
  2300
In order to increase the readability of the list produced by
wenzelm@26718
  2301
unused_thms, theorems that have been created by a particular instance
wenzelm@26874
  2302
of a theory command such as 'inductive' or 'function' are considered
wenzelm@26874
  2303
to belong to the same "group", meaning that if at least one theorem in
wenzelm@26718
  2304
this group is used, the other theorems in the same group are no longer
wenzelm@26718
  2305
reported as unused.  Moreover, if all theorems in the group are
wenzelm@26718
  2306
unused, only one theorem in the group is displayed.
wenzelm@26718
  2307
wenzelm@26718
  2308
Note that proof objects have to be switched on in order for
wenzelm@26718
  2309
unused_thms to work properly (i.e. !proofs must be >= 1, which is
wenzelm@26874
  2310
usually the case when using Proof General with the default settings).
berghofe@26681
  2311
wenzelm@26650
  2312
* Authentic naming of facts disallows ad-hoc overwriting of previous
wenzelm@26650
  2313
theorems within the same name space.  INCOMPATIBILITY, need to remove
wenzelm@26650
  2314
duplicate fact bindings, or even accidental fact duplications.  Note
wenzelm@26650
  2315
that tools may maintain dynamically scoped facts systematically, using
wenzelm@26650
  2316
PureThy.add_thms_dynamic.
wenzelm@26650
  2317
wenzelm@26660
  2318
* Command 'hide' now allows to hide from "fact" name space as well.
wenzelm@26660
  2319
wenzelm@26496
  2320
* Eliminated destructive theorem database, simpset, claset, and
wenzelm@26496
  2321
clasimpset.  Potential INCOMPATIBILITY, really need to observe linear
wenzelm@26496
  2322
update of theories within ML code.
wenzelm@26479
  2323
wenzelm@26955
  2324
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm@26955
  2325
INCOMPATIBILITY, object-logics depending on former Pure require
wenzelm@26955
  2326
additional setup PureThy.old_appl_syntax_setup; object-logics
wenzelm@26955
  2327
depending on former CPure need to refer to Pure.
wenzelm@26650
  2328
wenzelm@26495
  2329
* Commands 'use' and 'ML' are now purely functional, operating on
wenzelm@26479
  2330
theory/local_theory.  Removed former 'ML_setup' (on theory), use 'ML'
wenzelm@26479
  2331
instead.  Added 'ML_val' as mere diagnostic replacement for 'ML'.
wenzelm@26479
  2332
INCOMPATIBILITY.
wenzelm@26479
  2333
wenzelm@26874
  2334
* Command 'setup': discontinued implicit version with ML reference.
wenzelm@26434
  2335
wenzelm@25970
  2336
* Instantiation target allows for simultaneous specification of class
wenzelm@25970
  2337
instance operations together with an instantiation proof.
wenzelm@25970
  2338
Type-checking phase allows to refer to class operations uniformly.
wenzelm@27067
  2339
See src/HOL/Complex/Complex.thy for an Isar example and
wenzelm@27067
  2340
src/HOL/Library/Eval.thy for an ML example.
haftmann@25502
  2341
wenzelm@26201
  2342
* Indexing of literal facts: be more serious about including only
wenzelm@26201
  2343
facts from the visible specification/proof context, but not the
wenzelm@26201
  2344
background context (locale etc.).  Affects `prop` notation and method
wenzelm@26201
  2345
"fact".  INCOMPATIBILITY: need to name facts explicitly in rare
wenzelm@26201
  2346
situations.
wenzelm@26201
  2347
wenzelm@26925
  2348
* Method "cases", "induct", "coinduct": removed obsolete/undocumented
wenzelm@26925
  2349
"(open)" option, which used to expose internal bound variables to the
wenzelm@26925
  2350
proof text.
wenzelm@26925
  2351
wenzelm@26925
  2352
* Isar statements: removed obsolete case "rule_context".
wenzelm@26925
  2353
INCOMPATIBILITY, better use explicit fixes/assumes.
wenzelm@26925
  2354
wenzelm@26874
  2355
* Locale proofs: default proof step now includes 'unfold_locales';
wenzelm@26874
  2356
hence 'proof' without argument may be used to unfold locale
wenzelm@26874
  2357
predicates.
ballarin@26765
  2358
ballarin@26765
  2359
haftmann@26762
  2360
*** Document preparation ***
haftmann@26762
  2361
wenzelm@26914
  2362
* Simplified pdfsetup.sty: color/hyperref is used unconditionally for
wenzelm@26914
  2363
both pdf and dvi (hyperlinks usually work in xdvi as well); removed
wenzelm@26914
  2364
obsolete thumbpdf setup (contemporary PDF viewers do this on the
wenzelm@26914
  2365
spot); renamed link color from "darkblue" to "linkcolor" (default
wenzelm@26920
  2366
value unchanged, can be redefined via \definecolor); no longer sets
wenzelm@26920
  2367
"a4paper" option (unnecessary or even intrusive).
wenzelm@26914
  2368
wenzelm@27008
  2369
* Antiquotation @{lemma A method} proves proposition A by the given
wenzelm@27008
  2370
method (either a method name or a method name plus (optional) method
wenzelm@27008
  2371
arguments in parentheses) and prints A just like @{prop A}.
haftmann@26762
  2372
haftmann@26762
  2373
wenzelm@25464
  2374
*** HOL ***
wenzelm@25464
  2375
wenzelm@27067
  2376
* New primrec package.  Specification syntax conforms in style to
wenzelm@27067
  2377
definition/function/....  No separate induction rule is provided.  The
wenzelm@27067
  2378
"primrec" command distinguishes old-style and new-style specifications
wenzelm@27067
  2379
by syntax.  The former primrec package is now named OldPrimrecPackage.
wenzelm@27067
  2380
When adjusting theories, beware: constants stemming from new-style
wenzelm@27067
  2381
primrec specifications have authentic syntax.
wenzelm@27067
  2382
wenzelm@27067
  2383
* Metis prover is now an order of magnitude faster, and also works
wenzelm@27067
  2384
with multithreading.
wenzelm@27067
  2385
wenzelm@27067
  2386
* Metis: the maximum number of clauses that can be produced from a
wenzelm@27067
  2387
theorem is now given by the attribute max_clauses.  Theorems that
wenzelm@27067
  2388
exceed this number are ignored, with a warning printed.
wenzelm@27067
  2389
wenzelm@27067
  2390
* Sledgehammer no longer produces structured proofs by default. To
wenzelm@27067
  2391
enable, declare [[sledgehammer_full = true]].  Attributes
wenzelm@27067
  2392
reconstruction_modulus, reconstruction_sorts renamed
wenzelm@27067
  2393
sledgehammer_modulus, sledgehammer_sorts.  INCOMPATIBILITY.
wenzelm@27067
  2394
haftmann@27104
  2395
* Method "induct_scheme" derives user-specified induction rules
wenzelm@27067
  2396
from well-founded induction and completeness of patterns. This factors
wenzelm@27067
  2397
out some operations that are done internally by the function package
wenzelm@27067
  2398
and makes them available separately.  See
wenzelm@27067
  2399
src/HOL/ex/Induction_Scheme.thy for examples.
wenzelm@27067
  2400
wenzelm@27067
  2401
* More flexible generation of measure functions for termination
wenzelm@27067
  2402
proofs: Measure functions can be declared by proving a rule of the
wenzelm@27067
  2403
form "is_measure f" and giving it the [measure_function] attribute.
wenzelm@27067
  2404
The "is_measure" predicate is logically meaningless (always true), and
wenzelm@27067
  2405
just guides the heuristic.  To find suitable measure functions, the
wenzelm@27067
  2406
termination prover sets up the goal "is_measure ?f" of the appropriate
wenzelm@27067
  2407
type and generates all solutions by prolog-style backwards proof using
wenzelm@27067
  2408
the declared rules.
wenzelm@27067
  2409
wenzelm@27067
  2410
This setup also deals with rules like 
wenzelm@27067
  2411
wenzelm@27067
  2412
  "is_measure f ==> is_measure (list_size f)"
wenzelm@27067
  2413
wenzelm@27067
  2414
which accommodates nested datatypes that recurse through lists.
wenzelm@27067
  2415
Similar rules are predeclared for products and option types.
wenzelm@27067
  2416
berghofe@26964
  2417
* Turned the type of sets "'a set" into an abbreviation for "'a => bool"
berghofe@26964
  2418
berghofe@26964
  2419
  INCOMPATIBILITIES:
berghofe@26964
  2420
wenzelm@27008
  2421
  - Definitions of overloaded constants on sets have to be replaced by
wenzelm@27008
  2422
    definitions on => and bool.
berghofe@26964
  2423
berghofe@26964
  2424
  - Some definitions of overloaded operators on sets can now be proved
wenzelm@27008
  2425
    using the definitions of the operators on => and bool.  Therefore,
wenzelm@27008
  2426
    the following theorems have been renamed:
berghofe@26964
  2427
berghofe@26964
  2428
      subset_def   -> subset_eq
berghofe@26964
  2429
      psubset_def  -> psubset_eq
berghofe@26964
  2430
      set_diff_def -> set_diff_eq
berghofe@26964
  2431
      Compl_def    -> Compl_eq
berghofe@26964
  2432
      Sup_set_def  -> Sup_set_eq
berghofe@26964
  2433
      Inf_set_def  -> Inf_set_eq
berghofe@26964
  2434
      sup_set_def  -> sup_set_eq
berghofe@26964
  2435
      inf_set_def  -> inf_set_eq
berghofe@26964
  2436
berghofe@26964
  2437
  - Due to the incompleteness of the HO unification algorithm, some
berghofe@26964
  2438
    rules such as subst may require manual instantiation, if some of
berghofe@26964
  2439
    the unknowns in the rule is a set.
berghofe@26964
  2440
berghofe@26964
  2441
  - Higher order unification and forward proofs:
berghofe@26964
  2442
    The proof pattern
berghofe@26964
  2443
berghofe@26964
  2444
      have "P (S::'a set)" <...>
berghofe@26964
  2445
      then have "EX S. P S" ..
berghofe@26964
  2446
wenzelm@27008
  2447
    no longer works (due to the incompleteness of the HO unification
wenzelm@27008
  2448
    algorithm) and must be replaced by the pattern
berghofe@26964
  2449
berghofe@26964
  2450
      have "EX S. P S"
berghofe@26964
  2451
      proof
berghofe@26964
  2452
        show "P S" <...>
berghofe@26964
  2453
      qed
berghofe@26964
  2454
berghofe@26964
  2455
  - Calculational reasoning with subst (or similar rules):
berghofe@26964
  2456
    The proof pattern
berghofe@26964
  2457
berghofe@26964
  2458
      have "P (S::'a set)" <...>
berghofe@26964
  2459
      also have "S = T" <...>
berghofe@26964
  2460
      finally have "P T" .
berghofe@26964
  2461
wenzelm@27008
  2462
    no longer works (for similar reasons as the previous example) and
wenzelm@27008
  2463
    must be replaced by something like
berghofe@26964
  2464
berghofe@26964
  2465
      have "P (S::'a set)" <...>
berghofe@26964
  2466
      moreover have "S = T" <...>
berghofe@26964
  2467
      ultimately have "P T" by simp
berghofe@26964
  2468
berghofe@26964
  2469
  - Tactics or packages written in ML code:
berghofe@26964
  2470
    Code performing pattern matching on types via
berghofe@26964
  2471
berghofe@26964
  2472
      Type ("set", [T]) => ...
berghofe@26964
  2473
wenzelm@27008
  2474
    must be rewritten. Moreover, functions like strip_type or
wenzelm@27008
  2475
    binder_types no longer return the right value when applied to a
wenzelm@27008
  2476
    type of the form
berghofe@26964
  2477
berghofe@26964
  2478
      T1 => ... => Tn => U => bool
berghofe@26964
  2479
berghofe@26964
  2480
    rather than
berghofe@26964
  2481
berghofe@26964
  2482
      T1 => ... => Tn => U set
berghofe@26964
  2483
wenzelm@26874
  2484
* Merged theories Wellfounded_Recursion, Accessible_Part and
wenzelm@27067
  2485
Wellfounded_Relations to theory Wellfounded.
krauss@26748
  2486
haftmann@26513
  2487
* Explicit class "eq" for executable equality.  INCOMPATIBILITY.
haftmann@26513
  2488
wenzelm@26874
  2489
* Class finite no longer treats UNIV as class parameter.  Use class
wenzelm@26874
  2490
enum from theory Library/Enum instead to achieve a similar effect.
haftmann@26445
  2491
INCOMPATIBILITY.
haftmann@26445
  2492
wenzelm@26874
  2493
* Theory List: rule list_induct2 now has explicitly named cases "Nil"
wenzelm@26874
  2494
and "Cons".  INCOMPATIBILITY.
wenzelm@26874
  2495
wenzelm@26422
  2496
* HOL (and FOL): renamed variables in rules imp_elim and swap.
wenzelm@26422
  2497
Potential INCOMPATIBILITY.
wenzelm@26422
  2498
wenzelm@26874
  2499
* Theory Product_Type: duplicated lemmas split_Pair_apply and
wenzelm@26874
  2500
injective_fst_snd removed, use split_eta and prod_eqI instead.
wenzelm@26874
  2501
Renamed upd_fst to apfst and upd_snd to apsnd.  INCOMPATIBILITY.
haftmann@26355
  2502
wenzelm@26335
  2503
* Theory Nat: removed redundant lemmas that merely duplicate lemmas of
wenzelm@26335
  2504
the same name in theory Orderings:
wenzelm@26335
  2505
wenzelm@26335
  2506
  less_trans
wenzelm@26335
  2507
  less_linear
wenzelm@26335
  2508
  le_imp_less_or_eq
wenzelm@26335
  2509
  le_less_trans
wenzelm@26335
  2510
  less_le_trans
wenzelm@26335
  2511
  less_not_sym
wenzelm@26335
  2512
  less_asym
wenzelm@26335
  2513
wenzelm@26335
  2514
Renamed less_imp_le to less_imp_le_nat, and less_irrefl to
wenzelm@26335
  2515
less_irrefl_nat.  Potential INCOMPATIBILITY due to more general types
wenzelm@26335
  2516
and different variable names.
wenzelm@26315
  2517
haftmann@26231
  2518
* Library/Option_ord.thy: Canonical order on option type.
haftmann@26231
  2519
wenzelm@27008
  2520
* Library/RBT.thy: Red-black trees, an efficient implementation of
wenzelm@27008
  2521
finite maps.
krauss@26197
  2522
haftmann@26231
  2523
* Library/Countable.thy: Type class for countable types.
haftmann@26231
  2524
wenzelm@26180
  2525
* Theory Int: The representation of numerals has changed.  The infix
wenzelm@26180
  2526
operator BIT and the bit datatype with constructors B0 and B1 have
wenzelm@26180
  2527
disappeared.  INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in
wenzelm@26180
  2528
place of "x BIT bit.B0" and "y BIT bit.B1", respectively.  Theorems
wenzelm@26180
  2529
involving BIT, B0, or B1 have been renamed with "Bit0" or "Bit1"
wenzelm@26180
  2530
accordingly.
wenzelm@26180
  2531
wenzelm@26180
  2532
* Theory Nat: definition of <= and < on natural numbers no longer
wenzelm@26180
  2533
depend on well-founded relations.  INCOMPATIBILITY.  Definitions
wenzelm@26180
  2534
le_def and less_def have disappeared.  Consider lemmas not_less
wenzelm@26180
  2535
[symmetric, where ?'a = nat] and less_eq [symmetric] instead.
wenzelm@26180
  2536
wenzelm@26180
  2537
* Theory Finite_Set: locales ACf, ACe, ACIf, ACIfSL and ACIfSLlin
wenzelm@26180
  2538
(whose purpose mainly is for various fold_set functionals) have been
wenzelm@26874
  2539
abandoned in favor of the existing algebraic classes
wenzelm@26180
  2540
ab_semigroup_mult, comm_monoid_mult, ab_semigroup_idem_mult,
wenzelm@26180
  2541
lower_semilattice (resp. upper_semilattice) and linorder.
haftmann@26139
  2542
INCOMPATIBILITY.
haftmann@26041
  2543
wenzelm@26180
  2544
* Theory Transitive_Closure: induct and cases rules now declare proper
wenzelm@26180
  2545
case_names ("base" and "step").  INCOMPATIBILITY.
wenzelm@26180
  2546
wenzelm@26180
  2547
* Theorem Inductive.lfp_ordinal_induct generalized to complete
wenzelm@26180
  2548
lattices.  The form set-specific version is available as
wenzelm@26180
  2549
Inductive.lfp_ordinal_induct_set.
haftmann@26013
  2550
wenzelm@26874
  2551
* Renamed theorems "power.simps" to "power_int.simps".
wenzelm@27067
  2552
INCOMPATIBILITY.
haftmann@25961
  2553
wenzelm@26180
  2554
* Class semiring_div provides basic abstract properties of semirings
haftmann@25942
  2555
with division and modulo operations.  Subsumes former class dvd_mod.
haftmann@25942
  2556
wenzelm@26180
  2557
* Merged theories IntDef, Numeral and IntArith into unified theory
wenzelm@26180
  2558
Int.  INCOMPATIBILITY.
wenzelm@26180
  2559
wenzelm@26180
  2560
* Theory Library/Code_Index: type "index" now represents natural
wenzelm@26180
  2561
numbers rather than integers.  INCOMPATIBILITY.
wenzelm@26180
  2562
wenzelm@26180
  2563
* New class "uminus" with operation "uminus" (split of from class
wenzelm@26180
  2564
"minus" which now only has operation "minus", binary).
haftmann@25919
  2565
INCOMPATIBILITY.
haftmann@25919
  2566
wenzelm@25522
  2567
* Constants "card", "internal_split", "option_map" now with authentic
haftmann@25919
  2568
syntax.  INCOMPATIBILITY.
wenzelm@25522
  2569
wenzelm@25522
  2570
* Definitions subset_def, psubset_def, set_diff_def, Compl_def,
wenzelm@25522
  2571
le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def,
wenzelm@25522
  2572
sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def,
wenzelm@25522
  2573
Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def,
wenzelm@25522
  2574
Sup_set_def, le_def, less_def, option_map_def now with object
haftmann@25919
  2575
equality.  INCOMPATIBILITY.
wenzelm@25464
  2576
schirmer@25705
  2577
* Records. Removed K_record, and replaced it by pure lambda term
wenzelm@25726
  2578
%x. c. The simplifier setup is now more robust against eta expansion.
schirmer@25705
  2579
INCOMPATIBILITY: in cases explicitly referring to K_record.
wenzelm@25464
  2580
wenzelm@27067
  2581
* Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}.
wenzelm@27067
  2582
wenzelm@27067
  2583
* Library/ListVector: new theory of arithmetic vector operations.
wenzelm@27067
  2584
wenzelm@27067
  2585
* Library/Order_Relation: new theory of various orderings as sets of
wenzelm@27067
  2586
pairs.  Defines preorders, partial orders, linear orders and
wenzelm@27067
  2587
well-orders on sets and on types.
krauss@26877
  2588
wenzelm@25726
  2589
krauss@26197
  2590
*** ZF ***
krauss@26197
  2591
wenzelm@26874
  2592
* Renamed some theories to allow to loading both ZF and HOL in the
wenzelm@26874
  2593
same session:
wenzelm@26874
  2594
wenzelm@26874
  2595
  Datatype  -> Datatype_ZF
wenzelm@26874
  2596
  Inductive -> Inductive_ZF
wenzelm@26874
  2597
  Int       -> Int_ZF
wenzelm@26874
  2598
  IntDiv    -> IntDiv_ZF
wenzelm@26874
  2599
  Nat       -> Nat_ZF
wenzelm@26874
  2600
  List      -> List_ZF
wenzelm@26874
  2601
  Main      -> Main_ZF
wenzelm@26874
  2602
wenzelm@26874
  2603
INCOMPATIBILITY: ZF theories that import individual theories below
wenzelm@26874
  2604
Main might need to be adapted.  Regular theory Main is still
wenzelm@26874
  2605
available, as trivial extension of Main_ZF.
krauss@26197
  2606
krauss@26197
  2607
wenzelm@25737
  2608
*** ML ***
wenzelm@25737
  2609
wenzelm@27067
  2610
* ML within Isar: antiquotation @{const name} or @{const
wenzelm@27067
  2611
name(typargs)} produces statically-checked Const term.
wenzelm@27067
  2612
wenzelm@26401
  2613
* Functor NamedThmsFun: data is available to the user as dynamic fact
wenzelm@26724
  2614
(of the same name).  Removed obsolete print command.
wenzelm@26401
  2615
wenzelm@27067
  2616
* Removed obsolete "use_legacy_bindings" function.
wenzelm@26188
  2617
wenzelm@25737
  2618
* The ``print mode'' is now a thread-local value derived from a global
wenzelm@25737
  2619
template (the former print_mode reference), thus access becomes
wenzelm@25737
  2620
non-critical.  The global print_mode reference is for session
wenzelm@25737
  2621
management only; user-code should use print_mode_value,
wenzelm@25737
  2622
print_mode_active, PrintMode.setmp etc.  INCOMPATIBILITY.
wenzelm@25737
  2623
wenzelm@26874
  2624
* Functions system/system_out provide a robust way to invoke external
wenzelm@29161
  2625
shell commands, with propagation of interrupts (requires Poly/ML
wenzelm@29161
  2626
5.2.1).  Do not use OS.Process.system etc. from the basis library!
wenzelm@26222
  2627
wenzelm@25737
  2628
wenzelm@25626
  2629
*** System ***
wenzelm@25626
  2630
wenzelm@25971
  2631
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs ---
wenzelm@25971
  2632
in accordance with Proof General 3.7, which prefers GNU emacs.
wenzelm@25970
  2633
wenzelm@25626
  2634
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm@25626
  2635
optional line editor may be specified via ISABELLE_LINE_EDITOR