NEWS
author hoelzl
Mon Aug 23 19:35:57 2010 +0200 (2010-08-23)
changeset 38656 d5d342611edb
parent 38642 8fa437809c67
child 38708 8915e3ce8655
permissions -rw-r--r--
Rewrite the Probability theory.

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