NEWS
author krauss
Tue Sep 28 09:54:07 2010 +0200 (2010-09-28)
changeset 39754 150f831ce4a3
parent 39689 78b185bf7660
child 39771 553f9b9aed28
permissions -rw-r--r--
no longer declare .psimps rules as [simp].

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