NEWS
author kleing
Mon Aug 20 04:34:31 2007 +0200 (2007-08-20)
changeset 24333 e77ea0ea7f2c
parent 24238 ae70f95e31de
child 24342 a1d489e254ec
permissions -rw-r--r--
* HOL-Word:
New extensive library and type for generic, fixed size machine
words, with arithemtic, bit-wise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.

* still to do: README.html/document + moving some of the generic lemmas
to appropriate place in distribution
wenzelm@5363
     1
Isabelle NEWS -- history user-relevant changes
wenzelm@5363
     2
==============================================
wenzelm@2553
     3
wenzelm@20807
     4
New in this Isabelle version
wenzelm@17754
     5
----------------------------
wenzelm@17754
     6
wenzelm@17754
     7
*** General ***
wenzelm@17754
     8
wenzelm@22826
     9
* More uniform information about legacy features, notably a
wenzelm@22826
    10
warning/error of "Legacy feature: ...", depending on the state of the
wenzelm@23367
    11
tolerate_legacy_features flag (default true). FUTURE INCOMPATIBILITY:
wenzelm@23367
    12
legacy features will disappear eventually.
wenzelm@22826
    13
wenzelm@17918
    14
* Theory syntax: the header format ``theory A = B + C:'' has been
wenzelm@17918
    15
discontinued in favour of ``theory A imports B C begin''.  Use isatool
wenzelm@17918
    16
fixheaders to convert existing theory files.  INCOMPATIBILITY.
wenzelm@17918
    17
wenzelm@17918
    18
* Theory syntax: the old non-Isar theory file format has been
wenzelm@17918
    19
discontinued altogether.  Note that ML proof scripts may still be used
wenzelm@17918
    20
with Isar theories; migration is usually quite simple with the ML
wenzelm@17918
    21
function use_legacy_bindings.  INCOMPATIBILITY.
wenzelm@17918
    22
wenzelm@22871
    23
* Theory syntax: some popular names (e.g. 'class', 'declaration',
wenzelm@22871
    24
'fun', 'help', 'if') are now keywords.  INCOMPATIBILITY, use double
wenzelm@22871
    25
quotes.
wenzelm@19814
    26
wenzelm@23888
    27
* Theory loader: be more serious about observing the static theory
wenzelm@23888
    28
header specifications (including optional directories), but not the
wenzelm@24172
    29
accidental file locations of previously successful loads.  The strict
wenzelm@24172
    30
update policy of former update_thy is now already performed by
wenzelm@24172
    31
use_thy, so the former has been removed; use_thys updates several
wenzelm@24172
    32
theories simultaneously, just as 'imports' within a theory header
wenzelm@24172
    33
specification, but without merging the results.  Potential
wenzelm@24172
    34
INCOMPATIBILITY: may need to refine theory headers and commands
wenzelm@24172
    35
ROOT.ML which depend on load order.
wenzelm@23888
    36
wenzelm@23888
    37
* Theory loader: optional support for content-based file
wenzelm@23888
    38
identification, instead of the traditional scheme of full physical
wenzelm@23889
    39
path plus date stamp; configured by the ISABELLE_FILE_IDENT setting
wenzelm@23888
    40
(cf. the system manual).  The new scheme allows to work with
wenzelm@23888
    41
non-finished theories in persistent session images, such that source
wenzelm@23888
    42
files may be moved later on without requiring reloads.
wenzelm@23888
    43
wenzelm@24187
    44
* Theory loader: old-style ML proof scripts being *attached* to a thy
wenzelm@24187
    45
file (with the same base name as the theory) are considered a legacy
wenzelm@24187
    46
feature, which will disappear eventually. Even now, the theory loader no
wenzelm@24187
    47
longer maintains dependencies on such files.
wenzelm@24187
    48
wenzelm@24234
    49
* Syntax: the scope for resolving ambiguities via type-inference is now
wenzelm@24234
    50
limited to individual terms, instead of whole simultaneous
wenzelm@24234
    51
specifications as before. This greatly reduces the complexity of the
wenzelm@24234
    52
syntax module and improves flexibility by separating parsing and
wenzelm@24234
    53
type-checking. INCOMPATIBILITY: additional type-constraints (explicit
wenzelm@24234
    54
'fixes' etc.) are required in rare situations.
wenzelm@24234
    55
wenzelm@17981
    56
* Legacy goal package: reduced interface to the bare minimum required
wenzelm@17981
    57
to keep existing proof scripts running.  Most other user-level
wenzelm@17981
    58
functions are now part of the OldGoals structure, which is *not* open
wenzelm@17981
    59
by default (consider isatool expandshort before open OldGoals).
wenzelm@17981
    60
Removed top_sg, prin, printyp, pprint_term/typ altogether, because
wenzelm@17981
    61
these tend to cause confusion about the actual goal (!) context being
wenzelm@17981
    62
used here, which is not necessarily the same as the_context().
wenzelm@17918
    63
wenzelm@23379
    64
* Command 'find_theorems': supports "*" wild-card in "name:"
wenzelm@23379
    65
criterion; "with_dups" option.  Certain ProofGeneral versions might
wenzelm@23379
    66
support a specific search form (see ProofGeneral/CHANGES).
webertj@22965
    67
wenzelm@20370
    68
* The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1
wenzelm@20370
    69
by default, which means that "prems" (and also "fixed variables") are
wenzelm@20370
    70
suppressed from proof state output.  Note that the ProofGeneral
wenzelm@20370
    71
settings mechanism allows to change and save options persistently, but
wenzelm@20370
    72
older versions of Isabelle will fail to start up if a negative prems
wenzelm@20370
    73
limit is imposed.
wenzelm@20370
    74
wenzelm@21308
    75
* Local theory targets may be specified by non-nested blocks of
wenzelm@21308
    76
``context/locale/class ... begin'' followed by ``end''.  The body may
wenzelm@21308
    77
contain definitions, theorems etc., including any derived mechanism
wenzelm@21308
    78
that has been implemented on top of these primitives.  This concept
wenzelm@21308
    79
generalizes the existing ``theorem (in ...)'' towards more versatility
wenzelm@21308
    80
and scalability.
wenzelm@21308
    81
wenzelm@21960
    82
* Proof General interface: proper undo of final 'end' command;
wenzelm@21960
    83
discontinued Isabelle/classic mode (ML proof scripts).
wenzelm@21960
    84
wenzelm@17754
    85
wenzelm@17865
    86
*** Document preparation ***
wenzelm@17865
    87
wenzelm@21717
    88
* Added antiquotation @{theory name} which prints the given name,
wenzelm@21717
    89
after checking that it refers to a valid ancestor theory in the
wenzelm@21717
    90
current context.
haftmann@21339
    91
wenzelm@17869
    92
* Added antiquotations @{ML_type text} and @{ML_struct text} which
wenzelm@17869
    93
check the given source text as ML type/structure, printing verbatim.
wenzelm@17865
    94
wenzelm@21717
    95
* Added antiquotation @{abbrev "c args"} which prints the abbreviation
wenzelm@21717
    96
"c args == rhs" given in the current context.  (Any number of
wenzelm@21735
    97
arguments may be given on the LHS.)
wenzelm@21717
    98
wenzelm@21717
    99
wenzelm@17865
   100
wenzelm@17779
   101
*** Pure ***
wenzelm@17779
   102
haftmann@22921
   103
* code generator: consts in 'consts_code' Isar commands are now referred
haftmann@22921
   104
  to by usual term syntax (including optional type annotations).
haftmann@22921
   105
haftmann@22735
   106
* code generator: 
haftmann@22921
   107
  - Isar 'definition's, 'constdef's and primitive instance definitions are added
haftmann@22921
   108
    explicitly to the table of defining equations
haftmann@22754
   109
  - primitive definitions are not used as defining equations by default any longer
haftmann@22735
   110
  - defining equations are now definitly restricted to meta "==" and object
haftmann@22735
   111
        equality "="
haftmann@22735
   112
  - HOL theories have been adopted accordingly
haftmann@22735
   113
wenzelm@20807
   114
* class_package.ML offers a combination of axclasses and locales to
haftmann@22921
   115
achieve Haskell-like type classes in Isabelle.  See
wenzelm@20807
   116
HOL/ex/Classpackage.thy for examples.
wenzelm@20807
   117
wenzelm@20807
   118
* Yet another code generator framework allows to generate executable
haftmann@22921
   119
code for ML and Haskell (including "class"es).  A short usage sketch:
haftmann@20188
   120
haftmann@20188
   121
    internal compilation:
haftmann@23850
   122
        code_gen <list of constants (term syntax)> in SML
haftmann@20453
   123
    writing SML code to a file:
haftmann@23850
   124
        code_gen <list of constants (term syntax)> in SML <filename>
haftmann@22735
   125
    writing OCaml code to a file:
haftmann@23850
   126
        code_gen <list of constants (term syntax)> in OCaml <filename>
haftmann@20188
   127
    writing Haskell code to a bunch of files:
haftmann@23850
   128
        code_gen <list of constants (term syntax)> in Haskell <filename>
haftmann@20453
   129
haftmann@20453
   130
Reasonable default setup of framework in HOL/Main.
haftmann@20453
   131
haftmann@20453
   132
Theorem attributs for selecting and transforming function equations theorems:
haftmann@20453
   133
haftmann@22845
   134
    [code fun]:        select a theorem as function equation for a specific constant
haftmann@22845
   135
    [code fun del]:    deselect a theorem as function equation for a specific constant
haftmann@22845
   136
    [code inline]:     select an equation theorem for unfolding (inlining) in place
haftmann@22845
   137
    [code inline del]: deselect an equation theorem for unfolding (inlining) in place
haftmann@20453
   138
haftmann@22735
   139
User-defined serializations (target in {SML, OCaml, Haskell}):
haftmann@20453
   140
haftmann@20453
   141
    code_const <and-list of constants (term syntax)>
haftmann@20453
   142
      {(target) <and-list of const target syntax>}+
haftmann@20453
   143
haftmann@20453
   144
    code_type <and-list of type constructors>
haftmann@20453
   145
      {(target) <and-list of type target syntax>}+
haftmann@20453
   146
haftmann@20453
   147
    code_instance <and-list of instances>
haftmann@20453
   148
      {(target)}+
haftmann@20453
   149
        where instance ::= <type constructor> :: <class>
haftmann@20453
   150
haftmann@20453
   151
    code_class <and_list of classes>
haftmann@20453
   152
      {(target) <and-list of class target syntax>}+
haftmann@20453
   153
        where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}?
haftmann@20453
   154
haftmann@22735
   155
code_instance and code_class only apply to target Haskell.
haftmann@22735
   156
haftmann@22735
   157
See HOL theories and HOL/ex/Codegenerator*.thy for usage examples.
haftmann@22735
   158
Doc/Isar/Advanced/Codegen/ provides a tutorial.
haftmann@20188
   159
wenzelm@19254
   160
* Command 'no_translations' removes translation rules from theory
wenzelm@19254
   161
syntax.
wenzelm@19254
   162
wenzelm@19625
   163
* Overloaded definitions are now actually checked for acyclic
wenzelm@19714
   164
dependencies.  The overloading scheme is slightly more general than
wenzelm@19714
   165
that of Haskell98, although Isabelle does not demand an exact
wenzelm@19714
   166
correspondence to type class and instance declarations.
wenzelm@19714
   167
INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more
wenzelm@19714
   168
exotic versions of overloading -- at the discretion of the user!
wenzelm@19711
   169
wenzelm@19711
   170
Polymorphic constants are represented via type arguments, i.e. the
wenzelm@19711
   171
instantiation that matches an instance against the most general
wenzelm@19711
   172
declaration given in the signature.  For example, with the declaration
wenzelm@19711
   173
c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented
wenzelm@19711
   174
as c(nat).  Overloading is essentially simultaneous structural
wenzelm@19711
   175
recursion over such type arguments.  Incomplete specification patterns
wenzelm@19714
   176
impose global constraints on all occurrences, e.g. c('a * 'a) on the
wenzelm@19715
   177
LHS means that more general c('a * 'b) will be disallowed on any RHS.
wenzelm@19714
   178
Command 'print_theory' outputs the normalized system of recursive
wenzelm@19714
   179
equations, see section "definitions".
wenzelm@19625
   180
wenzelm@24086
   181
* Configuration options are maintained within the theory or proof
wenzelm@24086
   182
context (with name and type bool/int/string), providing a very simple
wenzelm@24086
   183
interface to a poor-man's version of general context data.  Tools may
wenzelm@24110
   184
declare options in ML (e.g. using Attrib.config_int) and then refer to
wenzelm@24110
   185
these values using Config.get etc.  Users may change options via an
wenzelm@24110
   186
associated attribute of the same name.  This form of context
wenzelm@24110
   187
declaration works particularly well with commands 'declare' or
wenzelm@24110
   188
'using', for example ``declare [[foo = 42]]''.  Thus it has become
wenzelm@24110
   189
very easy to avoid global references, which would not observe Isar
wenzelm@24110
   190
toplevel undo/redo and fail to work with multithreading.
wenzelm@24086
   191
wenzelm@24172
   192
Various global ML references of Pure and HOL have been turned into
wenzelm@24172
   193
configuration options:
wenzelm@24172
   194
wenzelm@24172
   195
  Unify.search_bound		unify_search_bound
wenzelm@24172
   196
  Unify.trace_bound		unify_trace_bound
wenzelm@24172
   197
  Unify.trace_simp		unify_trace_simp
wenzelm@24172
   198
  Unify.trace_types		unify_trace_types
wenzelm@24172
   199
  Simplifier.simp_depth_limit	simp_depth_limit
wenzelm@24172
   200
  Blast.depth_limit		blast_depth_limit
wenzelm@24172
   201
  DatatypeProp.dtK		datatype_distinctness_limit
wenzelm@24172
   202
  fast_arith_neq_limit  	fast_arith_neq_limit
wenzelm@24172
   203
  fast_arith_split_limit	fast_arith_split_limit
wenzelm@24172
   204
wenzelm@24086
   205
* Named collections of theorems may be easily installed as context
wenzelm@24086
   206
data using the functor NamedThmsFun (see
wenzelm@24086
   207
src/Pure/Tools/named_thms.ML).  The user may add or delete facts via
wenzelm@24110
   208
attributes; there is also a toplevel print command.  This facility is
wenzelm@24110
   209
just a common case of general context data, which is the preferred way
wenzelm@24110
   210
for anything more complex than just a list of facts in canonical
wenzelm@24110
   211
order.
wenzelm@24086
   212
wenzelm@24032
   213
* Isar: command 'declaration' augments a local theory by generic
wenzelm@24032
   214
declaration functions written in ML.  This enables arbitrary content
wenzelm@24032
   215
being added to the context, depending on a morphism that tells the
wenzelm@24032
   216
difference of the original declaration context wrt. the application
wenzelm@24032
   217
context encountered later on.
wenzelm@24032
   218
wenzelm@24032
   219
* Isar: proper interfaces for simplification procedures.  Command
wenzelm@24032
   220
'simproc_setup' declares named simprocs (with match patterns, and body
wenzelm@24032
   221
text in ML).  Attribute "simproc" adds/deletes simprocs in the current
wenzelm@24032
   222
context.  ML antiquotation @{simproc name} retrieves named simprocs.
wenzelm@24032
   223
wenzelm@24032
   224
* Isar: an extra pair of brackets around attribute declarations
wenzelm@24032
   225
abbreviates a theorem reference involving an internal dummy fact,
wenzelm@24032
   226
which will be ignored later --- only the effect of the attribute on
wenzelm@24032
   227
the background context will persist.  This form of in-place
wenzelm@24032
   228
declarations is particularly useful with commands like 'declare' and
wenzelm@24032
   229
'using', for example ``have A using [[simproc a]] by simp''.
wenzelm@24032
   230
wenzelm@23369
   231
* Isar: method "assumption" (and implicit closing of subproofs) now
wenzelm@23369
   232
takes simple non-atomic goal assumptions into account: after applying
wenzelm@23369
   233
an assumption as a rule the resulting subgoals are solved by atomic
wenzelm@23369
   234
assumption steps.  This is particularly useful to finish 'obtain'
wenzelm@23369
   235
goals, such as "!!x. (!!x. P x ==> thesis) ==> P x ==> thesis",
wenzelm@23369
   236
without referring to the original premise "!!x. P x ==> thesis" in the
wenzelm@23369
   237
Isar proof context.  POTENTIAL INCOMPATIBILITY: method "assumption" is
wenzelm@23369
   238
more permissive.
wenzelm@23369
   239
wenzelm@23369
   240
* Isar: implicit use of prems from the Isar proof context is
wenzelm@23369
   241
considered a legacy feature.  Common applications like ``have A .''
wenzelm@23369
   242
may be replaced by ``have A by fact'' or ``note `A`''.  In general,
wenzelm@23369
   243
referencing facts explicitly here improves readability and
wenzelm@23369
   244
maintainability of proof texts.
wenzelm@23369
   245
wenzelm@17865
   246
* Isar: improper proof element 'guess' is like 'obtain', but derives
wenzelm@17865
   247
the obtained context from the course of reasoning!  For example:
wenzelm@17865
   248
wenzelm@17865
   249
  assume "EX x y. A x & B y"   -- "any previous fact"
wenzelm@17865
   250
  then guess x and y by clarify
wenzelm@17865
   251
wenzelm@17865
   252
This technique is potentially adventurous, depending on the facts and
wenzelm@17865
   253
proof tools being involved here.
wenzelm@17865
   254
wenzelm@18020
   255
* Isar: known facts from the proof context may be specified as literal
wenzelm@18020
   256
propositions, using ASCII back-quote syntax.  This works wherever
wenzelm@18020
   257
named facts used to be allowed so far, in proof commands, proof
wenzelm@18020
   258
methods, attributes etc.  Literal facts are retrieved from the context
wenzelm@18020
   259
according to unification of type and term parameters.  For example,
wenzelm@18020
   260
provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known
wenzelm@18020
   261
theorems in the current context, then these are valid literal facts:
wenzelm@18020
   262
`A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc.
wenzelm@18020
   263
wenzelm@18020
   264
There is also a proof method "fact" which does the same composition
wenzelm@18044
   265
for explicit goal states, e.g. the following proof texts coincide with
wenzelm@18044
   266
certain special cases of literal facts:
wenzelm@18020
   267
wenzelm@18020
   268
  have "A" by fact                 ==  note `A`
wenzelm@18020
   269
  have "A ==> B" by fact           ==  note `A ==> B`
wenzelm@18020
   270
  have "!!x. P x ==> Q x" by fact  ==  note `!!x. P x ==> Q x`
wenzelm@18020
   271
  have "P a ==> Q a" by fact       ==  note `P a ==> Q a`
wenzelm@18020
   272
wenzelm@20118
   273
* Isar: ":" (colon) is no longer a symbolic identifier character in
wenzelm@20118
   274
outer syntax.  Thus symbolic identifiers may be used without
wenzelm@20118
   275
additional white space in declarations like this: ``assume *: A''.
wenzelm@20118
   276
wenzelm@20013
   277
* Isar: 'print_facts' prints all local facts of the current context,
wenzelm@20013
   278
both named and unnamed ones.
wenzelm@20013
   279
wenzelm@18308
   280
* Isar: 'def' now admits simultaneous definitions, e.g.:
wenzelm@18308
   281
wenzelm@18308
   282
  def x == "t" and y == "u"
wenzelm@18308
   283
wenzelm@18540
   284
* Isar: added command 'unfolding', which is structurally similar to
wenzelm@18540
   285
'using', but affects both the goal state and facts by unfolding given
wenzelm@18815
   286
rewrite rules.  Thus many occurrences of the 'unfold' method or
wenzelm@18540
   287
'unfolded' attribute may be replaced by first-class proof text.
wenzelm@18540
   288
wenzelm@18815
   289
* Isar: methods 'unfold' / 'fold', attributes 'unfolded' / 'folded',
wenzelm@18815
   290
and command 'unfolding' now all support object-level equalities
wenzelm@18815
   291
(potentially conditional).  The underlying notion of rewrite rule is
wenzelm@18815
   292
analogous to the 'rule_format' attribute, but *not* that of the
wenzelm@18815
   293
Simplifier (which is usually more generous).
wenzelm@18815
   294
kleing@24238
   295
* Isar: the new attribute [rotated n] (default n = 1) rotates the
kleing@24238
   296
premises of a theorem by n. Useful in conjunction with drule.
kleing@24238
   297
wenzelm@19220
   298
* Isar: the goal restriction operator [N] (default N = 1) evaluates a
wenzelm@19220
   299
method expression within a sandbox consisting of the first N
wenzelm@19240
   300
sub-goals, which need to exist.  For example, ``simp_all [3]''
wenzelm@19240
   301
simplifies the first three sub-goals, while (rule foo, simp_all)[]
wenzelm@19240
   302
simplifies all new goals that emerge from applying rule foo to the
wenzelm@19240
   303
originally first one.
wenzelm@19220
   304
wenzelm@19814
   305
* Isar: schematic goals are no longer restricted to higher-order
wenzelm@19814
   306
patterns; e.g. ``lemma "?P(?x)" by (rule TrueI)'' now works as
wenzelm@19814
   307
expected.
wenzelm@19814
   308
wenzelm@18901
   309
* Isar: the conclusion of a long theorem statement is now either
wenzelm@18901
   310
'shows' (a simultaneous conjunction, as before), or 'obtains'
wenzelm@18901
   311
(essentially a disjunction of cases with local parameters and
wenzelm@18901
   312
assumptions).  The latter allows to express general elimination rules
wenzelm@18910
   313
adequately; in this notation common elimination rules look like this:
wenzelm@18901
   314
wenzelm@18901
   315
  lemma exE:    -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis"
wenzelm@18901
   316
    assumes "EX x. P x"
wenzelm@18901
   317
    obtains x where "P x"
wenzelm@18901
   318
wenzelm@18901
   319
  lemma conjE:  -- "A & B ==> (A ==> B ==> thesis) ==> thesis"
wenzelm@18901
   320
    assumes "A & B"
wenzelm@18901
   321
    obtains A and B
wenzelm@18901
   322
wenzelm@18901
   323
  lemma disjE:  -- "A | B ==> (A ==> thesis) ==> (B ==> thesis) ==> thesis"
wenzelm@18901
   324
    assumes "A | B"
wenzelm@18901
   325
    obtains
wenzelm@18901
   326
      A
wenzelm@18901
   327
    | B
wenzelm@18901
   328
wenzelm@18910
   329
The subsequent classical rules even refer to the formal "thesis"
wenzelm@18901
   330
explicitly:
wenzelm@18901
   331
wenzelm@18901
   332
  lemma classical:     -- "(~ thesis ==> thesis) ==> thesis"
wenzelm@18901
   333
    obtains "~ thesis"
wenzelm@18901
   334
wenzelm@18910
   335
  lemma Peirce's_Law:  -- "((thesis ==> something) ==> thesis) ==> thesis"
wenzelm@18910
   336
    obtains "thesis ==> something"
wenzelm@18901
   337
wenzelm@18901
   338
The actual proof of an 'obtains' statement is analogous to that of the
wenzelm@18910
   339
Isar proof element 'obtain', only that there may be several cases.
wenzelm@18910
   340
Optional case names may be specified in parentheses; these will be
wenzelm@18910
   341
available both in the present proof and as annotations in the
wenzelm@18910
   342
resulting rule, for later use with the 'cases' method (cf. attribute
wenzelm@18910
   343
case_names).
wenzelm@18901
   344
wenzelm@21447
   345
* Isar: the assumptions of a long theorem statement are available as
wenzelm@21447
   346
"assms" fact in the proof context.  This is more appropriate than the
wenzelm@21447
   347
(historical) "prems", which refers to all assumptions of the current
wenzelm@21447
   348
context, including those from the target locale, proof body etc.
wenzelm@21447
   349
wenzelm@19263
   350
* Isar: 'print_statement' prints theorems from the current theory or
wenzelm@19263
   351
proof context in long statement form, according to the syntax of a
wenzelm@19263
   352
top-level lemma.
wenzelm@19263
   353
wenzelm@18901
   354
* Isar: 'obtain' takes an optional case name for the local context
wenzelm@18901
   355
introduction rule (default "that").
wenzelm@18901
   356
wenzelm@19587
   357
* Isar: removed obsolete 'concl is' patterns.  INCOMPATIBILITY, use
wenzelm@19587
   358
explicit (is "_ ==> ?foo") in the rare cases where this still happens
wenzelm@19587
   359
to occur.
wenzelm@19587
   360
wenzelm@19682
   361
* Pure: syntax "CONST name" produces a fully internalized constant
wenzelm@19682
   362
according to the current context.  This is particularly useful for
wenzelm@19682
   363
syntax translations that should refer to internal constant
wenzelm@19682
   364
representations independently of name spaces.
wenzelm@19682
   365
wenzelm@21537
   366
* Pure: syntax constant for foo (binder "FOO ") is called "foo_binder"
wenzelm@21537
   367
instead of "FOO ". This allows multiple binder declarations to coexist
wenzelm@21537
   368
in the same context.  INCOMPATIBILITY.
wenzelm@21537
   369
wenzelm@21209
   370
* Isar/locales: 'notation' provides a robust interface to the 'syntax'
wenzelm@21209
   371
primitive that also works in a locale context (both for constants and
wenzelm@21209
   372
fixed variables).  Type declaration and internal syntactic
wenzelm@21209
   373
representation of given constants retrieved from the context.
wenzelm@19682
   374
wenzelm@19665
   375
* Isar/locales: new derived specification elements 'axiomatization',
wenzelm@19665
   376
'definition', 'abbreviation', which support type-inference, admit
wenzelm@19083
   377
object-level specifications (equality, equivalence).  See also the
wenzelm@19083
   378
isar-ref manual.  Examples:
wenzelm@19081
   379
wenzelm@19665
   380
  axiomatization
wenzelm@21595
   381
    eq  (infix "===" 50) where
wenzelm@21595
   382
    eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
wenzelm@21595
   383
wenzelm@21595
   384
  definition "f x y = x + y + 1"
wenzelm@21595
   385
  definition g where "g x = f x x"
wenzelm@19081
   386
wenzelm@19363
   387
  abbreviation
wenzelm@21595
   388
    neq  (infix "=!=" 50) where
wenzelm@19363
   389
    "x =!= y == ~ (x === y)"
wenzelm@19081
   390
wenzelm@19083
   391
These specifications may be also used in a locale context.  Then the
wenzelm@19083
   392
constants being introduced depend on certain fixed parameters, and the
wenzelm@19083
   393
constant name is qualified by the locale base name.  An internal
wenzelm@19083
   394
abbreviation takes care for convenient input and output, making the
wenzelm@19088
   395
parameters implicit and using the original short name.  See also
wenzelm@19083
   396
HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic
wenzelm@19083
   397
entities from a monomorphic theory.
wenzelm@19083
   398
wenzelm@19083
   399
Presently, abbreviations are only available 'in' a target locale, but
wenzelm@19363
   400
not inherited by general import expressions.  Also note that
wenzelm@19363
   401
'abbreviation' may be used as a type-safe replacement for 'syntax' +
wenzelm@19363
   402
'translations' in common applications.
wenzelm@19084
   403
wenzelm@19682
   404
Concrete syntax is attached to specified constants in internal form,
wenzelm@19682
   405
independently of name spaces.  The parse tree representation is
wenzelm@21209
   406
slightly different -- use 'notation' instead of raw 'syntax', and
wenzelm@19682
   407
'translations' with explicit "CONST" markup to accommodate this.
wenzelm@19665
   408
wenzelm@21735
   409
* Pure: command 'print_abbrevs' prints all constant abbreviations of
wenzelm@21735
   410
the current context.  Print mode "no_abbrevs" prevents inversion of
wenzelm@21735
   411
abbreviations on output.
wenzelm@21735
   412
ballarin@19783
   413
* Isar/locales: improved parameter handling:
ballarin@19783
   414
- use of locales "var" and "struct" no longer necessary;
ballarin@19783
   415
- parameter renamings are no longer required to be injective.
ballarin@19783
   416
  This enables, for example, to define a locale for endomorphisms thus:
ballarin@19783
   417
  locale endom = homom mult mult h.
ballarin@19783
   418
ballarin@19931
   419
* Isar/locales: changed the way locales with predicates are defined.
ballarin@19931
   420
Instead of accumulating the specification, the imported expression is
wenzelm@22126
   421
now an interpretation.  INCOMPATIBILITY: different normal form of
wenzelm@22126
   422
locale expressions.  In particular, in interpretations of locales with
wenzelm@22126
   423
predicates, goals repesenting already interpreted fragments are not
wenzelm@22126
   424
removed automatically.  Use methods `intro_locales' and
wenzelm@22126
   425
`unfold_locales'; see below.
wenzelm@22126
   426
wenzelm@22126
   427
* Isar/locales: new methods `intro_locales' and `unfold_locales'
wenzelm@22126
   428
provide backward reasoning on locales predicates.  The methods are
wenzelm@22126
   429
aware of interpretations and discharge corresponding goals.
wenzelm@22126
   430
`intro_locales' is less aggressive then `unfold_locales' and does not
wenzelm@22126
   431
unfold predicates to assumptions.
ballarin@19931
   432
ballarin@19931
   433
* Isar/locales: the order in which locale fragments are accumulated
wenzelm@22126
   434
has changed.  This enables to override declarations from fragments due
wenzelm@22126
   435
to interpretations -- for example, unwanted simp rules.
ballarin@19931
   436
ballarin@23920
   437
* Isar/locales: interpretation in theories and proof contexts has been
ballarin@23920
   438
extended.  One may now specify (and prove) equations, which are
ballarin@23920
   439
unfolded in interpreted theorems.  This is useful for replacing
ballarin@23920
   440
defined concepts (constants depending on locale parameters) by
ballarin@23920
   441
concepts already existing in the target context.  Example:
ballarin@23920
   442
ballarin@23920
   443
  interpretation partial_order ["op <= :: [int, int] => bool"]
ballarin@23920
   444
    where "partial_order.less (op <=) (x::int) y = (x < y)"
ballarin@23920
   445
ballarin@23977
   446
Typically, the constant `partial_order.less' is created by a definition
ballarin@23977
   447
specification element in the context of locale partial_order.
ballarin@23920
   448
wenzelm@18233
   449
* Provers/induct: improved internal context management to support
wenzelm@18233
   450
local fixes and defines on-the-fly.  Thus explicit meta-level
wenzelm@18233
   451
connectives !! and ==> are rarely required anymore in inductive goals
wenzelm@18233
   452
(using object-logic connectives for this purpose has been long
wenzelm@18233
   453
obsolete anyway).  The subsequent proof patterns illustrate advanced
wenzelm@18233
   454
techniques of natural induction; general datatypes and inductive sets
wenzelm@18267
   455
work analogously (see also src/HOL/Lambda for realistic examples).
wenzelm@18267
   456
wenzelm@18267
   457
(1) This is how to ``strengthen'' an inductive goal wrt. certain
wenzelm@18239
   458
parameters:
wenzelm@18233
   459
wenzelm@18233
   460
  lemma
wenzelm@18233
   461
    fixes n :: nat and x :: 'a
wenzelm@18233
   462
    assumes a: "A n x"
wenzelm@18233
   463
    shows "P n x"
wenzelm@18233
   464
    using a                     -- {* make induct insert fact a *}
wenzelm@20503
   465
  proof (induct n arbitrary: x) -- {* generalize goal to "!!x. A n x ==> P n x" *}
wenzelm@18248
   466
    case 0
wenzelm@18233
   467
    show ?case sorry
wenzelm@18233
   468
  next
wenzelm@18248
   469
    case (Suc n)
wenzelm@18239
   470
    note `!!x. A n x ==> P n x` -- {* induction hypothesis, according to induction rule *}
wenzelm@18239
   471
    note `A (Suc n) x`          -- {* induction premise, stemming from fact a *}
wenzelm@18233
   472
    show ?case sorry
wenzelm@18233
   473
  qed
wenzelm@18233
   474
wenzelm@18267
   475
(2) This is how to perform induction over ``expressions of a certain
wenzelm@18233
   476
form'', using a locally defined inductive parameter n == "a x"
wenzelm@18239
   477
together with strengthening (the latter is usually required to get
wenzelm@18267
   478
sufficiently flexible induction hypotheses):
wenzelm@18233
   479
wenzelm@18233
   480
  lemma
wenzelm@18233
   481
    fixes a :: "'a => nat"
wenzelm@18233
   482
    assumes a: "A (a x)"
wenzelm@18233
   483
    shows "P (a x)"
wenzelm@18233
   484
    using a
wenzelm@20503
   485
  proof (induct n == "a x" arbitrary: x)
wenzelm@18233
   486
    ...
wenzelm@18233
   487
wenzelm@18267
   488
See also HOL/Isar_examples/Puzzle.thy for an application of the this
wenzelm@18267
   489
particular technique.
wenzelm@18267
   490
wenzelm@18901
   491
(3) This is how to perform existential reasoning ('obtains' or
wenzelm@18901
   492
'obtain') by induction, while avoiding explicit object-logic
wenzelm@18901
   493
encodings:
wenzelm@18901
   494
wenzelm@18901
   495
  lemma
wenzelm@18901
   496
    fixes n :: nat
wenzelm@18901
   497
    obtains x :: 'a where "P n x" and "Q n x"
wenzelm@20503
   498
  proof (induct n arbitrary: thesis)
wenzelm@18267
   499
    case 0
wenzelm@18267
   500
    obtain x where "P 0 x" and "Q 0 x" sorry
wenzelm@18399
   501
    then show thesis by (rule 0)
wenzelm@18267
   502
  next
wenzelm@18267
   503
    case (Suc n)
wenzelm@18267
   504
    obtain x where "P n x" and "Q n x" by (rule Suc.hyps)
wenzelm@18267
   505
    obtain x where "P (Suc n) x" and "Q (Suc n) x" sorry
wenzelm@18267
   506
    then show thesis by (rule Suc.prems)
wenzelm@18267
   507
  qed
wenzelm@18267
   508
wenzelm@20503
   509
Here the 'arbitrary: thesis' specification essentially modifies the
wenzelm@20503
   510
scope of the formal thesis parameter, in order to the get the whole
wenzelm@18267
   511
existence statement through the induction as expected.
wenzelm@18233
   512
wenzelm@18506
   513
* Provers/induct: mutual induction rules are now specified as a list
wenzelm@18506
   514
of rule sharing the same induction cases.  HOL packages usually
wenzelm@18506
   515
provide foo_bar.inducts for mutually defined items foo and bar
wenzelm@18506
   516
(e.g. inductive sets or datatypes).  INCOMPATIBILITY, users need to
wenzelm@18506
   517
specify mutual induction rules differently, i.e. like this:
wenzelm@18506
   518
wenzelm@18506
   519
  (induct rule: foo_bar.inducts)
wenzelm@18506
   520
  (induct set: foo bar)
wenzelm@18506
   521
  (induct type: foo bar)
wenzelm@18506
   522
wenzelm@18506
   523
The ML function ProjectRule.projections turns old-style rules into the
wenzelm@18506
   524
new format.
wenzelm@18506
   525
wenzelm@18506
   526
* Provers/induct: improved handling of simultaneous goals.  Instead of
wenzelm@18506
   527
introducing object-level conjunction, the statement is now split into
wenzelm@18506
   528
several conclusions, while the corresponding symbolic cases are
wenzelm@18601
   529
nested accordingly.  INCOMPATIBILITY, proofs need to be structured
wenzelm@18601
   530
explicitly.  For example:
wenzelm@18480
   531
wenzelm@18480
   532
  lemma
wenzelm@18480
   533
    fixes n :: nat
wenzelm@18480
   534
    shows "P n" and "Q n"
wenzelm@18480
   535
  proof (induct n)
wenzelm@18601
   536
    case 0 case 1
wenzelm@18480
   537
    show "P 0" sorry
wenzelm@18480
   538
  next
wenzelm@18601
   539
    case 0 case 2
wenzelm@18480
   540
    show "Q 0" sorry
wenzelm@18480
   541
  next
wenzelm@18601
   542
    case (Suc n) case 1
wenzelm@18480
   543
    note `P n` and `Q n`
wenzelm@18480
   544
    show "P (Suc n)" sorry
wenzelm@18480
   545
  next
wenzelm@18601
   546
    case (Suc n) case 2
wenzelm@18480
   547
    note `P n` and `Q n`
wenzelm@18480
   548
    show "Q (Suc n)" sorry
wenzelm@18480
   549
  qed
wenzelm@18480
   550
wenzelm@18601
   551
The split into subcases may be deferred as follows -- this is
wenzelm@18601
   552
particularly relevant for goal statements with local premises.
wenzelm@18601
   553
wenzelm@18601
   554
  lemma
wenzelm@18601
   555
    fixes n :: nat
wenzelm@18601
   556
    shows "A n ==> P n" and "B n ==> Q n"
wenzelm@18601
   557
  proof (induct n)
wenzelm@18601
   558
    case 0
wenzelm@18601
   559
    {
wenzelm@18601
   560
      case 1
wenzelm@18601
   561
      note `A 0`
wenzelm@18601
   562
      show "P 0" sorry
wenzelm@18601
   563
    next
wenzelm@18601
   564
      case 2
wenzelm@18601
   565
      note `B 0`
wenzelm@18601
   566
      show "Q 0" sorry
wenzelm@18601
   567
    }
wenzelm@18601
   568
  next
wenzelm@18601
   569
    case (Suc n)
wenzelm@18601
   570
    note `A n ==> P n` and `B n ==> Q n`
wenzelm@18601
   571
    {
wenzelm@18601
   572
      case 1
wenzelm@18601
   573
      note `A (Suc n)`
wenzelm@18601
   574
      show "P (Suc n)" sorry
wenzelm@18601
   575
    next
wenzelm@18601
   576
      case 2
wenzelm@18601
   577
      note `B (Suc n)`
wenzelm@18601
   578
      show "Q (Suc n)" sorry
wenzelm@18601
   579
    }
wenzelm@18601
   580
  qed
wenzelm@18601
   581
wenzelm@18506
   582
If simultaneous goals are to be used with mutual rules, the statement
wenzelm@18506
   583
needs to be structured carefully as a two-level conjunction, using
wenzelm@18506
   584
lists of propositions separated by 'and':
wenzelm@18506
   585
wenzelm@18507
   586
  lemma
wenzelm@18507
   587
    shows "a : A ==> P1 a"
wenzelm@18507
   588
          "a : A ==> P2 a"
wenzelm@18507
   589
      and "b : B ==> Q1 b"
wenzelm@18507
   590
          "b : B ==> Q2 b"
wenzelm@18507
   591
          "b : B ==> Q3 b"
wenzelm@18507
   592
  proof (induct set: A B)
wenzelm@18480
   593
wenzelm@18399
   594
* Provers/induct: support coinduction as well.  See
wenzelm@18399
   595
src/HOL/Library/Coinductive_List.thy for various examples.
wenzelm@18399
   596
wenzelm@20919
   597
* Attribute "symmetric" produces result with standardized schematic
wenzelm@20919
   598
variables (index 0).  Potential INCOMPATIBILITY.
wenzelm@20919
   599
wenzelm@22126
   600
* Simplifier: by default the simplifier trace only shows top level
wenzelm@22126
   601
rewrites now. That is, trace_simp_depth_limit is set to 1 by
wenzelm@22126
   602
default. Thus there is less danger of being flooded by the trace. The
wenzelm@22126
   603
trace indicates where parts have been suppressed.
nipkow@18674
   604
  
wenzelm@18536
   605
* Provers/classical: removed obsolete classical version of elim_format
wenzelm@18536
   606
attribute; classical elim/dest rules are now treated uniformly when
wenzelm@18536
   607
manipulating the claset.
wenzelm@18536
   608
wenzelm@18694
   609
* Provers/classical: stricter checks to ensure that supplied intro,
wenzelm@18694
   610
dest and elim rules are well-formed; dest and elim rules must have at
wenzelm@18694
   611
least one premise.
wenzelm@18694
   612
wenzelm@18694
   613
* Provers/classical: attributes dest/elim/intro take an optional
wenzelm@18695
   614
weight argument for the rule (just as the Pure versions).  Weights are
wenzelm@18696
   615
ignored by automated tools, but determine the search order of single
wenzelm@18694
   616
rule steps.
paulson@18557
   617
wenzelm@18536
   618
* Syntax: input syntax now supports dummy variable binding "%_. b",
wenzelm@18536
   619
where the body does not mention the bound variable.  Note that dummy
wenzelm@18536
   620
patterns implicitly depend on their context of bounds, which makes
wenzelm@18536
   621
"{_. _}" match any set comprehension as expected.  Potential
wenzelm@18536
   622
INCOMPATIBILITY -- parse translations need to cope with syntactic
wenzelm@18536
   623
constant "_idtdummy" in the binding position.
wenzelm@18536
   624
wenzelm@18536
   625
* Syntax: removed obsolete syntactic constant "_K" and its associated
wenzelm@18536
   626
parse translation.  INCOMPATIBILITY -- use dummy abstraction instead,
wenzelm@18536
   627
for example "A -> B" => "Pi A (%_. B)".
wenzelm@17779
   628
wenzelm@20582
   629
* Pure: 'class_deps' command visualizes the subclass relation, using
wenzelm@20582
   630
the graph browser tool.
wenzelm@20582
   631
wenzelm@20620
   632
* Pure: 'print_theory' now suppresses entities with internal name
wenzelm@20620
   633
(trailing "_") by default; use '!' option for full details.
wenzelm@20620
   634
wenzelm@17865
   635
nipkow@17806
   636
*** HOL ***
nipkow@17806
   637
kleing@24333
   638
* HOL-Word:
kleing@24333
   639
  New extensive library and type for generic, fixed size machine
kleing@24333
   640
  words, with arithemtic, bit-wise, shifting and rotating operations,
kleing@24333
   641
  reflection into int, nat, and bool lists, automation for linear
kleing@24333
   642
  arithmetic (by automatic reflection into nat or int), including
kleing@24333
   643
  lemmas on overflow and monotonicity. Instantiated to all appropriate
kleing@24333
   644
  arithmetic type classes, supporting automatic simplification of
kleing@24333
   645
  numerals on all operations. Jointly developed by NICTA, Galois, and
kleing@24333
   646
  PSU.
kleing@24333
   647
kleing@24333
   648
* Library/Boolean_Algebra: locales for abstract boolean algebras.
kleing@24333
   649
kleing@24333
   650
* Library/Numeral_Type: numbers as types, e.g. TYPE(32).
kleing@24333
   651
haftmann@23850
   652
* Code generator library theories:
haftmann@23850
   653
  * Pretty_Int represents HOL integers by big integer literals in target
haftmann@23850
   654
    languages.
haftmann@23850
   655
  * Pretty_Char represents HOL characters by character literals in target
haftmann@23850
   656
    languages.
haftmann@23850
   657
  * Pretty_Char_chr like Pretty_Char, but also offers treatment of character
haftmann@23850
   658
    codes; includes Pretty_Int.
haftmann@23850
   659
  * Executable_Set allows to generate code for finite sets using lists.
haftmann@23850
   660
  * Executable_Rat implements rational numbers as triples (sign, enumerator,
haftmann@23850
   661
    denominator).
haftmann@23850
   662
  * Executable_Real implements a subset of real numbers, namly those
haftmann@23850
   663
    representable by rational numbers.
haftmann@23850
   664
  * Efficient_Nat implements natural numbers by integers, which in general will
haftmann@23850
   665
    result in higher efficency; pattern matching with 0/Suc is eliminated;
haftmann@23850
   666
    includes Pretty_Int.
haftmann@23850
   667
  * ML_String provides an additional datatype ml_string; in the HOL default
haftmann@23850
   668
    setup, strings in HOL are mapped to lists of HOL characters in SML; values
haftmann@23850
   669
    of type ml_string are mapped to strings in SML.
haftmann@23850
   670
  * ML_Int provides an additional datatype ml_int which is mapped to to SML
haftmann@23850
   671
    built-in integers.
haftmann@23850
   672
berghofe@23783
   673
* New package for inductive predicates
berghofe@23783
   674
berghofe@23783
   675
  An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via
berghofe@23783
   676
berghofe@23783
   677
    inductive
berghofe@23783
   678
      p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
berghofe@23783
   679
      for z_1 :: U_1 and ... and z_n :: U_m
berghofe@23783
   680
    where
berghofe@23783
   681
      rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
berghofe@23783
   682
    | ...
berghofe@23783
   683
berghofe@23783
   684
  rather than
berghofe@23783
   685
berghofe@23783
   686
    consts s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
berghofe@23783
   687
berghofe@23783
   688
    abbreviation p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
berghofe@23783
   689
    where "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
berghofe@23783
   690
berghofe@23783
   691
    inductive "s z_1 ... z_m"
berghofe@23783
   692
    intros
berghofe@23783
   693
      rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
berghofe@23783
   694
      ...
berghofe@23783
   695
berghofe@23783
   696
  For backward compatibility, there is a wrapper allowing inductive
berghofe@23783
   697
  sets to be defined with the new package via
berghofe@23783
   698
berghofe@23783
   699
    inductive_set
berghofe@23783
   700
      s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
berghofe@23783
   701
      for z_1 :: U_1 and ... and z_n :: U_m
berghofe@23783
   702
    where
berghofe@23783
   703
      rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
berghofe@23783
   704
    | ...
berghofe@23783
   705
berghofe@23783
   706
  or
berghofe@23783
   707
berghofe@23783
   708
    inductive_set
berghofe@23783
   709
      s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
berghofe@23783
   710
      and p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
berghofe@23783
   711
      for z_1 :: U_1 and ... and z_n :: U_m
berghofe@23783
   712
    where
berghofe@23783
   713
      "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
berghofe@23783
   714
    | rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
berghofe@23783
   715
    | ...
berghofe@23783
   716
berghofe@23783
   717
  if the additional syntax "p ..." is required.
berghofe@23783
   718
berghofe@23783
   719
  Many examples can be found in the subdirectories Auth, Bali, Induct,
berghofe@23783
   720
  or MicroJava.
berghofe@23783
   721
berghofe@23783
   722
  INCOMPATIBILITIES:
berghofe@23783
   723
berghofe@23783
   724
  - Since declaration and definition of inductive sets or predicates
berghofe@23783
   725
    is no longer separated, abbreviations involving the newly introduced
berghofe@23783
   726
    sets or predicates must be specified together with the introduction
berghofe@23783
   727
    rules after the "where" keyword (see example above), rather than before
berghofe@23783
   728
    the actual inductive definition.
berghofe@23783
   729
berghofe@23783
   730
  - The variables in induction and elimination rules are now quantified
berghofe@23783
   731
    in the order of their occurrence in the introduction rules, rather than
berghofe@23783
   732
    in alphabetical order. Since this may break some proofs, these proofs
berghofe@23783
   733
    either have to be repaired, e.g. by reordering the variables
berghofe@23783
   734
    a_i_1 ... a_i_{k_i} in Isar "case" statements of the form
berghofe@23783
   735
berghofe@23783
   736
      case (rule_i a_i_1 ... a_i_{k_i})
berghofe@23783
   737
berghofe@23783
   738
    or the old order of quantification has to be restored by explicitly adding
berghofe@23783
   739
    meta-level quantifiers in the introduction rules, i.e.
berghofe@23783
   740
berghofe@23783
   741
      | rule_i: "!!a_i_1 ... a_i_{k_i}. ... ==> p z_1 ... z_m t_i_1 ... t_i_n"
berghofe@23783
   742
berghofe@23783
   743
  - The format of the elimination rules is now
berghofe@23783
   744
berghofe@23783
   745
      p z_1 ... z_m x_1 ... x_n ==>
berghofe@23783
   746
        (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
berghofe@23783
   747
        ==> ... ==> P
berghofe@23783
   748
berghofe@23783
   749
    for predicates and
berghofe@23783
   750
berghofe@23783
   751
      (x_1, ..., x_n) : s z_1 ... z_m ==>
berghofe@23783
   752
        (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
berghofe@23783
   753
        ==> ... ==> P
berghofe@23783
   754
berghofe@23783
   755
    for sets rather than
berghofe@23783
   756
berghofe@23783
   757
      x : s z_1 ... z_m ==>
berghofe@23783
   758
        (!!a_1_1 ... a_1_{k_1}. x = (t_1_1, ..., t_1_n) ==> ... ==> P)
berghofe@23783
   759
        ==> ... ==> P
berghofe@23783
   760
berghofe@23783
   761
    This may require terms in goals to be expanded to n-tuples (e.g. using case_tac
berghofe@23783
   762
    or simplification with the split_paired_all rule) before the above elimination
berghofe@23783
   763
    rule is applicable.
berghofe@23783
   764
berghofe@23783
   765
  - The elimination or case analysis rules for (mutually) inductive sets or
berghofe@23783
   766
    predicates are now called "p_1.cases" ... "p_k.cases". The list of rules
berghofe@23783
   767
    "p_1_..._p_k.elims" is no longer available.
berghofe@23783
   768
wenzelm@23562
   769
* Method "metis" proves goals by applying the Metis general-purpose
wenzelm@23562
   770
resolution prover.  Examples are in the directory MetisExamples.  See
wenzelm@23562
   771
also http://gilith.com/software/metis/
paulson@23449
   772
  
wenzelm@23562
   773
* Command 'sledgehammer' invokes external automatic theorem provers as
wenzelm@23562
   774
background processes.  It generates calls to the "metis" method if
wenzelm@23562
   775
successful. These can be pasted into the proof.  Users do not have to
wenzelm@23562
   776
wait for the automatic provers to return.
paulson@23449
   777
nipkow@23564
   778
* Case-expressions allow arbitrary constructor-patterns (including "_") and
nipkow@23565
   779
  take their order into account, like in functional programming.
nipkow@23564
   780
  Internally, this is translated into nested case-expressions; missing cases
nipkow@23564
   781
  are added and mapped to the predefined constant "undefined". In complicated
nipkow@23564
   782
  cases printing may no longer show the original input but the internal
nipkow@23565
   783
  form. Lambda-abstractions allow the same form of pattern matching:
nipkow@23564
   784
  "% pat1 => e1 | ..." is an abbreviation for
nipkow@23564
   785
  "%x. case x of pat1 => e1 | ..." where x is a new variable.
nipkow@23564
   786
huffman@23468
   787
* IntDef: The constant "int :: nat => int" has been removed; now "int"
huffman@23468
   788
  is an abbreviation for "of_nat :: nat => int". The simplification rules
huffman@23468
   789
  for "of_nat" have been changed to work like "int" did previously.
huffman@23468
   790
  (potential INCOMPATIBILITY)
huffman@23468
   791
  - "of_nat (Suc m)" simplifies to "1 + of_nat m" instead of "of_nat m + 1"
huffman@23468
   792
  - of_nat_diff and of_nat_mult are no longer default simp rules
huffman@23377
   793
chaieb@23295
   794
* Method "algebra" solves polynomial equations over (semi)rings using
chaieb@23295
   795
  Groebner bases. The (semi)ring structure is defined by locales and
chaieb@23295
   796
  the tool setup depends on that generic context. Installing the
chaieb@23295
   797
  method for a specific type involves instantiating the locale and
chaieb@23295
   798
  possibly adding declarations for computation on the coefficients.
chaieb@23295
   799
  The method is already instantiated for natural numbers and for the
chaieb@23295
   800
  axiomatic class of idoms with numerals.  See also the paper by
chaieb@23295
   801
  Chaieb and Wenzel at CALCULEMUS 2007 for the general principles
chaieb@23295
   802
  underlying this architecture of context-aware proof-tools.
chaieb@23295
   803
haftmann@23029
   804
* constant "List.op @" now named "List.append".  Use ML antiquotations
haftmann@23029
   805
@{const_name List.append} or @{term " ... @ ... "} to circumvent
haftmann@23029
   806
possible incompatibilities when working on ML level.
haftmann@23029
   807
haftmann@22997
   808
* Constant renames due to introduction of canonical name prefixing for
haftmann@22997
   809
  class package:
haftmann@22997
   810
haftmann@22997
   811
    HOL.abs ~> HOL.minus_class.abs
haftmann@22997
   812
    HOL.divide ~> HOL.divide_class.divide
haftmann@22997
   813
    Nat.power ~> Nat.power_class.power
haftmann@22997
   814
    Nat.size ~> Nat.size_class.size
haftmann@22997
   815
    Numeral.number_of ~> Numeral.number_class.number_of
haftmann@23129
   816
    FixedPoint.Inf ~> FixedPoint.complete_lattice_class.Inf
haftmann@23129
   817
haftmann@23180
   818
* Rudimentary class target mechanism involves constant renames:
haftmann@23129
   819
haftmann@23129
   820
    Orderings.min ~> Orderings.ord_class.min
haftmann@23129
   821
    Orderings.max ~> Orderings.ord_class.max
haftmann@23129
   822
    FixedPoint.Sup ~> FixedPoint.complete_lattice_class.Sup
haftmann@22997
   823
nipkow@23564
   824
* primrec: missing cases mapped to "undefined" instead of "arbitrary"
haftmann@22845
   825
haftmann@22845
   826
* new constant "undefined" with axiom "undefined x = undefined"
haftmann@22845
   827
haftmann@22845
   828
* new class "default" with associated constant "default"
haftmann@22845
   829
nipkow@23104
   830
* new function listsum :: 'a list => 'a for arbitrary monoids.
nipkow@23104
   831
  Special syntax: "SUM x <- xs. f x" (and latex variants)
nipkow@23104
   832
nipkow@23210
   833
* new (input only) syntax for Haskell-like list comprehension, eg
nipkow@23210
   834
  [(x,y). x <- xs, y <- ys, x ~= y]
nipkow@23210
   835
  For details see List.thy.
nipkow@23102
   836
nipkow@23300
   837
* The special syntax for function "filter" has changed from [x : xs. P] to
nipkow@23300
   838
  [x <- xs. P] to avoid an ambiguity caused by list comprehension syntax,
nipkow@23300
   839
  and for uniformity. INCOMPATIBILITY
nipkow@23300
   840
krauss@23971
   841
* Lemma "set_take_whileD" renamed to "set_takeWhileD"
krauss@23971
   842
nipkow@23480
   843
* New lemma collection field_simps (an extension of ring_simps)
nipkow@23480
   844
  for manipulating (in)equations involving division. Multiplies
nipkow@23481
   845
  with all denominators that can be proved to be non-zero (in equations)
nipkow@23480
   846
  or positive/negative (in inequations).
nipkow@23480
   847
nipkow@23480
   848
* Lemma collections ring_eq_simps, group_eq_simps and ring_distrib
nipkow@23478
   849
  have been improved and renamed to ring_simps, group_simps and ring_distribs.
nipkow@23509
   850
  Removed lemmas field_xyz in Ring_and_Field
nipkow@23509
   851
  because they were subsumed by lemmas xyz.
nipkow@23509
   852
INCOMPATIBILITY.
nipkow@23478
   853
haftmann@22799
   854
* Library/Pretty_Int.thy: maps HOL numerals on target language integer literals
nipkow@23480
   855
  when generating code.
haftmann@22799
   856
haftmann@22799
   857
* Library/Pretty_Char.thy: maps HOL characters on target language character literals
nipkow@23480
   858
  when generating code.
haftmann@22799
   859
haftmann@22735
   860
* Library/Commutative_Ring.thy: switched from recdef to function package;
nipkow@23480
   861
  constants add, mul, pow now curried.  Infix syntax for algebraic operations.
haftmann@22735
   862
haftmann@22450
   863
* Some steps towards more uniform lattice theory development in HOL.
haftmann@22422
   864
haftmann@22422
   865
    constants "meet" and "join" now named "inf" and "sup"
haftmann@22422
   866
    constant "Meet" now named "Inf"
haftmann@22422
   867
haftmann@22450
   868
    classes "meet_semilorder" and "join_semilorder" now named
haftmann@22450
   869
      "lower_semilattice" and "upper_semilattice"
haftmann@22450
   870
    class "lorder" now named "lattice"
haftmann@22450
   871
    class "comp_lat" now named "complete_lattice"
haftmann@22450
   872
haftmann@22450
   873
    Instantiation of lattice classes allows explicit definitions
haftmann@22450
   874
    for "inf" and "sup" operations.
haftmann@22450
   875
haftmann@23129
   876
  INCOMPATIBILITY.  Theorem renames:
haftmann@22450
   877
haftmann@22422
   878
    meet_left_le            ~> inf_le1
haftmann@22422
   879
    meet_right_le           ~> inf_le2
haftmann@22422
   880
    join_left_le            ~> sup_ge1
haftmann@22422
   881
    join_right_le           ~> sup_ge2
haftmann@22422
   882
    meet_join_le            ~> inf_sup_ord
haftmann@22422
   883
    le_meetI                ~> le_infI
haftmann@22422
   884
    join_leI                ~> le_supI
haftmann@22422
   885
    le_meet                 ~> le_inf_iff
haftmann@22422
   886
    le_join                 ~> ge_sup_conv
haftmann@22422
   887
    meet_idempotent         ~> inf_idem
haftmann@22422
   888
    join_idempotent         ~> sup_idem
haftmann@22422
   889
    meet_comm               ~> inf_commute
haftmann@22422
   890
    join_comm               ~> sup_commute
haftmann@22422
   891
    meet_leI1               ~> le_infI1
haftmann@22422
   892
    meet_leI2               ~> le_infI2
haftmann@22422
   893
    le_joinI1               ~> le_supI1
haftmann@22422
   894
    le_joinI2               ~> le_supI2
haftmann@22422
   895
    meet_assoc              ~> inf_assoc
haftmann@22422
   896
    join_assoc              ~> sup_assoc
haftmann@22422
   897
    meet_left_comm          ~> inf_left_commute
haftmann@22422
   898
    meet_left_idempotent    ~> inf_left_idem
haftmann@22422
   899
    join_left_comm          ~> sup_left_commute
haftmann@22422
   900
    join_left_idempotent    ~> sup_left_idem
haftmann@22422
   901
    meet_aci                ~> inf_aci
haftmann@22422
   902
    join_aci                ~> sup_aci
haftmann@22422
   903
    le_def_meet             ~> le_iff_inf
haftmann@22422
   904
    le_def_join             ~> le_iff_sup
haftmann@22422
   905
    join_absorp2            ~> sup_absorb2
haftmann@22422
   906
    join_absorp1            ~> sup_absorb1
haftmann@22422
   907
    meet_absorp1            ~> inf_absorb1
haftmann@22422
   908
    meet_absorp2            ~> inf_absorb2
haftmann@22422
   909
    meet_join_absorp        ~> inf_sup_absorb
haftmann@22422
   910
    join_meet_absorp        ~> sup_inf_absorb
haftmann@22422
   911
    distrib_join_le         ~> distrib_sup_le
haftmann@22422
   912
    distrib_meet_le         ~> distrib_inf_le
haftmann@22422
   913
haftmann@22422
   914
    add_meet_distrib_left   ~> add_inf_distrib_left
haftmann@22422
   915
    add_join_distrib_left   ~> add_sup_distrib_left
haftmann@22422
   916
    is_join_neg_meet        ~> is_join_neg_inf
haftmann@22422
   917
    is_meet_neg_join        ~> is_meet_neg_sup
haftmann@22422
   918
    add_meet_distrib_right  ~> add_inf_distrib_right
haftmann@22422
   919
    add_join_distrib_right  ~> add_sup_distrib_right
haftmann@22422
   920
    add_meet_join_distribs  ~> add_sup_inf_distribs
haftmann@22422
   921
    join_eq_neg_meet        ~> sup_eq_neg_inf
haftmann@22422
   922
    meet_eq_neg_join        ~> inf_eq_neg_sup
haftmann@22422
   923
    add_eq_meet_join        ~> add_eq_inf_sup
haftmann@22422
   924
    meet_0_imp_0            ~> inf_0_imp_0
haftmann@22422
   925
    join_0_imp_0            ~> sup_0_imp_0
haftmann@22422
   926
    meet_0_eq_0             ~> inf_0_eq_0
haftmann@22422
   927
    join_0_eq_0             ~> sup_0_eq_0
haftmann@22422
   928
    neg_meet_eq_join        ~> neg_inf_eq_sup
haftmann@22422
   929
    neg_join_eq_meet        ~> neg_sup_eq_inf
haftmann@22422
   930
    join_eq_if              ~> sup_eq_if
haftmann@22422
   931
haftmann@22422
   932
    mono_meet               ~> mono_inf
haftmann@22422
   933
    mono_join               ~> mono_sup
haftmann@22422
   934
    meet_bool_eq            ~> inf_bool_eq
haftmann@22422
   935
    join_bool_eq            ~> sup_bool_eq
haftmann@22422
   936
    meet_fun_eq             ~> inf_fun_eq
haftmann@22422
   937
    join_fun_eq             ~> sup_fun_eq
haftmann@22422
   938
    meet_set_eq             ~> inf_set_eq
haftmann@22422
   939
    join_set_eq             ~> sup_set_eq
haftmann@22422
   940
    meet1_iff               ~> inf1_iff
haftmann@22422
   941
    meet2_iff               ~> inf2_iff
haftmann@22422
   942
    meet1I                  ~> inf1I
haftmann@22422
   943
    meet2I                  ~> inf2I
haftmann@22422
   944
    meet1D1                 ~> inf1D1
haftmann@22422
   945
    meet2D1                 ~> inf2D1
haftmann@22422
   946
    meet1D2                 ~> inf1D2
haftmann@22422
   947
    meet2D2                 ~> inf2D2
haftmann@22422
   948
    meet1E                  ~> inf1E
haftmann@22422
   949
    meet2E                  ~> inf2E
haftmann@22422
   950
    join1_iff               ~> sup1_iff
haftmann@22422
   951
    join2_iff               ~> sup2_iff
haftmann@22422
   952
    join1I1                 ~> sup1I1
haftmann@22422
   953
    join2I1                 ~> sup2I1
haftmann@22422
   954
    join1I1                 ~> sup1I1
haftmann@22422
   955
    join2I2                 ~> sup1I2
haftmann@22422
   956
    join1CI                 ~> sup1CI
haftmann@22422
   957
    join2CI                 ~> sup2CI
haftmann@22422
   958
    join1E                  ~> sup1E
haftmann@22422
   959
    join2E                  ~> sup2E
haftmann@22422
   960
haftmann@22422
   961
    is_meet_Meet            ~> is_meet_Inf
haftmann@22422
   962
    Meet_bool_def           ~> Inf_bool_def
haftmann@22422
   963
    Meet_fun_def            ~> Inf_fun_def
haftmann@22422
   964
    Meet_greatest           ~> Inf_greatest
haftmann@22422
   965
    Meet_lower              ~> Inf_lower
haftmann@22422
   966
    Meet_set_def            ~> Inf_set_def
haftmann@22422
   967
haftmann@22422
   968
    listsp_meetI            ~> listsp_infI
haftmann@22422
   969
    listsp_meet_eq          ~> listsp_inf_eq
haftmann@22422
   970
haftmann@22450
   971
    meet_min                ~> inf_min
haftmann@22450
   972
    join_max                ~> sup_max
haftmann@22450
   973
haftmann@22845
   974
* Classes "order" and "linorder": facts "refl", "trans" and
haftmann@22384
   975
"cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to
haftmann@22384
   976
avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY.
haftmann@22384
   977
haftmann@22845
   978
* Classes "order" and "linorder": 
haftmann@22316
   979
potential INCOMPATIBILITY: order of proof goals in order/linorder instance
haftmann@22316
   980
proofs changed.
haftmann@22316
   981
haftmann@22218
   982
* Dropped lemma duplicate def_imp_eq in favor of meta_eq_to_obj_eq.
haftmann@22218
   983
INCOMPATIBILITY.
haftmann@22218
   984
haftmann@22218
   985
* Dropped lemma duplicate if_def2 in favor of if_bool_eq_conj.
haftmann@22218
   986
INCOMPATIBILITY.
haftmann@22218
   987
wenzelm@22126
   988
* Added syntactic class "size"; overloaded constant "size" now has
wenzelm@22126
   989
type "'a::size ==> bool"
wenzelm@22126
   990
wenzelm@22126
   991
* Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op
haftmann@22997
   992
dvd" to "Divides.div_class.div", "Divides.div_class.mod" and "Divides.dvd". INCOMPATIBILITY.
wenzelm@22126
   993
wenzelm@22126
   994
* Added method "lexicographic_order" automatically synthesizes
wenzelm@22126
   995
termination relations as lexicographic combinations of size measures
wenzelm@22126
   996
-- 'function' package.
wenzelm@22126
   997
wenzelm@22126
   998
* HOL/records: generalised field-update to take a function on the
wenzelm@22126
   999
field rather than the new value: r(|A := x|) is translated to A_update
wenzelm@22126
  1000
(K x) r The K-combinator that is internally used is called K_record.
schirmer@21226
  1001
INCOMPATIBILITY: Usage of the plain update functions has to be
schirmer@21226
  1002
adapted.
schirmer@21226
  1003
 
wenzelm@22126
  1004
* axclass "semiring_0" now contains annihilation axioms x * 0 = 0 and
wenzelm@22126
  1005
0 * x = 0, which are required for a semiring.  Richer structures do
wenzelm@22126
  1006
not inherit from semiring_0 anymore, because this property is a
wenzelm@22126
  1007
theorem there, not an axiom.  INCOMPATIBILITY: In instances of
wenzelm@22126
  1008
semiring_0, there is more to prove, but this is mostly trivial.
wenzelm@22126
  1009
wenzelm@22126
  1010
* axclass "recpower" was generalized to arbitrary monoids, not just
wenzelm@22126
  1011
commutative semirings.  INCOMPATIBILITY: If you use recpower and need
wenzelm@22126
  1012
commutativity or a semiring property, add the corresponding classes.
wenzelm@22126
  1013
wenzelm@22126
  1014
* Unified locale partial_order with class definition (cf. theory
wenzelm@22126
  1015
Orderings), added parameter ``less''.  INCOMPATIBILITY.
haftmann@21215
  1016
haftmann@21099
  1017
* Constant "List.list_all2" in List.thy now uses authentic syntax.
wenzelm@22126
  1018
INCOMPATIBILITY: translations containing list_all2 may go wrong.  On
wenzelm@22126
  1019
Isar level, use abbreviations instead.
wenzelm@22126
  1020
wenzelm@22126
  1021
* Renamed constant "List.op mem" to "List.memberl" INCOMPATIBILITY:
wenzelm@22126
  1022
rarely occuring name references (e.g. ``List.op mem.simps'') require
wenzelm@22126
  1023
renaming (e.g. ``List.memberl.simps'').
wenzelm@22126
  1024
haftmann@22997
  1025
* Renamed constants "0" to "HOL.zero_class.zero" and "1" to "HOL.one_class.one".
wenzelm@22126
  1026
INCOMPATIBILITY.
wenzelm@22126
  1027
haftmann@23251
  1028
* Added class "HOL.eq", allowing for code generation with polymorphic equality.
wenzelm@22126
  1029
wenzelm@22126
  1030
* Numeral syntax: type 'bin' which was a mere type copy of 'int' has
wenzelm@22126
  1031
been abandoned in favour of plain 'int'. INCOMPATIBILITY --
wenzelm@22126
  1032
significant changes for setting up numeral syntax for types:
haftmann@20485
  1033
haftmann@20485
  1034
  - new constants Numeral.pred and Numeral.succ instead
haftmann@20485
  1035
      of former Numeral.bin_pred and Numeral.bin_succ.
haftmann@20485
  1036
  - Use integer operations instead of bin_add, bin_mult and so on.
haftmann@20485
  1037
  - Numeral simplification theorems named Numeral.numeral_simps instead of Bin_simps.
haftmann@20485
  1038
  - ML structure Bin_Simprocs now named Int_Numeral_Base_Simprocs.
haftmann@20485
  1039
haftmann@20485
  1040
See HOL/Integ/IntArith.thy for an example setup.
haftmann@20485
  1041
wenzelm@22126
  1042
* New top level command 'normal_form' computes the normal form of a
wenzelm@22126
  1043
term that may contain free variables. For example ``normal_form
wenzelm@22126
  1044
"rev[a,b,c]"'' produces ``[b,c,a]'' (without proof).  This command is
wenzelm@22126
  1045
suitable for heavy-duty computations because the functions are
wenzelm@22126
  1046
compiled to ML first.
nipkow@19895
  1047
wenzelm@17996
  1048
* Alternative iff syntax "A <-> B" for equality on bool (with priority
wenzelm@17996
  1049
25 like -->); output depends on the "iff" print_mode, the default is
wenzelm@17996
  1050
"A = B" (with priority 50).
wenzelm@17996
  1051
ballarin@19279
  1052
* Renamed constants in HOL.thy and Orderings.thy:
haftmann@22997
  1053
    op +   ~> HOL.plus_class.plus
haftmann@22997
  1054
    op -   ~> HOL.minus_class.minus
haftmann@22997
  1055
    uminus ~> HOL.minus_class.uminus
haftmann@23881
  1056
    abs    ~> HOL.abs_class.abs
haftmann@22997
  1057
    op *   ~> HOL.times_class.times
haftmann@23881
  1058
    op <   ~> HOL.ord_class.less
haftmann@23881
  1059
    op <=  ~> HOL.ord_class.less_eq
haftmann@19233
  1060
haftmann@19233
  1061
Adaptions may be required in the following cases:
haftmann@19233
  1062
nipkow@19377
  1063
a) User-defined constants using any of the names "plus", "minus", "times",
nipkow@19377
  1064
"less" or "less_eq". The standard syntax translations for "+", "-" and "*"
nipkow@19377
  1065
may go wrong.
haftmann@19233
  1066
INCOMPATIBILITY: use more specific names.
haftmann@19233
  1067
haftmann@19277
  1068
b) Variables named "plus", "minus", "times", "less", "less_eq"
haftmann@19233
  1069
INCOMPATIBILITY: use more specific names.
haftmann@19233
  1070
nipkow@19377
  1071
c) Permutative equations (e.g. "a + b = b + a")
nipkow@19377
  1072
Since the change of names also changes the order of terms, permutative
nipkow@19377
  1073
rewrite rules may get applied in a different order. Experience shows that
nipkow@19377
  1074
this is rarely the case (only two adaptions in the whole Isabelle
nipkow@19377
  1075
distribution).
nipkow@19377
  1076
INCOMPATIBILITY: rewrite proofs
haftmann@19233
  1077
haftmann@19233
  1078
d) ML code directly refering to constant names
haftmann@19233
  1079
This in general only affects hand-written proof tactics, simprocs and so on.
haftmann@22997
  1080
INCOMPATIBILITY: grep your sourcecode and replace names.  Consider use
haftmann@22997
  1081
of const_name ML antiquotations.
haftmann@19233
  1082
wenzelm@21265
  1083
* Relations less (<) and less_eq (<=) are also available on type bool.
wenzelm@21265
  1084
Modified syntax to disallow nesting without explicit parentheses,
wenzelm@21265
  1085
e.g. "(x < y) < z" or "x < (y < z)", but NOT "x < y < z".
wenzelm@21265
  1086
nipkow@18674
  1087
* "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
nipkow@18674
  1088
krauss@20716
  1089
* Relation composition operator "op O" now has precedence 75 and binds
krauss@20716
  1090
stronger than union and intersection. INCOMPATIBILITY.
krauss@20716
  1091
wenzelm@22126
  1092
* The old set interval syntax "{m..n(}" (and relatives) has been
wenzelm@22126
  1093
removed.  Use "{m..<n}" (and relatives) instead.
nipkow@19377
  1094
wenzelm@17865
  1095
* In the context of the assumption "~(s = t)" the Simplifier rewrites
wenzelm@17865
  1096
"t = s" to False (by simproc "neq_simproc").  For backward
wenzelm@17865
  1097
compatibility this can be disabled by ML "reset use_neq_simproc".
wenzelm@17779
  1098
wenzelm@22126
  1099
* "m dvd n" where m and n are numbers is evaluated to True/False by
wenzelm@22126
  1100
simp.
wenzelm@22126
  1101
wenzelm@22126
  1102
* Theorem Cons_eq_map_conv no longer declared as ``simp''.
nipkow@19211
  1103
ballarin@19279
  1104
* Theorem setsum_mult renamed to setsum_right_distrib.
ballarin@19279
  1105
nipkow@19211
  1106
* Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the
wenzelm@22126
  1107
``rule'' method.
wenzelm@22126
  1108
wenzelm@22126
  1109
* Reimplemented methods ``sat'' and ``satx'', with several
wenzelm@22126
  1110
improvements: goals no longer need to be stated as "<prems> ==>
wenzelm@22126
  1111
False", equivalences (i.e. "=" on type bool) are handled, variable
wenzelm@22126
  1112
names of the form "lit_<n>" are no longer reserved, significant
wenzelm@22126
  1113
speedup.
wenzelm@22126
  1114
wenzelm@22126
  1115
* Methods ``sat'' and ``satx'' can now replay MiniSat proof traces.
wenzelm@22126
  1116
zChaff is still supported as well.
wenzelm@22126
  1117
wenzelm@22126
  1118
* 'inductive' and 'datatype': provide projections of mutual rules,
wenzelm@22126
  1119
bundled as foo_bar.inducts;
wenzelm@22126
  1120
wenzelm@22126
  1121
* Library: moved theories Parity, GCD, Binomial, Infinite_Set to
wenzelm@22126
  1122
Library.
wenzelm@21256
  1123
wenzelm@21256
  1124
* Library: moved theory Accessible_Part to main HOL.
wenzelm@19572
  1125
wenzelm@18446
  1126
* Library: added theory Coinductive_List of potentially infinite lists
wenzelm@18446
  1127
as greatest fixed-point.
wenzelm@18399
  1128
wenzelm@19254
  1129
* Library: added theory AssocList which implements (finite) maps as
schirmer@19252
  1130
association lists.
webertj@17809
  1131
wenzelm@22126
  1132
* Added proof method ``evaluation'' for efficiently solving a goal
wenzelm@22126
  1133
(i.e. a boolean expression) by compiling it to ML. The goal is
wenzelm@22126
  1134
"proved" (via an oracle) if it evaluates to True.
wenzelm@20807
  1135
wenzelm@20807
  1136
* Linear arithmetic now splits certain operators (e.g. min, max, abs)
wenzelm@20807
  1137
also when invoked by the simplifier.  This results in the simplifier
haftmann@21056
  1138
being more powerful on arithmetic goals.  INCOMPATIBILITY.  Set
wenzelm@20807
  1139
fast_arith_split_limit to 0 to obtain the old behavior.
webertj@20217
  1140
wenzelm@22126
  1141
* Support for hex (0x20) and binary (0b1001) numerals.
wenzelm@19254
  1142
wenzelm@20807
  1143
* New method: reify eqs (t), where eqs are equations for an
wenzelm@20807
  1144
interpretation I :: 'a list => 'b => 'c and t::'c is an optional
wenzelm@20807
  1145
parameter, computes a term s::'b and a list xs::'a list and proves the
wenzelm@20807
  1146
theorem I xs s = t. This is also known as reification or quoting. The
wenzelm@20807
  1147
resulting theorem is applied to the subgoal to substitute t with I xs
wenzelm@20807
  1148
s.  If t is omitted, the subgoal itself is reified.
wenzelm@20807
  1149
wenzelm@20807
  1150
* New method: reflection corr_thm eqs (t). The parameters eqs and (t)
wenzelm@20807
  1151
are as explained above. corr_thm is a theorem for I vs (f t) = I vs t,
wenzelm@20807
  1152
where f is supposed to be a computable function (in the sense of code
wenzelm@20807
  1153
generattion). The method uses reify to compute s and xs as above then
wenzelm@20807
  1154
applies corr_thm and uses normalization by evaluation to "prove" f s =
wenzelm@20807
  1155
r and finally gets the theorem t = r, which is again applied to the
wenzelm@20807
  1156
subgoal. An Example is available in HOL/ex/ReflectionEx.thy.
wenzelm@20807
  1157
haftmann@23881
  1158
* Reflection: Automatic reification now handels binding, an example
wenzelm@20807
  1159
is available in HOL/ex/ReflectionEx.thy
wenzelm@20807
  1160
wenzelm@20807
  1161
ballarin@20169
  1162
*** HOL-Algebra ***
ballarin@20169
  1163
wenzelm@21170
  1164
* Formalisation of ideals and the quotient construction over rings.
wenzelm@21170
  1165
wenzelm@21170
  1166
* Order and lattice theory no longer based on records.
wenzelm@21170
  1167
INCOMPATIBILITY.
wenzelm@21170
  1168
wenzelm@22126
  1169
* Renamed lemmas least_carrier -> least_closed and greatest_carrier ->
wenzelm@22126
  1170
greatest_closed.  INCOMPATIBILITY.
ballarin@21896
  1171
wenzelm@21170
  1172
* Method algebra is now set up via an attribute.  For examples see
ballarin@21896
  1173
Ring.thy.  INCOMPATIBILITY: the method is now weaker on combinations
wenzelm@21170
  1174
of algebraic structures.
ballarin@20318
  1175
wenzelm@22126
  1176
* Renamed theory CRing to Ring.
ballarin@20169
  1177
wenzelm@20807
  1178
wenzelm@19653
  1179
*** HOL-Complex ***
wenzelm@19653
  1180
wenzelm@19653
  1181
* Theory Real: new method ferrack implements quantifier elimination
wenzelm@19653
  1182
for linear arithmetic over the reals. The quantifier elimination
wenzelm@19653
  1183
feature is used only for decision, for compatibility with arith. This
wenzelm@19653
  1184
means a goal is either solved or left unchanged, no simplification.
wenzelm@19653
  1185
huffman@22971
  1186
* Hyperreal: Functions root and sqrt are now defined on negative real
huffman@22971
  1187
inputs so that root n (- x) = - root n x and sqrt (- x) = - sqrt x.
huffman@22971
  1188
Nonnegativity side conditions have been removed from many lemmas, so
huffman@22971
  1189
that more subgoals may now be solved by simplification; potential
huffman@22971
  1190
INCOMPATIBILITY.
huffman@22971
  1191
huffman@21791
  1192
* Real: New axiomatic classes formalize real normed vector spaces and
huffman@21791
  1193
algebras, using new overloaded constants scaleR :: real => 'a => 'a
huffman@21791
  1194
and norm :: 'a => real.
huffman@21791
  1195
wenzelm@22126
  1196
* Real: New constant of_real :: real => 'a::real_algebra_1 injects
wenzelm@22126
  1197
from reals into other types. The overloaded constant Reals :: 'a set
wenzelm@22126
  1198
is now defined as range of_real; potential INCOMPATIBILITY.
wenzelm@22126
  1199
nipkow@23013
  1200
* Real: ML code generation is supported now and hence also quickcheck.
nipkow@23013
  1201
Reals are implemented as arbitrary precision rationals.
nipkow@23013
  1202
wenzelm@22126
  1203
* Hyperreal: Several constants that previously worked only for the
wenzelm@22126
  1204
reals have been generalized, so they now work over arbitrary vector
wenzelm@22126
  1205
spaces. Type annotations may need to be added in some cases; potential
wenzelm@22126
  1206
INCOMPATIBILITY.
huffman@21791
  1207
huffman@22972
  1208
  Infinitesimal  :: ('a::real_normed_vector) star set
huffman@22972
  1209
  HFinite        :: ('a::real_normed_vector) star set
huffman@22972
  1210
  HInfinite      :: ('a::real_normed_vector) star set
huffman@21791
  1211
  approx         :: ('a::real_normed_vector) star => 'a star => bool
huffman@21791
  1212
  monad          :: ('a::real_normed_vector) star => 'a star set
huffman@21791
  1213
  galaxy         :: ('a::real_normed_vector) star => 'a star set
huffman@22972
  1214
  (NS)LIMSEQ     :: [nat => 'a::real_normed_vector, 'a] => bool
huffman@21791
  1215
  (NS)convergent :: (nat => 'a::real_normed_vector) => bool
huffman@21791
  1216
  (NS)Bseq       :: (nat => 'a::real_normed_vector) => bool
huffman@21791
  1217
  (NS)Cauchy     :: (nat => 'a::real_normed_vector) => bool
huffman@21791
  1218
  (NS)LIM        :: ['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool
huffman@21791
  1219
  is(NS)Cont     :: ['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool
huffman@21791
  1220
  deriv          :: ['a::real_normed_field => 'a, 'a, 'a] => bool
huffman@22972
  1221
  sgn            :: 'a::real_normed_vector => 'a
huffman@23116
  1222
  exp            :: 'a::{recpower,real_normed_field,banach} => 'a
huffman@21791
  1223
huffman@21791
  1224
* Complex: Some complex-specific constants are now abbreviations for
wenzelm@22126
  1225
overloaded ones: complex_of_real = of_real, cmod = norm, hcmod =
wenzelm@22126
  1226
hnorm.  Other constants have been entirely removed in favor of the
wenzelm@22126
  1227
polymorphic versions (INCOMPATIBILITY):
huffman@21791
  1228
huffman@21791
  1229
  approx        <-- capprox
huffman@21791
  1230
  HFinite       <-- CFinite
huffman@21791
  1231
  HInfinite     <-- CInfinite
huffman@21791
  1232
  Infinitesimal <-- CInfinitesimal
huffman@21791
  1233
  monad         <-- cmonad
huffman@21791
  1234
  galaxy        <-- cgalaxy
huffman@21791
  1235
  (NS)LIM       <-- (NS)CLIM, (NS)CRLIM
huffman@21791
  1236
  is(NS)Cont    <-- is(NS)Contc, is(NS)contCR
huffman@21791
  1237
  (ns)deriv     <-- (ns)cderiv
huffman@21791
  1238
wenzelm@19653
  1239
wenzelm@17878
  1240
*** ML ***
wenzelm@17878
  1241
haftmann@23251
  1242
* Generic arithmetic modules: Tools/integer.ML, Tools/rat.ML, Tools/float.ML
haftmann@23251
  1243
wenzelm@22848
  1244
* Context data interfaces (Theory/Proof/GenericDataFun): removed
wenzelm@22863
  1245
name/print, uninitialized data defaults to ad-hoc copy of empty value,
wenzelm@22863
  1246
init only required for impure data.  INCOMPATIBILITY: empty really
wenzelm@22863
  1247
need to be empty (no dependencies on theory content!)
wenzelm@22848
  1248
wenzelm@22138
  1249
* ML within Isar: antiquotations allow to embed statically-checked
wenzelm@22138
  1250
formal entities in the source, referring to the context available at
wenzelm@22138
  1251
compile-time.  For example:
wenzelm@22138
  1252
wenzelm@22138
  1253
ML {* @{typ "'a => 'b"} *}
wenzelm@22138
  1254
ML {* @{term "%x. x"} *}
wenzelm@22138
  1255
ML {* @{prop "x == y"} *}
wenzelm@22138
  1256
ML {* @{ctyp "'a => 'b"} *}
wenzelm@22138
  1257
ML {* @{cterm "%x. x"} *}
wenzelm@22138
  1258
ML {* @{cprop "x == y"} *}
wenzelm@22138
  1259
ML {* @{thm asm_rl} *}
wenzelm@22138
  1260
ML {* @{thms asm_rl} *}
wenzelm@22376
  1261
ML {* @{const_name c} *}
wenzelm@22376
  1262
ML {* @{const_syntax c} *}
wenzelm@22138
  1263
ML {* @{context} *}
wenzelm@22138
  1264
ML {* @{theory} *}
wenzelm@22138
  1265
ML {* @{theory Pure} *}
wenzelm@22138
  1266
ML {* @{simpset} *}
wenzelm@22138
  1267
ML {* @{claset} *}
wenzelm@22138
  1268
ML {* @{clasimpset} *}
wenzelm@22138
  1269
wenzelm@22151
  1270
The same works for sources being ``used'' within an Isar context.
wenzelm@22151
  1271
wenzelm@22152
  1272
* ML in Isar: improved error reporting; extra verbosity with
wenzelm@22152
  1273
Toplevel.debug enabled.
wenzelm@22152
  1274
haftmann@20348
  1275
* Pure/library:
haftmann@20348
  1276
haftmann@18450
  1277
  val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
haftmann@18549
  1278
  val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
haftmann@18450
  1279
wenzelm@18540
  1280
The semantics of "burrow" is: "take a function with *simulatanously*
wenzelm@18540
  1281
transforms a list of value, and apply it *simulatanously* to a list of
wenzelm@22126
  1282
list of values of the appropriate type". Compare this with "map" which
wenzelm@18540
  1283
would *not* apply its argument function simulatanously but in
wenzelm@22126
  1284
sequence; "fold_burrow" has an additional context.
haftmann@18450
  1285
wenzelm@18446
  1286
* Pure/library: functions map2 and fold2 with curried syntax for
wenzelm@18446
  1287
simultanous mapping and folding:
wenzelm@18446
  1288
haftmann@18422
  1289
    val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
haftmann@18422
  1290
    val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
haftmann@18422
  1291
wenzelm@18446
  1292
* Pure/library: indexed lists - some functions in the Isabelle library
wenzelm@18446
  1293
treating lists over 'a as finite mappings from [0...n] to 'a have been
wenzelm@18446
  1294
given more convenient names and signatures reminiscent of similar
wenzelm@18446
  1295
functions for alists, tables, etc:
haftmann@18051
  1296
haftmann@18051
  1297
  val nth: 'a list -> int -> 'a 
haftmann@18051
  1298
  val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
haftmann@18051
  1299
  val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
haftmann@18051
  1300
wenzelm@18446
  1301
Note that fold_index starts counting at index 0, not 1 like foldln
wenzelm@18446
  1302
used to.
wenzelm@18446
  1303
wenzelm@22126
  1304
* Pure/library: added general ``divide_and_conquer'' combinator on
wenzelm@22126
  1305
lists.
wenzelm@19032
  1306
wenzelm@19032
  1307
* Pure/General/table.ML: the join operations now works via exceptions
wenzelm@19081
  1308
DUP/SAME instead of type option.  This is simpler in simple cases, and
wenzelm@19081
  1309
admits slightly more efficient complex applications.
wenzelm@18446
  1310
wenzelm@18642
  1311
* Pure: datatype Context.generic joins theory/Proof.context and
wenzelm@18644
  1312
provides some facilities for code that works in either kind of
wenzelm@18642
  1313
context, notably GenericDataFun for uniform theory and proof data.
wenzelm@18642
  1314
wenzelm@18862
  1315
* Pure: 'advanced' translation functions (parse_translation etc.) now
wenzelm@18862
  1316
use Context.generic instead of just theory.
wenzelm@18862
  1317
wenzelm@18737
  1318
* Pure: simplified internal attribute type, which is now always
wenzelm@18737
  1319
Context.generic * thm -> Context.generic * thm.  Global (theory)
wenzelm@18737
  1320
vs. local (Proof.context) attributes have been discontinued, while
wenzelm@18738
  1321
minimizing code duplication.  Thm.rule_attribute and
wenzelm@18738
  1322
Thm.declaration_attribute build canonical attributes; see also
wenzelm@19006
  1323
structure Context for further operations on Context.generic, notably
wenzelm@19006
  1324
GenericDataFun.  INCOMPATIBILITY, need to adapt attribute type
wenzelm@19006
  1325
declarations and definitions.
wenzelm@19006
  1326
wenzelm@19508
  1327
* Pure/kernel: consts certification ignores sort constraints given in
wenzelm@19508
  1328
signature declarations.  (This information is not relevant to the
wenzelm@22126
  1329
logic, but only for type inference.)  IMPORTANT INTERNAL CHANGE,
wenzelm@22126
  1330
potential INCOMPATIBILITY.
wenzelm@19508
  1331
wenzelm@19508
  1332
* Pure: axiomatic type classes are now purely definitional, with
wenzelm@19508
  1333
explicit proofs of class axioms and super class relations performed
wenzelm@19508
  1334
internally.  See Pure/axclass.ML for the main internal interfaces --
wenzelm@19508
  1335
notably AxClass.define_class supercedes AxClass.add_axclass, and
wenzelm@19508
  1336
AxClass.axiomatize_class/classrel/arity supercede
wenzelm@19508
  1337
Sign.add_classes/classrel/arities.
wenzelm@19508
  1338
wenzelm@19006
  1339
* Pure/Isar: Args/Attrib parsers operate on Context.generic --
wenzelm@19006
  1340
global/local versions on theory vs. Proof.context have been
wenzelm@19006
  1341
discontinued; Attrib.syntax and Method.syntax have been adapted
wenzelm@19006
  1342
accordingly.  INCOMPATIBILITY, need to adapt parser expressions for
wenzelm@19006
  1343
attributes, methods, etc.
wenzelm@18642
  1344
wenzelm@18446
  1345
* Pure: several functions of signature "... -> theory -> theory * ..."
wenzelm@18446
  1346
have been reoriented to "... -> theory -> ... * theory" in order to
wenzelm@18446
  1347
allow natural usage in combination with the ||>, ||>>, |-> and
wenzelm@18446
  1348
fold_map combinators.
haftmann@18051
  1349
wenzelm@21647
  1350
* Pure: official theorem names (closed derivations) and additional
wenzelm@21647
  1351
comments (tags) are now strictly separate.  Name hints -- which are
wenzelm@21647
  1352
maintained as tags -- may be attached any time without affecting the
wenzelm@21647
  1353
derivation.
wenzelm@21647
  1354
wenzelm@18020
  1355
* Pure: primitive rule lift_rule now takes goal cterm instead of an
wenzelm@18145
  1356
actual goal state (thm).  Use Thm.lift_rule (Thm.cprem_of st i) to
wenzelm@18020
  1357
achieve the old behaviour.
wenzelm@18020
  1358
wenzelm@18020
  1359
* Pure: the "Goal" constant is now called "prop", supporting a
wenzelm@18020
  1360
slightly more general idea of ``protecting'' meta-level rule
wenzelm@18020
  1361
statements.
wenzelm@18020
  1362
wenzelm@20040
  1363
* Pure: Logic.(un)varify only works in a global context, which is now
wenzelm@20040
  1364
enforced instead of silently assumed.  INCOMPATIBILITY, may use
wenzelm@20040
  1365
Logic.legacy_(un)varify as temporary workaround.
wenzelm@20040
  1366
wenzelm@20090
  1367
* Pure: structure Name provides scalable operations for generating
wenzelm@20090
  1368
internal variable names, notably Name.variants etc.  This replaces
wenzelm@20090
  1369
some popular functions from term.ML:
wenzelm@20090
  1370
wenzelm@20090
  1371
  Term.variant		->  Name.variant
wenzelm@20090
  1372
  Term.variantlist	->  Name.variant_list  (*canonical argument order*)
wenzelm@20090
  1373
  Term.invent_names	->  Name.invent_list
wenzelm@20090
  1374
wenzelm@20090
  1375
Note that low-level renaming rarely occurs in new code -- operations
wenzelm@20090
  1376
from structure Variable are used instead (see below).
wenzelm@20090
  1377
wenzelm@20040
  1378
* Pure: structure Variable provides fundamental operations for proper
wenzelm@20040
  1379
treatment of fixed/schematic variables in a context.  For example,
wenzelm@20040
  1380
Variable.import introduces fixes for schematics of given facts and
wenzelm@20040
  1381
Variable.export reverses the effect (up to renaming) -- this replaces
wenzelm@20040
  1382
various freeze_thaw operations.
wenzelm@20040
  1383
wenzelm@18567
  1384
* Pure: structure Goal provides simple interfaces for
wenzelm@17981
  1385
init/conclude/finish and tactical prove operations (replacing former
wenzelm@20040
  1386
Tactic.prove).  Goal.prove is the canonical way to prove results
wenzelm@20040
  1387
within a given context; Goal.prove_global is a degraded version for
wenzelm@20040
  1388
theory level goals, including a global Drule.standard.  Note that
wenzelm@20040
  1389
OldGoals.prove_goalw_cterm has long been obsolete, since it is
wenzelm@20040
  1390
ill-behaved in a local proof context (e.g. with local fixes/assumes or
wenzelm@20040
  1391
in a locale context).
wenzelm@17981
  1392
wenzelm@18815
  1393
* Isar: simplified treatment of user-level errors, using exception
wenzelm@18687
  1394
ERROR of string uniformly.  Function error now merely raises ERROR,
wenzelm@18686
  1395
without any side effect on output channels.  The Isar toplevel takes
wenzelm@18686
  1396
care of proper display of ERROR exceptions.  ML code may use plain
wenzelm@18686
  1397
handle/can/try; cat_error may be used to concatenate errors like this:
wenzelm@18686
  1398
wenzelm@18686
  1399
  ... handle ERROR msg => cat_error msg "..."
wenzelm@18686
  1400
wenzelm@18686
  1401
Toplevel ML code (run directly or through the Isar toplevel) may be
wenzelm@18687
  1402
embedded into the Isar toplevel with exception display/debug like
wenzelm@18687
  1403
this:
wenzelm@18686
  1404
wenzelm@18686
  1405
  Isar.toplevel (fn () => ...)
wenzelm@18686
  1406
wenzelm@18686
  1407
INCOMPATIBILITY, removed special transform_error facilities, removed
wenzelm@18686
  1408
obsolete variants of user-level exceptions (ERROR_MESSAGE,
wenzelm@18686
  1409
Context.PROOF, ProofContext.CONTEXT, Proof.STATE, ProofHistory.FAIL)
wenzelm@18686
  1410
-- use plain ERROR instead.
wenzelm@18686
  1411
wenzelm@18815
  1412
* Isar: theory setup now has type (theory -> theory), instead of a
wenzelm@18722
  1413
list.  INCOMPATIBILITY, may use #> to compose setup functions.
wenzelm@18722
  1414
wenzelm@18815
  1415
* Isar: installed ML toplevel pretty printer for type Proof.context,
wenzelm@18815
  1416
subject to ProofContext.debug/verbose flags.
wenzelm@18815
  1417
wenzelm@18815
  1418
* Isar: Toplevel.theory_to_proof admits transactions that modify the
wenzelm@18815
  1419
theory before entering a proof state.  Transactions now always see a
wenzelm@18815
  1420
quasi-functional intermediate checkpoint, both in interactive and
wenzelm@18590
  1421
batch mode.
wenzelm@18567
  1422
wenzelm@17878
  1423
* Simplifier: the simpset of a running simplification process now
wenzelm@17878
  1424
contains a proof context (cf. Simplifier.the_context), which is the
wenzelm@17878
  1425
very context that the initial simpset has been retrieved from (by
wenzelm@17890
  1426
simpset_of/local_simpset_of).  Consequently, all plug-in components
wenzelm@17878
  1427
(solver, looper etc.) may depend on arbitrary proof data.
wenzelm@17878
  1428
wenzelm@17878
  1429
* Simplifier.inherit_context inherits the proof context (plus the
wenzelm@17878
  1430
local bounds) of the current simplification process; any simproc
wenzelm@17878
  1431
etc. that calls the Simplifier recursively should do this!  Removed
wenzelm@17878
  1432
former Simplifier.inherit_bounds, which is already included here --
wenzelm@17890
  1433
INCOMPATIBILITY.  Tools based on low-level rewriting may even have to
wenzelm@17890
  1434
specify an explicit context using Simplifier.context/theory_context.
wenzelm@17878
  1435
wenzelm@17878
  1436
* Simplifier/Classical Reasoner: more abstract interfaces
wenzelm@17878
  1437
change_simpset/claset for modifying the simpset/claset reference of a
wenzelm@17878
  1438
theory; raw versions simpset/claset_ref etc. have been discontinued --
wenzelm@17878
  1439
INCOMPATIBILITY.
wenzelm@17878
  1440
wenzelm@18540
  1441
* Provers: more generic wrt. syntax of object-logics, avoid hardwired
wenzelm@18540
  1442
"Trueprop" etc.
wenzelm@18540
  1443
wenzelm@17878
  1444
wenzelm@20988
  1445
*** System ***
wenzelm@20988
  1446
wenzelm@21471
  1447
* settings: ML_IDENTIFIER -- which is appended to user specific heap
wenzelm@21471
  1448
locations -- now includes the Isabelle version identifier as well.
wenzelm@21471
  1449
This simplifies use of multiple Isabelle installations.
wenzelm@21471
  1450
wenzelm@20988
  1451
* isabelle-process: option -S (secure mode) disables some critical
wenzelm@20988
  1452
operations, notably runtime compilation and evaluation of ML source
wenzelm@20988
  1453
code.
wenzelm@20988
  1454
wenzelm@24210
  1455
* Experimental support for multithreading, using Poly/ML 5.1 (internal
wenzelm@24213
  1456
version from CVS). The theory loader exploits parallelism when
wenzelm@24213
  1457
processing independent theories, following the header specifications.
wenzelm@24213
  1458
The maximum number of worker threads is specified via usedir option -M
wenzelm@24213
  1459
or the "max-threads" setting in Proof General.  User-code needs to
wenzelm@24213
  1460
observe certain guidelines for thread-safe programming, see appendix A
wenzelm@24213
  1461
in the Isar Implementation manual.
wenzelm@24210
  1462
wenzelm@17754
  1463
wenzelm@17720
  1464
New in Isabelle2005 (October 2005)
wenzelm@17720
  1465
----------------------------------
wenzelm@14655
  1466
wenzelm@14655
  1467
*** General ***
wenzelm@14655
  1468
nipkow@15130
  1469
* Theory headers: the new header syntax for Isar theories is
nipkow@15130
  1470
nipkow@15130
  1471
  theory <name>
wenzelm@16234
  1472
  imports <theory1> ... <theoryN>
wenzelm@16234
  1473
  uses <file1> ... <fileM>
nipkow@15130
  1474
  begin
nipkow@15130
  1475
wenzelm@16234
  1476
where the 'uses' part is optional.  The previous syntax
wenzelm@16234
  1477
wenzelm@16234
  1478
  theory <name> = <theory1> + ... + <theoryN>:
wenzelm@16234
  1479
wenzelm@16717
  1480
will disappear in the next release.  Use isatool fixheaders to convert
wenzelm@16717
  1481
existing theory files.  Note that there is no change in ancient
wenzelm@17371
  1482
non-Isar theories now, but these will disappear soon.
nipkow@15130
  1483
berghofe@15475
  1484
* Theory loader: parent theories can now also be referred to via
wenzelm@16234
  1485
relative and absolute paths.
wenzelm@16234
  1486
wenzelm@17408
  1487
* Command 'find_theorems' searches for a list of criteria instead of a
wenzelm@17408
  1488
list of constants. Known criteria are: intro, elim, dest, name:string,
wenzelm@17408
  1489
simp:term, and any term. Criteria can be preceded by '-' to select
wenzelm@17408
  1490
theorems that do not match. Intro, elim, dest select theorems that
wenzelm@17408
  1491
match the current goal, name:s selects theorems whose fully qualified
wenzelm@17408
  1492
name contain s, and simp:term selects all simplification rules whose
wenzelm@17408
  1493
lhs match term.  Any other term is interpreted as pattern and selects
wenzelm@17408
  1494
all theorems matching the pattern. Available in ProofGeneral under
wenzelm@17408
  1495
'ProofGeneral -> Find Theorems' or C-c C-f.  Example:
wenzelm@16234
  1496
wenzelm@17275
  1497
  C-c C-f (100) "(_::nat) + _ + _" intro -name: "HOL."
wenzelm@16234
  1498
wenzelm@16234
  1499
prints the last 100 theorems matching the pattern "(_::nat) + _ + _",
wenzelm@16234
  1500
matching the current goal as introduction rule and not having "HOL."
wenzelm@16234
  1501
in their name (i.e. not being defined in theory HOL).
wenzelm@16013
  1502
wenzelm@17408
  1503
* Command 'thms_containing' has been discontinued in favour of
wenzelm@17408
  1504
'find_theorems'; INCOMPATIBILITY.
wenzelm@17408
  1505
wenzelm@17385
  1506
* Communication with Proof General is now 8bit clean, which means that
wenzelm@17385
  1507
Unicode text in UTF-8 encoding may be used within theory texts (both
wenzelm@17408
  1508
formal and informal parts).  Cf. option -U of the Isabelle Proof
wenzelm@17538
  1509
General interface.  Here are some simple examples (cf. src/HOL/ex):
wenzelm@17538
  1510
wenzelm@17538
  1511
  http://isabelle.in.tum.de/library/HOL/ex/Hebrew.html
wenzelm@17538
  1512
  http://isabelle.in.tum.de/library/HOL/ex/Chinese.html
wenzelm@17385
  1513
wenzelm@17425
  1514
* Improved efficiency of the Simplifier and, to a lesser degree, the
wenzelm@17425
  1515
Classical Reasoner.  Typical big applications run around 2 times
wenzelm@17425
  1516
faster.
wenzelm@17425
  1517
wenzelm@15703
  1518
wenzelm@15703
  1519
*** Document preparation ***
wenzelm@15703
  1520
wenzelm@16234
  1521
* Commands 'display_drafts' and 'print_drafts' perform simple output
wenzelm@16234
  1522
of raw sources.  Only those symbols that do not require additional
wenzelm@16234
  1523
LaTeX packages (depending on comments in isabellesym.sty) are
wenzelm@16234
  1524
displayed properly, everything else is left verbatim.  isatool display
wenzelm@16234
  1525
and isatool print are used as front ends (these are subject to the
wenzelm@16234
  1526
DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively).
wenzelm@16234
  1527
wenzelm@17047
  1528
* Command tags control specific markup of certain regions of text,
wenzelm@17047
  1529
notably folding and hiding.  Predefined tags include "theory" (for
wenzelm@17047
  1530
theory begin and end), "proof" for proof commands, and "ML" for
wenzelm@17047
  1531
commands involving ML code; the additional tags "visible" and
wenzelm@17047
  1532
"invisible" are unused by default.  Users may give explicit tag
wenzelm@17047
  1533
specifications in the text, e.g. ''by %invisible (auto)''.  The
wenzelm@17047
  1534
interpretation of tags is determined by the LaTeX job during document
wenzelm@17047
  1535
preparation: see option -V of isatool usedir, or options -n and -t of
wenzelm@17047
  1536
isatool document, or even the LaTeX macros \isakeeptag, \isafoldtag,
wenzelm@17047
  1537
\isadroptag.
wenzelm@17047
  1538
wenzelm@17047
  1539
Several document versions may be produced at the same time via isatool
wenzelm@17047
  1540
usedir (the generated index.html will link all of them).  Typical
wenzelm@17047
  1541
specifications include ''-V document=theory,proof,ML'' to present
wenzelm@17047
  1542
theory/proof/ML parts faithfully, ''-V outline=/proof,/ML'' to fold
wenzelm@17047
  1543
proof and ML commands, and ''-V mutilated=-theory,-proof,-ML'' to omit
wenzelm@17047
  1544
these parts without any formal replacement text.  The Isabelle site
wenzelm@17047
  1545
default settings produce ''document'' and ''outline'' versions as
wenzelm@17047
  1546
specified above.
wenzelm@16234
  1547
haftmann@17402
  1548
* Several new antiquotations:
wenzelm@15979
  1549
wenzelm@15979
  1550
  @{term_type term} prints a term with its type annotated;
wenzelm@15979
  1551
wenzelm@15979
  1552
  @{typeof term} prints the type of a term;
wenzelm@15979
  1553
wenzelm@16234
  1554
  @{const const} is the same as @{term const}, but checks that the
wenzelm@16234
  1555
  argument is a known logical constant;
wenzelm@15979
  1556
wenzelm@15979
  1557
  @{term_style style term} and @{thm_style style thm} print a term or
wenzelm@16234
  1558
  theorem applying a "style" to it
wenzelm@16234
  1559
wenzelm@17117
  1560
  @{ML text}
wenzelm@17117
  1561
wenzelm@16234
  1562
Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of
wenzelm@16234
  1563
definitions, equations, inequations etc., 'concl' printing only the
schirmer@17393
  1564
conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem19'
wenzelm@16234
  1565
to print the specified premise.  TermStyle.add_style provides an ML
wenzelm@16234
  1566
interface for introducing further styles.  See also the "LaTeX Sugar"
wenzelm@17117
  1567
document practical applications.  The ML antiquotation prints
wenzelm@17117
  1568
type-checked ML expressions verbatim.
wenzelm@16234
  1569
wenzelm@17259
  1570
* Markup commands 'chapter', 'section', 'subsection', 'subsubsection',
wenzelm@17259
  1571
and 'text' support optional locale specification '(in loc)', which
wenzelm@17269
  1572
specifies the default context for interpreting antiquotations.  For
wenzelm@17269
  1573
example: 'text (in lattice) {* @{thm inf_assoc}*}'.
wenzelm@17259
  1574
wenzelm@17259
  1575
* Option 'locale=NAME' of antiquotations specifies an alternative
wenzelm@17259
  1576
context interpreting the subsequent argument.  For example: @{thm
wenzelm@17269
  1577
[locale=lattice] inf_assoc}.
wenzelm@17259
  1578
wenzelm@17097
  1579
* Proper output of proof terms (@{prf ...} and @{full_prf ...}) within
wenzelm@17097
  1580
a proof context.
wenzelm@17097
  1581
wenzelm@17097
  1582
* Proper output of antiquotations for theory commands involving a
wenzelm@17097
  1583
proof context (such as 'locale' or 'theorem (in loc) ...').
wenzelm@17097
  1584
wenzelm@17193
  1585
* Delimiters of outer tokens (string etc.) now produce separate LaTeX
wenzelm@17193
  1586
macros (\isachardoublequoteopen, isachardoublequoteclose etc.).
wenzelm@17193
  1587
wenzelm@17193
  1588
* isatool usedir: new option -C (default true) controls whether option
wenzelm@17193
  1589
-D should include a copy of the original document directory; -C false
wenzelm@17193
  1590
prevents unwanted effects such as copying of administrative CVS data.
wenzelm@17193
  1591
wenzelm@16234
  1592
wenzelm@16234
  1593
*** Pure ***
wenzelm@16234
  1594
wenzelm@16234
  1595
* Considerably improved version of 'constdefs' command.  Now performs
wenzelm@16234
  1596
automatic type-inference of declared constants; additional support for
wenzelm@16234
  1597
local structure declarations (cf. locales and HOL records), see also
wenzelm@16234
  1598
isar-ref manual.  Potential INCOMPATIBILITY: need to observe strictly
wenzelm@16234
  1599
sequential dependencies of definitions within a single 'constdefs'
wenzelm@16234
  1600
section; moreover, the declared name needs to be an identifier.  If
wenzelm@16234
  1601
all fails, consider to fall back on 'consts' and 'defs' separately.
wenzelm@16234
  1602
wenzelm@16234
  1603
* Improved indexed syntax and implicit structures.  First of all,
wenzelm@16234
  1604
indexed syntax provides a notational device for subscripted
wenzelm@16234
  1605
application, using the new syntax \<^bsub>term\<^esub> for arbitrary
wenzelm@16234
  1606
expressions.  Secondly, in a local context with structure
wenzelm@16234
  1607
declarations, number indexes \<^sub>n or the empty index (default
wenzelm@16234
  1608
number 1) refer to a certain fixed variable implicitly; option
wenzelm@16234
  1609
show_structs controls printing of implicit structures.  Typical
wenzelm@16234
  1610
applications of these concepts involve record types and locales.
wenzelm@16234
  1611
wenzelm@16234
  1612
* New command 'no_syntax' removes grammar declarations (and
wenzelm@16234
  1613
translations) resulting from the given syntax specification, which is
wenzelm@16234
  1614
interpreted in the same manner as for the 'syntax' command.
wenzelm@16234
  1615
wenzelm@16234
  1616
* 'Advanced' translation functions (parse_translation etc.) may depend
wenzelm@16234
  1617
on the signature of the theory context being presently used for
wenzelm@16234
  1618
parsing/printing, see also isar-ref manual.
wenzelm@16234
  1619
wenzelm@16856
  1620
* Improved 'oracle' command provides a type-safe interface to turn an
wenzelm@16856
  1621
ML expression of type theory -> T -> term into a primitive rule of
wenzelm@16856
  1622
type theory -> T -> thm (i.e. the functionality of Thm.invoke_oracle
wenzelm@16856
  1623
is already included here); see also FOL/ex/IffExample.thy;
wenzelm@16856
  1624
INCOMPATIBILITY.
wenzelm@16856
  1625
wenzelm@17275
  1626
* axclass: name space prefix for class "c" is now "c_class" (was "c"
wenzelm@17275
  1627
before); "cI" is no longer bound, use "c.intro" instead.
wenzelm@17275
  1628
INCOMPATIBILITY.  This change avoids clashes of fact bindings for
wenzelm@17275
  1629
axclasses vs. locales.
wenzelm@17275
  1630
wenzelm@16234
  1631
* Improved internal renaming of symbolic identifiers -- attach primes
wenzelm@16234
  1632
instead of base 26 numbers.
wenzelm@16234
  1633
wenzelm@16234
  1634
* New flag show_question_marks controls printing of leading question
wenzelm@16234
  1635
marks in schematic variable names.
wenzelm@16234
  1636
wenzelm@16234
  1637
* In schematic variable names, *any* symbol following \<^isub> or
wenzelm@16234
  1638
\<^isup> is now treated as part of the base name.  For example, the
wenzelm@16234
  1639
following works without printing of awkward ".0" indexes:
wenzelm@16234
  1640
wenzelm@16234
  1641
  lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1"
wenzelm@16234
  1642
    by simp
wenzelm@16234
  1643
wenzelm@16234
  1644
* Inner syntax includes (*(*nested*) comments*).
wenzelm@16234
  1645
wenzelm@17548
  1646
* Pretty printer now supports unbreakable blocks, specified in mixfix
wenzelm@16234
  1647
annotations as "(00...)".
wenzelm@16234
  1648
wenzelm@16234
  1649
* Clear separation of logical types and nonterminals, where the latter
wenzelm@16234
  1650
may only occur in 'syntax' specifications or type abbreviations.
wenzelm@16234
  1651
Before that distinction was only partially implemented via type class
wenzelm@16234
  1652
"logic" vs. "{}".  Potential INCOMPATIBILITY in rare cases of improper
wenzelm@16234
  1653
use of 'types'/'consts' instead of 'nonterminals'/'syntax'.  Some very
wenzelm@16234
  1654
exotic syntax specifications may require further adaption
wenzelm@17691
  1655
(e.g. Cube/Cube.thy).
wenzelm@16234
  1656
wenzelm@16234
  1657
* Removed obsolete type class "logic", use the top sort {} instead.
wenzelm@16234
  1658
Note that non-logical types should be declared as 'nonterminals'
wenzelm@16234
  1659
rather than 'types'.  INCOMPATIBILITY for new object-logic
wenzelm@16234
  1660
specifications.
wenzelm@16234
  1661
ballarin@17095
  1662
* Attributes 'induct' and 'cases': type or set names may now be
ballarin@17095
  1663
locally fixed variables as well.
ballarin@17095
  1664
wenzelm@16234
  1665
* Simplifier: can now control the depth to which conditional rewriting
wenzelm@16234
  1666
is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth
wenzelm@16234
  1667
Limit.
wenzelm@16234
  1668
wenzelm@16234
  1669
* Simplifier: simplification procedures may now take the current
wenzelm@16234
  1670
simpset into account (cf. Simplifier.simproc(_i) / mk_simproc
wenzelm@16234
  1671
interface), which is very useful for calling the Simplifier
wenzelm@16234
  1672
recursively.  Minor INCOMPATIBILITY: the 'prems' argument of simprocs
wenzelm@16234
  1673
is gone -- use prems_of_ss on the simpset instead.  Moreover, the
wenzelm@16234
  1674
low-level mk_simproc no longer applies Logic.varify internally, to
wenzelm@16234
  1675
allow for use in a context of fixed variables.
wenzelm@16234
  1676
wenzelm@16234
  1677
* thin_tac now works even if the assumption being deleted contains !!
wenzelm@16234
  1678
or ==>.  More generally, erule now works even if the major premise of
wenzelm@16234
  1679
the elimination rule contains !! or ==>.
wenzelm@16234
  1680
wenzelm@17597
  1681
* Method 'rules' has been renamed to 'iprover'. INCOMPATIBILITY.
nipkow@17590
  1682
wenzelm@16234
  1683
* Reorganized bootstrapping of the Pure theories; CPure is now derived
wenzelm@16234
  1684
from Pure, which contains all common declarations already.  Both
wenzelm@16234
  1685
theories are defined via plain Isabelle/Isar .thy files.
wenzelm@16234
  1686
INCOMPATIBILITY: elements of CPure (such as the CPure.intro /
wenzelm@16234
  1687
CPure.elim / CPure.dest attributes) now appear in the Pure name space;
wenzelm@16234
  1688
use isatool fixcpure to adapt your theory and ML sources.
wenzelm@16234
  1689
wenzelm@16234
  1690
* New syntax 'name(i-j, i-, i, ...)' for referring to specific
wenzelm@16234
  1691
selections of theorems in named facts via index ranges.
wenzelm@16234
  1692
wenzelm@17097
  1693
* 'print_theorems': in theory mode, really print the difference
wenzelm@17097
  1694
wrt. the last state (works for interactive theory development only),
wenzelm@17097
  1695
in proof mode print all local facts (cf. 'print_facts');
wenzelm@17097
  1696
wenzelm@17397
  1697
* 'hide': option '(open)' hides only base names.
wenzelm@17397
  1698
wenzelm@17275
  1699
* More efficient treatment of intermediate checkpoints in interactive
wenzelm@17275
  1700
theory development.
wenzelm@17275
  1701
berghofe@17663
  1702
* Code generator is now invoked via code_module (incremental code
wenzelm@17664
  1703
generation) and code_library (modular code generation, ML structures
wenzelm@17664
  1704
for each theory).  INCOMPATIBILITY: new keywords 'file' and 'contains'
wenzelm@17664
  1705
must be quoted when used as identifiers.
wenzelm@17664
  1706
wenzelm@17664
  1707
* New 'value' command for reading, evaluating and printing terms using
wenzelm@17664
  1708
the code generator.  INCOMPATIBILITY: command keyword 'value' must be
wenzelm@17664
  1709
quoted when used as identifier.
berghofe@17663
  1710
wenzelm@16234
  1711
wenzelm@16234
  1712
*** Locales ***
ballarin@17095
  1713
wenzelm@17385
  1714
* New commands for the interpretation of locale expressions in
wenzelm@17385
  1715
theories (1), locales (2) and proof contexts (3).  These generate
wenzelm@17385
  1716
proof obligations from the expression specification.  After the
wenzelm@17385
  1717
obligations have been discharged, theorems of the expression are added
wenzelm@17385
  1718
to the theory, target locale or proof context.  The synopsis of the
wenzelm@17385
  1719
commands is a follows:
wenzelm@17385
  1720
ballarin@17095
  1721
  (1) interpretation expr inst
ballarin@17095
  1722
  (2) interpretation target < expr
ballarin@17095
  1723
  (3) interpret expr inst
wenzelm@17385
  1724
ballarin@17095
  1725
Interpretation in theories and proof contexts require a parameter
ballarin@17095
  1726
instantiation of terms from the current context.  This is applied to
wenzelm@17385
  1727
specifications and theorems of the interpreted expression.
wenzelm@17385
  1728
Interpretation in locales only permits parameter renaming through the
wenzelm@17385
  1729
locale expression.  Interpretation is smart in that interpretations
wenzelm@17385
  1730
that are active already do not occur in proof obligations, neither are
wenzelm@17385
  1731
instantiated theorems stored in duplicate.  Use 'print_interps' to
wenzelm@17385
  1732
inspect active interpretations of a particular locale.  For details,
ballarin@17436
  1733
see the Isar Reference manual.  Examples can be found in
ballarin@17436
  1734
HOL/Finite_Set.thy and HOL/Algebra/UnivPoly.thy.
wenzelm@16234
  1735
wenzelm@16234
  1736
INCOMPATIBILITY: former 'instantiate' has been withdrawn, use
wenzelm@16234
  1737
'interpret' instead.
wenzelm@16234
  1738
wenzelm@17385
  1739
* New context element 'constrains' for adding type constraints to
wenzelm@17385
  1740
parameters.
wenzelm@17385
  1741
wenzelm@17385
  1742
* Context expressions: renaming of parameters with syntax
wenzelm@17385
  1743
redeclaration.
ballarin@17095
  1744
ballarin@17095
  1745
* Locale declaration: 'includes' disallowed.
ballarin@17095
  1746
wenzelm@16234
  1747
* Proper static binding of attribute syntax -- i.e. types / terms /
wenzelm@16234
  1748
facts mentioned as arguments are always those of the locale definition
wenzelm@16234
  1749
context, independently of the context of later invocations.  Moreover,
wenzelm@16234
  1750
locale operations (renaming and type / term instantiation) are applied
wenzelm@16234
  1751
to attribute arguments as expected.
wenzelm@16234
  1752
wenzelm@16234
  1753
INCOMPATIBILITY of the ML interface: always pass Attrib.src instead of
wenzelm@16234
  1754
actual attributes; rare situations may require Attrib.attribute to
wenzelm@16234
  1755
embed those attributes into Attrib.src that lack concrete syntax.
wenzelm@16234
  1756
Attribute implementations need to cooperate properly with the static
wenzelm@16234
  1757
binding mechanism.  Basic parsers Args.XXX_typ/term/prop and
wenzelm@16234
  1758
Attrib.XXX_thm etc. already do the right thing without further
wenzelm@16234
  1759
intervention.  Only unusual applications -- such as "where" or "of"
wenzelm@16234
  1760
(cf. src/Pure/Isar/attrib.ML), which process arguments depending both
wenzelm@16234
  1761
on the context and the facts involved -- may have to assign parsed
wenzelm@16234
  1762
values to argument tokens explicitly.
wenzelm@16234
  1763
wenzelm@16234
  1764
* Changed parameter management in theorem generation for long goal
wenzelm@16234
  1765
statements with 'includes'.  INCOMPATIBILITY: produces a different
wenzelm@16234
  1766
theorem statement in rare situations.
wenzelm@16234
  1767
ballarin@17228
  1768
* Locale inspection command 'print_locale' omits notes elements.  Use
ballarin@17228
  1769
'print_locale!' to have them included in the output.
ballarin@17228
  1770
wenzelm@16234
  1771
wenzelm@16234
  1772
*** Provers ***
wenzelm@16234
  1773
wenzelm@16234
  1774
* Provers/hypsubst.ML: improved version of the subst method, for
wenzelm@16234
  1775
single-step rewriting: it now works in bound variable contexts. New is
wenzelm@16234
  1776
'subst (asm)', for rewriting an assumption.  INCOMPATIBILITY: may
wenzelm@16234
  1777
rewrite a different subterm than the original subst method, which is
wenzelm@16234
  1778
still available as 'simplesubst'.
wenzelm@16234
  1779
wenzelm@16234
  1780
* Provers/quasi.ML: new transitivity reasoners for transitivity only
wenzelm@16234
  1781
and quasi orders.
wenzelm@16234
  1782
wenzelm@16234
  1783
* Provers/trancl.ML: new transitivity reasoner for transitive and
wenzelm@16234
  1784
reflexive-transitive closure of relations.
wenzelm@16234
  1785
wenzelm@16234
  1786
* Provers/blast.ML: new reference depth_limit to make blast's depth
wenzelm@16234
  1787
limit (previously hard-coded with a value of 20) user-definable.
wenzelm@16234
  1788
wenzelm@16234
  1789
* Provers/simplifier.ML has been moved to Pure, where Simplifier.setup
wenzelm@16234
  1790
is peformed already.  Object-logics merely need to finish their
wenzelm@16234
  1791
initial simpset configuration as before.  INCOMPATIBILITY.
wenzelm@15703
  1792
berghofe@15475
  1793
schirmer@14700
  1794
*** HOL ***
schirmer@14700
  1795
wenzelm@16234
  1796
* Symbolic syntax of Hilbert Choice Operator is now as follows:
wenzelm@14878
  1797
wenzelm@14878
  1798
  syntax (epsilon)
wenzelm@14878
  1799
    "_Eps" :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
wenzelm@14878
  1800
wenzelm@16234
  1801
The symbol \<some> is displayed as the alternative epsilon of LaTeX
wenzelm@16234
  1802
and x-symbol; use option '-m epsilon' to get it actually printed.
wenzelm@16234
  1803
Moreover, the mathematically important symbolic identifier \<epsilon>
wenzelm@16234
  1804
becomes available as variable, constant etc.  INCOMPATIBILITY,
wenzelm@16234
  1805
wenzelm@16234
  1806
* "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
wenzelm@16234
  1807
Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=
wenzelm@17371
  1808
is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to
avigad@17016
  1809
support corresponding Isar calculations.
wenzelm@16234
  1810
wenzelm@16234
  1811
* "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>"
wenzelm@16234
  1812
instead of ":".
wenzelm@16234
  1813
wenzelm@16234
  1814
* theory SetInterval: changed the syntax for open intervals:
wenzelm@16234
  1815
wenzelm@16234
  1816
  Old       New
wenzelm@16234
  1817
  {..n(}    {..<n}
wenzelm@16234
  1818
  {)n..}    {n<..}
wenzelm@16234
  1819
  {m..n(}   {m..<n}
wenzelm@16234
  1820
  {)m..n}   {m<..n}
wenzelm@16234
  1821
  {)m..n(}  {m<..<n}
wenzelm@16234
  1822
wenzelm@16234
  1823
The old syntax is still supported but will disappear in the next
wenzelm@16234
  1824
release.  For conversion use the following Emacs search and replace
wenzelm@16234
  1825
patterns (these are not perfect but work quite well):
nipkow@15046
  1826
nipkow@15046
  1827
  {)\([^\.]*\)\.\.  ->  {\1<\.\.}
nipkow@15046
  1828
  \.\.\([^(}]*\)(}  ->  \.\.<\1}
nipkow@15046
  1829
wenzelm@17533
  1830
* Theory Commutative_Ring (in Library): method comm_ring for proving
wenzelm@17533
  1831
equalities in commutative rings; method 'algebra' provides a generic
wenzelm@17533
  1832
interface.
wenzelm@17389
  1833
wenzelm@17389
  1834
* Theory Finite_Set: changed the syntax for 'setsum', summation over
wenzelm@16234
  1835
finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is
wenzelm@17371
  1836
now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can
paulson@17189
  1837
be a tuple pattern.
wenzelm@16234
  1838
wenzelm@16234
  1839
Some new syntax forms are available:
wenzelm@16234
  1840
wenzelm@16234
  1841
  "\<Sum>x | P. e"      for     "setsum (%x. e) {x. P}"
wenzelm@16234
  1842
  "\<Sum>x = a..b. e"   for     "setsum (%x. e) {a..b}"
wenzelm@16234
  1843
  "\<Sum>x = a..<b. e"  for     "setsum (%x. e) {a..<b}"
wenzelm@16234
  1844
  "\<Sum>x < k. e"      for     "setsum (%x. e) {..<k}"
wenzelm@16234
  1845
wenzelm@16234
  1846
The latter form "\<Sum>x < k. e" used to be based on a separate
wenzelm@16234
  1847
function "Summation", which has been discontinued.
wenzelm@16234
  1848
wenzelm@16234
  1849
* theory Finite_Set: in structured induction proofs, the insert case
wenzelm@16234
  1850
is now 'case (insert x F)' instead of the old counterintuitive 'case
wenzelm@16234
  1851
(insert F x)'.
wenzelm@16234
  1852
wenzelm@16234
  1853
* The 'refute' command has been extended to support a much larger
wenzelm@16234
  1854
fragment of HOL, including axiomatic type classes, constdefs and
wenzelm@16234
  1855
typedefs, inductive datatypes and recursion.
wenzelm@16234
  1856
webertj@17700
  1857
* New tactics 'sat' and 'satx' to prove propositional tautologies.
webertj@17700
  1858
Requires zChaff with proof generation to be installed.  See
webertj@17700
  1859
HOL/ex/SAT_Examples.thy for examples.
webertj@17619
  1860
wenzelm@16234
  1861
* Datatype induction via method 'induct' now preserves the name of the
wenzelm@16234
  1862
induction variable. For example, when proving P(xs::'a list) by
wenzelm@16234
  1863
induction on xs, the induction step is now P(xs) ==> P(a#xs) rather
wenzelm@16234
  1864
than P(list) ==> P(a#list) as previously.  Potential INCOMPATIBILITY
wenzelm@16234
  1865
in unstructured proof scripts.
wenzelm@16234
  1866
wenzelm@16234
  1867
* Reworked implementation of records.  Improved scalability for
wenzelm@16234
  1868
records with many fields, avoiding performance problems for type
wenzelm@16234
  1869
inference. Records are no longer composed of nested field types, but
wenzelm@16234
  1870
of nested extension types. Therefore the record type only grows linear
wenzelm@16234
  1871
in the number of extensions and not in the number of fields.  The
wenzelm@16234
  1872
top-level (users) view on records is preserved.  Potential
wenzelm@16234
  1873
INCOMPATIBILITY only in strange cases, where the theory depends on the
wenzelm@16234
  1874
old record representation. The type generated for a record is called
wenzelm@16234
  1875
<record_name>_ext_type.
wenzelm@16234
  1876
wenzelm@16234
  1877
Flag record_quick_and_dirty_sensitive can be enabled to skip the
wenzelm@16234
  1878
proofs triggered by a record definition or a simproc (if
wenzelm@16234
  1879
quick_and_dirty is enabled).  Definitions of large records can take
wenzelm@16234
  1880
quite long.
wenzelm@16234
  1881
wenzelm@16234
  1882
New simproc record_upd_simproc for simplification of multiple record
wenzelm@16234
  1883
updates enabled by default.  Moreover, trivial updates are also
wenzelm@16234
  1884
removed: r(|x := x r|) = r.  INCOMPATIBILITY: old proofs break
wenzelm@16234
  1885
occasionally, since simplification is more powerful by default.
wenzelm@16234
  1886
wenzelm@17275
  1887
* typedef: proper support for polymorphic sets, which contain extra
wenzelm@17275
  1888
type-variables in the term.
wenzelm@17275
  1889
wenzelm@16234
  1890
* Simplifier: automatically reasons about transitivity chains
wenzelm@16234
  1891
involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics
wenzelm@16234
  1892
provided by Provers/trancl.ML as additional solvers.  INCOMPATIBILITY:
wenzelm@16234
  1893
old proofs break occasionally as simplification may now solve more
wenzelm@16234
  1894
goals than previously.
wenzelm@16234
  1895
wenzelm@16234
  1896
* Simplifier: converts x <= y into x = y if assumption y <= x is
wenzelm@16234
  1897
present.  Works for all partial orders (class "order"), in particular
wenzelm@16234
  1898
numbers and sets.  For linear orders (e.g. numbers) it treats ~ x < y
wenzelm@16234
  1899
just like y <= x.
wenzelm@16234
  1900
wenzelm@16234
  1901
* Simplifier: new simproc for "let x = a in f x".  If a is a free or
wenzelm@16234
  1902
bound variable or a constant then the let is unfolded.  Otherwise
wenzelm@16234
  1903
first a is simplified to b, and then f b is simplified to g. If
wenzelm@16234
  1904
possible we abstract b from g arriving at "let x = b in h x",
wenzelm@16234
  1905
otherwise we unfold the let and arrive at g.  The simproc can be
wenzelm@16234
  1906
enabled/disabled by the reference use_let_simproc.  Potential
wenzelm@16234
  1907
INCOMPATIBILITY since simplification is more powerful by default.
webertj@15776
  1908
paulson@16563
  1909
* Classical reasoning: the meson method now accepts theorems as arguments.
paulson@16563
  1910
paulson@17595
  1911
* Prover support: pre-release of the Isabelle-ATP linkup, which runs background
paulson@17595
  1912
jobs to provide advice on the provability of subgoals.
paulson@17595
  1913
wenzelm@16891
  1914
* Theory OrderedGroup and Ring_and_Field: various additions and
wenzelm@16891
  1915
improvements to faciliate calculations involving equalities and
wenzelm@16891
  1916
inequalities.
wenzelm@16891
  1917
wenzelm@16891
  1918
The following theorems have been eliminated or modified
wenzelm@16891
  1919
(INCOMPATIBILITY):
avigad@16888
  1920
avigad@16888
  1921
  abs_eq             now named abs_of_nonneg
wenzelm@17371
  1922
  abs_of_ge_0        now named abs_of_nonneg
wenzelm@17371
  1923
  abs_minus_eq       now named abs_of_nonpos
avigad@16888
  1924
  imp_abs_id         now named abs_of_nonneg
avigad@16888
  1925
  imp_abs_neg_id     now named abs_of_nonpos
avigad@16888
  1926
  mult_pos           now named mult_pos_pos
avigad@16888
  1927
  mult_pos_le        now named mult_nonneg_nonneg
avigad@16888
  1928
  mult_pos_neg_le    now named mult_nonneg_nonpos
avigad@16888
  1929
  mult_pos_neg2_le   now named mult_nonneg_nonpos2
avigad@16888
  1930
  mult_neg           now named mult_neg_neg
avigad@16888
  1931
  mult_neg_le        now named mult_nonpos_nonpos
avigad@16888
  1932
obua@23495
  1933
* The following lemmas in Ring_and_Field have been added to the simplifier:
obua@23495
  1934
     
obua@23495
  1935
     zero_le_square
obua@23495
  1936
     not_square_less_zero 
obua@23495
  1937
obua@23495
  1938
  The following lemmas have been deleted from Real/RealPow:
obua@23495
  1939
  
obua@23495
  1940
     realpow_zero_zero
obua@23495
  1941
     realpow_two
obua@23495
  1942
     realpow_less
obua@23495
  1943
     zero_le_power
obua@23495
  1944
     realpow_two_le
obua@23495
  1945
     abs_realpow_two
obua@23495
  1946
     realpow_two_abs     
obua@23495
  1947
wenzelm@16891
  1948
* Theory Parity: added rules for simplifying exponents.
wenzelm@16891
  1949
nipkow@17092
  1950
* Theory List:
nipkow@17092
  1951
nipkow@17092
  1952
The following theorems have been eliminated or modified
nipkow@17092
  1953
(INCOMPATIBILITY):
nipkow@17092
  1954
nipkow@17092
  1955
  list_all_Nil       now named list_all.simps(1)
nipkow@17092
  1956
  list_all_Cons      now named list_all.simps(2)
nipkow@17092
  1957
  list_all_conv      now named list_all_iff
nipkow@17092
  1958
  set_mem_eq         now named mem_iff
nipkow@17092
  1959
wenzelm@16929
  1960
* Theories SetsAndFunctions and BigO (see HOL/Library) support
wenzelm@16929
  1961
asymptotic "big O" calculations.  See the notes in BigO.thy.
wenzelm@16929
  1962
avigad@16888
  1963
avigad@16888
  1964
*** HOL-Complex ***
avigad@16888
  1965
wenzelm@16891
  1966
* Theory RealDef: better support for embedding natural numbers and
wenzelm@16891
  1967
integers in the reals.
wenzelm@16891
  1968
wenzelm@16891
  1969
The following theorems have been eliminated or modified
wenzelm@16891
  1970
(INCOMPATIBILITY):
wenzelm@16891
  1971
avigad@17016
  1972
  exp_ge_add_one_self  now requires no hypotheses
avigad@17016
  1973
  real_of_int_add      reversed direction of equality (use [symmetric])
avigad@17016
  1974
  real_of_int_minus    reversed direction of equality (use [symmetric])
avigad@17016
  1975
  real_of_int_diff     reversed direction of equality (use [symmetric])
avigad@17016
  1976
  real_of_int_mult     reversed direction of equality (use [symmetric])
wenzelm@16891
  1977
wenzelm@16891
  1978
* Theory RComplete: expanded support for floor and ceiling functions.
avigad@16888
  1979
avigad@16962
  1980
* Theory Ln is new, with properties of the natural logarithm
avigad@16962
  1981
wenzelm@17423
  1982
* Hyperreal: There is a new type constructor "star" for making
wenzelm@17423
  1983
nonstandard types.  The old type names are now type synonyms:
wenzelm@17423
  1984
wenzelm@17423
  1985
  hypreal = real star
wenzelm@17423
  1986
  hypnat = nat star
wenzelm@17423
  1987
  hcomplex = complex star
wenzelm@17423
  1988
wenzelm@17423
  1989
* Hyperreal: Many groups of similarly-defined constants have been
huffman@17442
  1990
replaced by polymorphic versions (INCOMPATIBILITY):
wenzelm@17423
  1991
wenzelm@17423
  1992
  star_of <-- hypreal_of_real, hypnat_of_nat, hcomplex_of_complex
wenzelm@17423
  1993
wenzelm@17423
  1994
  starset      <-- starsetNat, starsetC
wenzelm@17423
  1995
  *s*          <-- *sNat*, *sc*
wenzelm@17423
  1996
  starset_n    <-- starsetNat_n, starsetC_n
wenzelm@17423
  1997
  *sn*         <-- *sNatn*, *scn*
wenzelm@17423
  1998
  InternalSets <-- InternalNatSets, InternalCSets
wenzelm@17423
  1999
huffman@17442
  2000
  starfun      <-- starfun{Nat,Nat2,C,RC,CR}
wenzelm@17423
  2001
  *f*          <-- *fNat*, *fNat2*, *fc*, *fRc*, *fcR*
huffman@17442
  2002
  starfun_n    <-- starfun{Nat,Nat2,C,RC,CR}_n
wenzelm@17423
  2003
  *fn*         <-- *fNatn*, *fNat2n*, *fcn*, *fRcn*, *fcRn*
huffman@17442
  2004
  InternalFuns <-- InternalNatFuns, InternalNatFuns2, Internal{C,RC,CR}Funs
wenzelm@17423
  2005
wenzelm@17423
  2006
* Hyperreal: Many type-specific theorems have been removed in favor of
huffman@17442
  2007
theorems specific to various axiomatic type classes (INCOMPATIBILITY):
huffman@17442
  2008
huffman@17442
  2009
  add_commute <-- {hypreal,hypnat,hcomplex}_add_commute
huffman@17442
  2010
  add_assoc   <-- {hypreal,hypnat,hcomplex}_add_assocs
huffman@17442
  2011
  OrderedGroup.add_0 <-- {hypreal,hypnat,hcomplex}_add_zero_left
huffman@17442
  2012
  OrderedGroup.add_0_right <-- {hypreal,hcomplex}_add_zero_right
wenzelm@17423
  2013
  right_minus <-- hypreal_add_minus
huffman@17442
  2014
  left_minus <-- {hypreal,hcomplex}_add_minus_left
huffman@17442
  2015
  mult_commute <-- {hypreal,hypnat,hcomplex}_mult_commute
huffman@17442
  2016
  mult_assoc <-- {hypreal,hypnat,hcomplex}_mult_assoc
huffman@17442
  2017
  mult_1_left <-- {hypreal,hypnat}_mult_1, hcomplex_mult_one_left
wenzelm@17423
  2018
  mult_1_right <-- hcomplex_mult_one_right
wenzelm@17423
  2019
  mult_zero_left <-- hcomplex_mult_zero_left
huffman@17442
  2020
  left_distrib <-- {hypreal,hypnat,hcomplex}_add_mult_distrib
wenzelm@17423
  2021
  right_distrib <-- hypnat_add_mult_distrib2
huffman@17442
  2022
  zero_neq_one <-- {hypreal,hypnat,hcomplex}_zero_not_eq_one
wenzelm@17423
  2023
  right_inverse <-- hypreal_mult_inverse
wenzelm@17423
  2024
  left_inverse <-- hypreal_mult_inverse_left, hcomplex_mult_inv_left
huffman@17442
  2025
  order_refl <-- {hypreal,hypnat}_le_refl
huffman@17442
  2026
  order_trans <-- {hypreal,hypnat}_le_trans
huffman@17442
  2027
  order_antisym <-- {hypreal,hypnat}_le_anti_sym
huffman@17442
  2028
  order_less_le <-- {hypreal,hypnat}_less_le
huffman@17442
  2029
  linorder_linear <-- {hypreal,hypnat}_le_linear
huffman@17442
  2030
  add_left_mono <-- {hypreal,hypnat}_add_left_mono
huffman@17442
  2031
  mult_strict_left_mono <-- {hypreal,hypnat}_mult_less_mono2
wenzelm@17423
  2032
  add_nonneg_nonneg <-- hypreal_le_add_order
wenzelm@17423
  2033
wenzelm@17423
  2034
* Hyperreal: Separate theorems having to do with type-specific
wenzelm@17423
  2035
versions of constants have been merged into theorems that apply to the
huffman@17442
  2036
new polymorphic constants (INCOMPATIBILITY):
huffman@17442
  2037
huffman@17442
  2038
  STAR_UNIV_set <-- {STAR_real,NatStar_real,STARC_complex}_set
huffman@17442
  2039
  STAR_empty_set <-- {STAR,NatStar,STARC}_empty_set
huffman@17442
  2040
  STAR_Un <-- {STAR,NatStar,STARC}_Un
huffman@17442
  2041
  STAR_Int <-- {STAR,NatStar,STARC}_Int
huffman@17442
  2042
  STAR_Compl <-- {STAR,NatStar,STARC}_Compl
huffman@17442
  2043
  STAR_subset <-- {STAR,NatStar,STARC}_subset
huffman@17442
  2044
  STAR_mem <-- {STAR,NatStar,STARC}_mem
huffman@17442
  2045
  STAR_mem_Compl <-- {STAR,STARC}_mem_Compl
huffman@17442
  2046
  STAR_diff <-- {STAR,STARC}_diff
huffman@17442
  2047
  STAR_star_of_image_subset <-- {STAR_hypreal_of_real, NatStar_hypreal_of_real,
huffman@17442
  2048
    STARC_hcomplex_of_complex}_image_subset
huffman@17442
  2049
  starset_n_Un <-- starset{Nat,C}_n_Un
huffman@17442
  2050
  starset_n_Int <-- starset{Nat,C}_n_Int
huffman@17442
  2051
  starset_n_Compl <-- starset{Nat,C}_n_Compl
huffman@17442
  2052
  starset_n_diff <-- starset{Nat,C}_n_diff
huffman@17442
  2053
  InternalSets_Un <-- Internal{Nat,C}Sets_Un
huffman@17442
  2054
  InternalSets_Int <-- Internal{Nat,C}Sets_Int
huffman@17442
  2055
  InternalSets_Compl <-- Internal{Nat,C}Sets_Compl
huffman@17442
  2056
  InternalSets_diff <-- Internal{Nat,C}Sets_diff
huffman@17442
  2057
  InternalSets_UNIV_diff <-- Internal{Nat,C}Sets_UNIV_diff
huffman@17442
  2058
  InternalSets_starset_n <-- Internal{Nat,C}Sets_starset{Nat,C}_n
huffman@17442
  2059
  starset_starset_n_eq <-- starset{Nat,C}_starset{Nat,C}_n_eq
huffman@17442
  2060
  starset_n_starset <-- starset{Nat,C}_n_starset{Nat,C}
huffman@17442
  2061
  starfun_n_starfun <-- starfun{Nat,Nat2,C,RC,CR}_n_starfun{Nat,Nat2,C,RC,CR}
huffman@17442
  2062
  starfun <-- starfun{Nat,Nat2,C,RC,CR}
huffman@17442
  2063
  starfun_mult <-- starfun{Nat,Nat2,C,RC,CR}_mult
huffman@17442
  2064
  starfun_add <-- starfun{Nat,Nat2,C,RC,CR}_add
huffman@17442
  2065
  starfun_minus <-- starfun{Nat,Nat2,C,RC,CR}_minus
huffman@17442
  2066
  starfun_diff <-- starfun{C,RC,CR}_diff
huffman@17442
  2067
  starfun_o <-- starfun{NatNat2,Nat2,_stafunNat,C,C_starfunRC,_starfunCR}_o
huffman@17442
  2068
  starfun_o2 <-- starfun{NatNat2,_stafunNat,C,C_starfunRC,_starfunCR}_o2
huffman@17442
  2069
  starfun_const_fun <-- starfun{Nat,Nat2,C,RC,CR}_const_fun
huffman@17442
  2070
  starfun_inverse <-- starfun{Nat,C,RC,CR}_inverse
huffman@17442
  2071
  starfun_eq <-- starfun{Nat,Nat2,C,RC,CR}_eq
huffman@17442
  2072
  starfun_eq_iff <-- starfun{C,RC,CR}_eq_iff
wenzelm@17423
  2073
  starfun_Id <-- starfunC_Id
huffman@17442
  2074
  starfun_approx <-- starfun{Nat,CR}_approx
huffman@17442
  2075
  starfun_capprox <-- starfun{C,RC}_capprox
wenzelm@17423
  2076
  starfun_abs <-- starfunNat_rabs
huffman@17442
  2077
  starfun_lambda_cancel <-- starfun{C,CR,RC}_lambda_cancel
huffman@17442
  2078
  starfun_lambda_cancel2 <-- starfun{C,CR,RC}_lambda_cancel2
wenzelm@17423
  2079
  starfun_mult_HFinite_approx <-- starfunCR_mult_HFinite_capprox
huffman@17442
  2080
  starfun_mult_CFinite_capprox <-- starfun{C,RC}_mult_CFinite_capprox
huffman@17442
  2081
  starfun_add_capprox <-- starfun{C,RC}_add_capprox
wenzelm@17423
  2082
  starfun_add_approx <-- starfunCR_add_approx
wenzelm@17423
  2083
  starfun_inverse_inverse <-- starfunC_inverse_inverse
huffman@17442
  2084
  starfun_divide <-- starfun{C,CR,RC}_divide
huffman@17442
  2085
  starfun_n <-- starfun{Nat,C}_n
huffman@17442
  2086
  starfun_n_mult <-- starfun{Nat,C}_n_mult
huffman@17442
  2087
  starfun_n_add <-- starfun{Nat,C}_n_add
wenzelm@17423
  2088
  starfun_n_add_minus <-- starfunNat_n_add_minus
huffman@17442
  2089
  starfun_n_const_fun <-- starfun{Nat,C}_n_const_fun
huffman@17442
  2090
  starfun_n_minus <-- starfun{Nat,C}_n_minus
huffman@17442
  2091
  starfun_n_eq <-- starfun{Nat,C}_n_eq
huffman@17442
  2092
huffman@17442
  2093
  star_n_add <-- {hypreal,hypnat,hcomplex}_add
huffman@17442
  2094
  star_n_minus <-- {hypreal,hcomplex}_minus
huffman@17442
  2095
  star_n_diff <-- {hypreal,hcomplex}_diff
huffman@17442
  2096
  star_n_mult <-- {hypreal,hcomplex}_mult
huffman@17442
  2097
  star_n_inverse <-- {hypreal,hcomplex}_inverse
huffman@17442
  2098
  star_n_le <-- {hypreal,hypnat}_le
huffman@17442
  2099
  star_n_less <-- {hypreal,hypnat}_less
huffman@17442
  2100
  star_n_zero_num <-- {hypreal,hypnat,hcomplex}_zero_num
huffman@17442
  2101
  star_n_one_num <-- {hypreal,hypnat,hcomplex}_one_num
wenzelm@17423
  2102
  star_n_abs <-- hypreal_hrabs
wenzelm@17423
  2103
  star_n_divide <-- hcomplex_divide
wenzelm@17423
  2104
huffman@17442
  2105
  star_of_add <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_add
huffman@17442
  2106
  star_of_minus <-- {hypreal_of_real,hcomplex_of_complex}_minus
wenzelm@17423
  2107
  star_of_diff <-- hypreal_of_real_diff
huffman@17442
  2108
  star_of_mult <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_mult
huffman@17442
  2109
  star_of_one <-- {hypreal_of_real,hcomplex_of_complex}_one
huffman@17442
  2110
  star_of_zero <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_zero
huffman@17442
  2111
  star_of_le <-- {hypreal_of_real,hypnat_of_nat}_le_iff
huffman@17442
  2112
  star_of_less <-- {hypreal_of_real,hypnat_of_nat}_less_iff
huffman@17442
  2113
  star_of_eq <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_eq_iff
huffman@17442
  2114
  star_of_inverse <-- {hypreal_of_real,hcomplex_of_complex}_inverse
huffman@17442
  2115
  star_of_divide <-- {hypreal_of_real,hcomplex_of_complex}_divide
huffman@17442
  2116
  star_of_of_nat <-- {hypreal_of_real,hcomplex_of_complex}_of_nat
huffman@17442
  2117
  star_of_of_int <-- {hypreal_of_real,hcomplex_of_complex}_of_int
huffman@17442
  2118
  star_of_number_of <-- {hypreal,hcomplex}_number_of
wenzelm@17423
  2119
  star_of_number_less <-- number_of_less_hypreal_of_real_iff
wenzelm@17423
  2120
  star_of_number_le <-- number_of_le_hypreal_of_real_iff
wenzelm@17423
  2121
  star_of_eq_number <-- hypreal_of_real_eq_number_of_iff
wenzelm@17423
  2122
  star_of_less_number <-- hypreal_of_real_less_number_of_iff
wenzelm@17423
  2123
  star_of_le_number <-- hypreal_of_real_le_number_of_iff
wenzelm@17423
  2124
  star_of_power <-- hypreal_of_real_power
wenzelm@17423
  2125
  star_of_eq_0 <-- hcomplex_of_complex_zero_iff
wenzelm@17423
  2126
huffman@17442
  2127
* Hyperreal: new method "transfer" that implements the transfer
huffman@17442
  2128
principle of nonstandard analysis. With a subgoal that mentions
huffman@17442
  2129
nonstandard types like "'a star", the command "apply transfer"
huffman@17442
  2130
replaces it with an equivalent one that mentions only standard types.
huffman@17442
  2131
To be successful, all free variables must have standard types; non-
huffman@17442
  2132
standard variables must have explicit universal quantifiers.
huffman@17442
  2133
wenzelm@17641
  2134
* Hyperreal: A theory of Taylor series.
wenzelm@17641
  2135
wenzelm@14655
  2136
wenzelm@14682
  2137
*** HOLCF ***
wenzelm@14682
  2138
wenzelm@17533
  2139
* Discontinued special version of 'constdefs' (which used to support
wenzelm@17533
  2140
continuous functions) in favor of the general Pure one with full
wenzelm@17533
  2141
type-inference.
wenzelm@17533
  2142
wenzelm@17533
  2143
* New simplification procedure for solving continuity conditions; it
wenzelm@17533
  2144
is much faster on terms with many nested lambda abstractions (cubic
huffman@17442
  2145
instead of exponential time).
huffman@17442
  2146
wenzelm@17533
  2147
* New syntax for domain package: selector names are now optional.
huffman@17442
  2148
Parentheses should be omitted unless argument is lazy, for example:
huffman@17442
  2149
huffman@17442
  2150
  domain 'a stream = cons "'a" (lazy "'a stream")
huffman@17442
  2151
wenzelm@17533
  2152
* New command 'fixrec' for defining recursive functions with pattern
wenzelm@17533
  2153
matching; defining multiple functions with mutual recursion is also
wenzelm@17533
  2154
supported.  Patterns may include the constants cpair, spair, up, sinl,
wenzelm@17533
  2155
sinr, or any data constructor defined by the domain package. The given
wenzelm@17533
  2156
equations are proven as rewrite rules. See HOLCF/ex/Fixrec_ex.thy for
wenzelm@17533
  2157
syntax and examples.
wenzelm@17533
  2158
wenzelm@17533
  2159
* New commands 'cpodef' and 'pcpodef' for defining predicate subtypes
wenzelm@17533
  2160
of cpo and pcpo types. Syntax is exactly like the 'typedef' command,
wenzelm@17533
  2161
but the proof obligation additionally includes an admissibility
wenzelm@17533
  2162
requirement. The packages generate instances of class cpo or pcpo,
wenzelm@17533
  2163
with continuity and strictness theorems for Rep and Abs.
huffman@17442
  2164
huffman@17584
  2165
* HOLCF: Many theorems have been renamed according to a more standard naming
huffman@17584
  2166
scheme (INCOMPATIBILITY):
huffman@17584
  2167
huffman@17584
  2168
  foo_inject:  "foo$x = foo$y ==> x = y"
huffman@17584
  2169
  foo_eq:      "(foo$x = foo$y) = (x = y)"
huffman@17584
  2170
  foo_less:    "(foo$x << foo$y) = (x << y)"
huffman@17584
  2171
  foo_strict:  "foo$UU = UU"
huffman@17584
  2172
  foo_defined: "... ==> foo$x ~= UU"
huffman@17584
  2173
  foo_defined_iff: "(foo$x = UU) = (x = UU)"
huffman@17584
  2174
wenzelm@14682
  2175
paulson@14885
  2176
*** ZF ***
paulson@14885
  2177
wenzelm@16234
  2178
* ZF/ex: theories Group and Ring provide examples in abstract algebra,
wenzelm@16234
  2179
including the First Isomorphism Theorem (on quotienting by the kernel
wenzelm@16234
  2180
of a homomorphism).
wenzelm@15089
  2181
wenzelm@15089
  2182
* ZF/Simplifier: install second copy of type solver that actually
wenzelm@16234
  2183
makes use of TC rules declared to Isar proof contexts (or locales);
wenzelm@16234
  2184
the old version is still required for ML proof scripts.
wenzelm@15703
  2185
wenzelm@15703
  2186
wenzelm@17445
  2187
*** Cube ***
wenzelm@17445
  2188
wenzelm@17445
  2189
* Converted to Isar theory format; use locales instead of axiomatic
wenzelm@17445
  2190
theories.
wenzelm@17445
  2191
wenzelm@17445
  2192
wenzelm@15703
  2193
*** ML ***
wenzelm@15703
  2194
haftmann@21339
  2195
* Pure/library.ML: added ##>, ##>>, #>> -- higher-order counterparts
haftmann@21339
  2196
for ||>, ||>>, |>>,
haftmann@21339
  2197
wenzelm@15973
  2198
* Pure/library.ML no longer defines its own option datatype, but uses
wenzelm@16234
  2199
that of the SML basis, which has constructors NONE and SOME instead of
wenzelm@16234
  2200
None and Some, as well as exception Option.Option instead of OPTION.
wenzelm@16234
  2201
The functions the, if_none, is_some, is_none have been adapted
wenzelm@16234
  2202
accordingly, while Option.map replaces apsome.
wenzelm@15973
  2203
wenzelm@16860
  2204
* Pure/library.ML: the exception LIST has been given up in favour of
wenzelm@16860
  2205
the standard exceptions Empty and Subscript, as well as
wenzelm@16860
  2206
Library.UnequalLengths.  Function like Library.hd and Library.tl are
wenzelm@16860
  2207
superceded by the standard hd and tl functions etc.
wenzelm@16860
  2208
wenzelm@16860
  2209
A number of basic list functions are no longer exported to the ML
wenzelm@16860
  2210
toplevel, as they are variants of predefined functions.  The following
wenzelm@16234
  2211
suggests how one can translate existing code:
wenzelm@15973
  2212
wenzelm@15973
  2213
    rev_append xs ys = List.revAppend (xs, ys)
wenzelm@15973
  2214
    nth_elem (i, xs) = List.nth (xs, i)
wenzelm@15973
  2215
    last_elem xs = List.last xs
wenzelm@15973
  2216
    flat xss = List.concat xss
wenzelm@16234
  2217
    seq fs = List.app fs
wenzelm@15973
  2218
    partition P xs = List.partition P xs
wenzelm@15973
  2219
    mapfilter f xs = List.mapPartial f xs
wenzelm@15973
  2220
wenzelm@16860
  2221
* Pure/library.ML: several combinators for linear functional
wenzelm@16860
  2222
transformations, notably reverse application and composition:
wenzelm@16860
  2223
wenzelm@17371
  2224
  x |> f                f #> g
wenzelm@17371
  2225
  (x, y) |-> f          f #-> g
wenzelm@16860
  2226
haftmann@17495
  2227
* Pure/library.ML: introduced/changed precedence of infix operators:
haftmann@17495
  2228
haftmann@17495
  2229
  infix 1 |> |-> ||> ||>> |>> |>>> #> #->;
haftmann@17495
  2230
  infix 2 ?;
haftmann@17495
  2231
  infix 3 o oo ooo oooo;
haftmann@17495
  2232
  infix 4 ~~ upto downto;
haftmann@17495
  2233
haftmann@17495
  2234
Maybe INCOMPATIBILITY when any of those is used in conjunction with other
haftmann@17495
  2235
infix operators.
haftmann@17495
  2236
wenzelm@17408
  2237
* Pure/library.ML: natural list combinators fold, fold_rev, and
haftmann@16869
  2238
fold_map support linear functional transformations and nesting.  For
wenzelm@16860
  2239
example:
wenzelm@16860
  2240
wenzelm@16860
  2241
  fold f [x1, ..., xN] y =
wenzelm@16860
  2242
    y |> f x1 |> ... |> f xN
wenzelm@16860
  2243
wenzelm@16860
  2244
  (fold o fold) f [xs1, ..., xsN] y =
wenzelm@16860
  2245
    y |> fold f xs1 |> ... |> fold f xsN
wenzelm@16860
  2246
wenzelm@16860
  2247
  fold f [x1, ..., xN] =
wenzelm@16860
  2248
    f x1 #> ... #> f xN
wenzelm@16860
  2249
wenzelm@16860
  2250
  (fold o fold) f [xs1, ..., xsN] =
wenzelm@16860
  2251
    fold f xs1 #> ... #> fold f xsN
wenzelm@16860
  2252
wenzelm@17408
  2253
* Pure/library.ML: the following selectors on type 'a option are
wenzelm@17408
  2254
available:
wenzelm@17408
  2255
wenzelm@17408
  2256
  the:               'a option -> 'a  (*partial*)
wenzelm@17408
  2257
  these:             'a option -> 'a  where 'a = 'b list
haftmann@17402
  2258
  the_default: 'a -> 'a option -> 'a
haftmann@17402
  2259
  the_list:          'a option -> 'a list
haftmann@17402
  2260
wenzelm@17408
  2261
* Pure/General: structure AList (cf. Pure/General/alist.ML) provides
wenzelm@17408
  2262
basic operations for association lists, following natural argument
haftmann@17564
  2263
order; moreover the explicit equality predicate passed here avoids
haftmann@17495
  2264
potentially expensive polymorphic runtime equality checks.
haftmann@17495
  2265
The old functions may be expressed as follows:
wenzelm@17408
  2266
wenzelm@17408
  2267
  assoc = uncurry (AList.lookup (op =))
wenzelm@17408
  2268
  assocs = these oo AList.lookup (op =)
wenzelm@17408
  2269
  overwrite = uncurry (AList.update (op =)) o swap
wenzelm@17408
  2270
haftmann@17564
  2271
* Pure/General: structure AList (cf. Pure/General/alist.ML) provides
haftmann@17564
  2272
haftmann@17564
  2273
  val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
haftmann@17564
  2274
  val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list
haftmann@17564
  2275
haftmann@17564
  2276
replacing make_keylist and keyfilter (occassionally used)
haftmann@17564
  2277
Naive rewrites:
haftmann@17564
  2278
haftmann@17564
  2279
  make_keylist = AList.make
haftmann@17564
  2280
  keyfilter = AList.find (op =)
haftmann@17564
  2281
haftmann@17564
  2282
* eq_fst and eq_snd now take explicit equality parameter, thus
haftmann@17564
  2283
  avoiding eqtypes. Naive rewrites:
haftmann@17564
  2284
haftmann@17564
  2285
    eq_fst = eq_fst (op =)
haftmann@17564
  2286
    eq_snd = eq_snd (op =)
haftmann@17564
  2287
haftmann@17564
  2288
* Removed deprecated apl and apr (rarely used).
haftmann@17564
  2289
  Naive rewrites:
haftmann@17564
  2290
haftmann@17564
  2291
    apl (n, op) =>>= curry op n
haftmann@17564
  2292
    apr (op, m) =>>= fn n => op (n, m)
haftmann@17564
  2293
wenzelm@17408
  2294
* Pure/General: structure OrdList (cf. Pure/General/ord_list.ML)
wenzelm@17408
  2295
provides a reasonably efficient light-weight implementation of sets as
wenzelm@17408
  2296
lists.
wenzelm@17408
  2297
wenzelm@17408
  2298
* Pure/General: generic tables (cf. Pure/General/table.ML) provide a
wenzelm@17408
  2299
few new operations; existing lookup and update are now curried to
wenzelm@17408
  2300
follow natural argument order (for use with fold etc.);
wenzelm@17408
  2301
INCOMPATIBILITY, use (uncurry Symtab.lookup) etc. as last resort.
wenzelm@17408
  2302
wenzelm@17408
  2303
* Pure/General: output via the Isabelle channels of
wenzelm@17408
  2304
writeln/warning/error etc. is now passed through Output.output, with a
wenzelm@17408
  2305
hook for arbitrary transformations depending on the print_mode
wenzelm@17408
  2306
(cf. Output.add_mode -- the first active mode that provides a output
wenzelm@17408
  2307
function wins).  Already formatted output may be embedded into further
wenzelm@17408
  2308
text via Output.raw; the result of Pretty.string_of/str_of and derived
wenzelm@17408
  2309
functions (string_of_term/cterm/thm etc.) is already marked raw to
wenzelm@17408
  2310
accommodate easy composition of diagnostic messages etc.  Programmers
wenzelm@17408
  2311
rarely need to care about Output.output or Output.raw at all, with
wenzelm@17408
  2312
some notable exceptions: Output.output is required when bypassing the
wenzelm@17408
  2313
standard channels (writeln etc.), or in token translations to produce
wenzelm@17408
  2314
properly formatted results; Output.raw is required when capturing
wenzelm@17408
  2315
already output material that will eventually be presented to the user
wenzelm@17408
  2316
a second time.  For the default print mode, both Output.output and
wenzelm@17408
  2317
Output.raw have no effect.
wenzelm@17408
  2318
wenzelm@17408
  2319
* Pure/General: Output.time_accumulator NAME creates an operator ('a
wenzelm@17408
  2320
-> 'b) -> 'a -> 'b to measure runtime and count invocations; the
wenzelm@17408
  2321
cumulative results are displayed at the end of a batch session.
wenzelm@17408
  2322
wenzelm@17408
  2323
* Pure/General: File.sysify_path and File.quote_sysify path have been
wenzelm@17408
  2324
replaced by File.platform_path and File.shell_path (with appropriate
wenzelm@17408
  2325
hooks).  This provides a clean interface for unusual systems where the
wenzelm@17408
  2326
internal and external process view of file names are different.
wenzelm@17408
  2327
wenzelm@16689
  2328
* Pure: more efficient orders for basic syntactic entities: added
wenzelm@16689
  2329
fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord
wenzelm@16689
  2330
and typ_ord to use fast_string_ord and fast_indexname_ord (term_ord is
wenzelm@16689
  2331
NOT affected); structures Symtab, Vartab, Typtab, Termtab use the fast
wenzelm@16689
  2332
orders now -- potential INCOMPATIBILITY for code that depends on a
wenzelm@16689
  2333
particular order for Symtab.keys, Symtab.dest, etc. (consider using
wenzelm@16689
  2334
Library.sort_strings on result).
wenzelm@16689
  2335
wenzelm@17408
  2336
* Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types,
wenzelm@17408
  2337
fold_types traverse types/terms from left to right, observing natural
wenzelm@17408
  2338
argument order.  Supercedes previous foldl_XXX versions, add_frees,
wenzelm@17408
  2339
add_vars etc. have been adapted as well: INCOMPATIBILITY.
wenzelm@17408
  2340
wenzelm@16151
  2341
* Pure: name spaces have been refined, with significant changes of the
wenzelm@16234
  2342
internal interfaces -- INCOMPATIBILITY.  Renamed cond_extern(_table)
wenzelm@16234
  2343
to extern(_table).  The plain name entry path is superceded by a
wenzelm@16234
  2344
general 'naming' context, which also includes the 'policy' to produce
wenzelm@16234
  2345
a fully qualified name and external accesses of a fully qualified
wenzelm@16234
  2346
name; NameSpace.extend is superceded by context dependent
wenzelm@16234
  2347
Sign.declare_name.  Several theory and proof context operations modify
wenzelm@16234
  2348
the naming context.  Especially note Theory.restore_naming and
wenzelm@16234
  2349
ProofContext.restore_naming to get back to a sane state; note that
wenzelm@16234
  2350
Theory.add_path is no longer sufficient to recover from
wenzelm@16234
  2351
Theory.absolute_path in particular.
wenzelm@16234
  2352
wenzelm@16234
  2353
* Pure: new flags short_names (default false) and unique_names
wenzelm@16234
  2354
(default true) for controlling output of qualified names.  If
wenzelm@16234
  2355
short_names is set, names are printed unqualified.  If unique_names is
wenzelm@16234
  2356
reset, the name prefix is reduced to the minimum required to achieve
wenzelm@16234
  2357
the original result when interning again, even if there is an overlap
wenzelm@16234
  2358
with earlier declarations.
wenzelm@16151
  2359
wenzelm@16456
  2360
* Pure/TheoryDataFun: change of the argument structure; 'prep_ext' is
wenzelm@16456
  2361
now 'extend', and 'merge' gets an additional Pretty.pp argument
wenzelm@16456
  2362
(useful for printing error messages).  INCOMPATIBILITY.
wenzelm@16456
  2363
wenzelm@16456
  2364
* Pure: major reorganization of the theory context.  Type Sign.sg and
wenzelm@16456
  2365
Theory.theory are now identified, referring to the universal
wenzelm@16456
  2366
Context.theory (see Pure/context.ML).  Actual signature and theory
wenzelm@16456
  2367
content is managed as theory data.  The old code and interfaces were
wenzelm@16456
  2368
spread over many files and structures; the new arrangement introduces
wenzelm@16456
  2369
considerable INCOMPATIBILITY to gain more clarity:
wenzelm@16456
  2370
wenzelm@16456
  2371
  Context -- theory management operations (name, identity, inclusion,
wenzelm@16456
  2372
    parents, ancestors, merge, etc.), plus generic theory data;
wenzelm@16456
  2373
wenzelm@16456
  2374
  Sign -- logical signature and syntax operations (declaring consts,
wenzelm@16456
  2375
    types, etc.), plus certify/read for common entities;
wenzelm@16456
  2376
wenzelm@16456
  2377
  Theory -- logical theory operations (stating axioms, definitions,
wenzelm@16456
  2378
    oracles), plus a copy of logical signature operations (consts,
wenzelm@16456
  2379
    types, etc.); also a few basic management operations (Theory.copy,
wenzelm@16456
  2380
    Theory.merge, etc.)
wenzelm@16456
  2381
wenzelm@16456
  2382
The most basic sign_of operations (Theory.sign_of, Thm.sign_of_thm
wenzelm@16456
  2383
etc.) as well as the sign field in Thm.rep_thm etc. have been retained
wenzelm@16456
  2384
for convenience -- they merely return the theory.
wenzelm@16456
  2385
wenzelm@17193
  2386
* Pure: type Type.tsig is superceded by theory in most interfaces.
wenzelm@17193
  2387
wenzelm@16547
  2388
* Pure: the Isar proof context type is already defined early in Pure
wenzelm@16547
  2389
as Context.proof (note that ProofContext.context and Proof.context are
wenzelm@16547
  2390
aliases, where the latter is the preferred name).  This enables other
wenzelm@16547
  2391
Isabelle components to refer to that type even before Isar is present.
wenzelm@16547
  2392
wenzelm@16373
  2393
* Pure/sign/theory: discontinued named name spaces (i.e. classK,
wenzelm@16373
  2394
typeK, constK, axiomK, oracleK), but provide explicit operations for
wenzelm@16373
  2395
any of these kinds.  For example, Sign.intern typeK is now
wenzelm@16373
  2396
Sign.intern_type, Theory.hide_space Sign.typeK is now
wenzelm@16373
  2397
Theory.hide_types.  Also note that former
wenzelm@16373
  2398
Theory.hide_classes/types/consts are now
wenzelm@16373
  2399
Theory.hide_classes_i/types_i/consts_i, while the non '_i' versions
wenzelm@16373
  2400
internalize their arguments!  INCOMPATIBILITY.
wenzelm@16373
  2401
wenzelm@16506
  2402
* Pure: get_thm interface (of PureThy and ProofContext) expects
wenzelm@16506
  2403
datatype thmref (with constructors Name and NameSelection) instead of
wenzelm@16506
  2404
plain string -- INCOMPATIBILITY;
wenzelm@16506
  2405
wenzelm@16151
  2406
* Pure: cases produced by proof methods specify options, where NONE
wenzelm@16234
  2407
means to remove case bindings -- INCOMPATIBILITY in
wenzelm@16234
  2408
(RAW_)METHOD_CASES.
wenzelm@16151
  2409
wenzelm@16373
  2410
* Pure: the following operations retrieve axioms or theorems from a
wenzelm@16373
  2411
theory node or theory hierarchy, respectively:
wenzelm@16373
  2412
wenzelm@16373
  2413
  Theory.axioms_of: theory -> (string * term) list
wenzelm@16373
  2414
  Theory.all_axioms_of: theory -> (string * term) list
wenzelm@16373
  2415
  PureThy.thms_of: theory -> (string * thm) list
wenzelm@16373
  2416
  PureThy.all_thms_of: theory -> (string * thm) list
wenzelm@16373
  2417
wenzelm@16718
  2418
* Pure: print_tac now outputs the goal through the trace channel.
wenzelm@16718
  2419
wenzelm@17408
  2420
* Isar toplevel: improved diagnostics, mostly for Poly/ML only.
wenzelm@17408
  2421
Reference Toplevel.debug (default false) controls detailed printing
wenzelm@17408
  2422
and tracing of low-level exceptions; Toplevel.profiling (default 0)
wenzelm@17408
  2423
controls execution profiling -- set to 1 for time and 2 for space
wenzelm@17408
  2424
(both increase the runtime).
wenzelm@17408
  2425
wenzelm@17408
  2426
* Isar session: The initial use of ROOT.ML is now always timed,
wenzelm@17408
  2427
i.e. the log will show the actual process times, in contrast to the
wenzelm@17408
  2428
elapsed wall-clock time that the outer shell wrapper produces.
wenzelm@17408
  2429
wenzelm@17408
  2430
* Simplifier: improved handling of bound variables (nameless
wenzelm@16997
  2431
representation, avoid allocating new strings).  Simprocs that invoke
wenzelm@16997
  2432
the Simplifier recursively should use Simplifier.inherit_bounds to
wenzelm@17720
  2433
avoid local name clashes.  Failure to do so produces warnings
wenzelm@17720
  2434
"Simplifier: renamed bound variable ..."; set Simplifier.debug_bounds
wenzelm@17720
  2435
for further details.
wenzelm@16234
  2436
wenzelm@17166
  2437
* ML functions legacy_bindings and use_legacy_bindings produce ML fact
wenzelm@17166
  2438
bindings for all theorems stored within a given theory; this may help
wenzelm@17166
  2439
in porting non-Isar theories to Isar ones, while keeping ML proof
wenzelm@17166
  2440
scripts for the time being.
wenzelm@17166
  2441
wenzelm@17457
  2442
* ML operator HTML.with_charset specifies the charset begin used for
wenzelm@17457
  2443
generated HTML files.  For example:
wenzelm@17457
  2444
wenzelm@17457
  2445
  HTML.with_charset "utf-8" use_thy "Hebrew";
wenzelm@17538
  2446
  HTML.with_charset "utf-8" use_thy "Chinese";
wenzelm@17457
  2447
wenzelm@16234
  2448
wenzelm@16234
  2449
*** System ***
wenzelm@16234
  2450
wenzelm@16234
  2451
* Allow symlinks to all proper Isabelle executables (Isabelle,
wenzelm@16234
  2452
isabelle, isatool etc.).
wenzelm@16234
  2453
wenzelm@16234
  2454
* ISABELLE_DOC_FORMAT setting specifies preferred document format (for
wenzelm@16234
  2455
isatool doc, isatool mkdir, display_drafts etc.).
wenzelm@16234
  2456
wenzelm@16234
  2457
* isatool usedir: option -f allows specification of the ML file to be
wenzelm@16234
  2458
used by Isabelle; default is ROOT.ML.
wenzelm@16234
  2459
wenzelm@16251
  2460
* New isatool version outputs the version identifier of the Isabelle
wenzelm@16251
  2461
distribution being used.
wenzelm@16251
  2462
wenzelm@16251
  2463
* HOL: new isatool dimacs2hol converts files in DIMACS CNF format
wenzelm@16234
  2464
(containing Boolean satisfiability problems) into Isabelle/HOL
wenzelm@16234
  2465
theories.
wenzelm@15703
  2466
wenzelm@15703
  2467
wenzelm@14655
  2468
wenzelm@14606
  2469
New in Isabelle2004 (April 2004)
wenzelm@14606
  2470
--------------------------------
wenzelm@13280
  2471
skalberg@14171
  2472
*** General ***
skalberg@14171
  2473
ballarin@14398
  2474
* Provers/order.ML:  new efficient reasoner for partial and linear orders.
ballarin@14398
  2475
  Replaces linorder.ML.
ballarin@14398
  2476
wenzelm@14606
  2477
* Pure: Greek letters (except small lambda, \<lambda>), as well as Gothic
wenzelm@14606
  2478
  (\<aa>...\<zz>\<AA>...\<ZZ>), calligraphic (\<A>...\<Z>), and Euler
skalberg@14173
  2479
  (\<a>...\<z>), are now considered normal letters, and can therefore
skalberg@14173
  2480
  be used anywhere where an ASCII letter (a...zA...Z) has until
skalberg@14173
  2481
  now. COMPATIBILITY: This obviously changes the parsing of some
skalberg@14173
  2482
  terms, especially where a symbol has been used as a binder, say
skalberg@14173
  2483
  '\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed
skalberg@14173
  2484
  as an identifier.  Fix it by inserting a space around former
skalberg@14173
  2485
  symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
skalberg@14173
  2486
  existing theory and ML files.
skalberg@14171
  2487
paulson@14237
  2488
* Pure: Macintosh and Windows line-breaks are now allowed in theory files.
paulson@14237
  2489
wenzelm@14731
  2490
* Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now
wenzelm@14731
  2491
  allowed in identifiers. Similar to Greek letters \<^isub> is now considered
wenzelm@14731
  2492
  a normal (but invisible) letter. For multiple letter subscripts repeat
wenzelm@14731
  2493
  \<^isub> like this: x\<^isub>1\<^isub>2.
kleing@14233
  2494
kleing@14333
  2495
* Pure: There are now sub-/superscripts that can span more than one
kleing@14333
  2496
  character. Text between \<^bsub> and \<^esub> is set in subscript in
wenzelm@14606
  2497
  ProofGeneral and LaTeX, text between \<^bsup> and \<^esup> in
wenzelm@14606
  2498
  superscript. The new control characters are not identifier parts.
kleing@14333
  2499
schirmer@14561
  2500
* Pure: Control-symbols of the form \<^raw:...> will literally print the
wenzelm@14606
  2501
  content of "..." to the latex file instead of \isacntrl... . The "..."
wenzelm@14606
  2502
  may consist of any printable characters excluding the end bracket >.
schirmer@14361
  2503
paulson@14237
  2504
* Pure: Using new Isar command "finalconsts" (or the ML functions
paulson@14237
  2505
  Theory.add_finals or Theory.add_finals_i) it is now possible to
paulson@14237
  2506
  declare constants "final", which prevents their being given a definition
paulson@14237
  2507
  later.  It is useful for constants whose behaviour is fixed axiomatically
skalberg@14224
  2508
  rather than definitionally, such as the meta-logic connectives.
skalberg@14224
  2509
wenzelm@14606
  2510
* Pure: 'instance' now handles general arities with general sorts
wenzelm@14606
  2511
  (i.e. intersections of classes),
skalberg@14503
  2512
kleing@14547
  2513
* Presentation: generated HTML now uses a CSS style sheet to make layout
wenzelm@14731
  2514
  (somewhat) independent of content. It is copied from lib/html/isabelle.css.
kleing@14547
  2515
  It can be changed to alter the colors/layout of generated pages.
kleing@14547
  2516
wenzelm@14556
  2517
ballarin@14175
  2518
*** Isar ***
ballarin@14175
  2519
ballarin@14508
  2520
* Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac,
ballarin@14508
  2521
  cut_tac, subgoal_tac and thin_tac:
ballarin@14175
  2522
  - Now understand static (Isar) contexts.  As a consequence, users of Isar
ballarin@14175
  2523
    locales are no longer forced to write Isar proof scripts.
ballarin@14175
  2524
    For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
ballarin@14175
  2525
    emulations.
ballarin@14175
  2526
  - INCOMPATIBILITY: names of variables to be instantiated may no
ballarin@14211
  2527
    longer be enclosed in quotes.  Instead, precede variable name with `?'.
ballarin@14211
  2528
    This is consistent with the instantiation attribute "where".
ballarin@14211
  2529
ballarin@14257
  2530
* Attributes "where" and "of":
ballarin@14285
  2531
  - Now take type variables of instantiated theorem into account when reading
ballarin@14285
  2532
    the instantiation string.  This fixes a bug that caused instantiated
ballarin@14285
  2533
    theorems to have too special types in some circumstances.
ballarin@14285
  2534
  - "where" permits explicit instantiations of type variables.
ballarin@14257
  2535
wenzelm@14556
  2536
* Calculation commands "moreover" and "also" no longer interfere with
wenzelm@14556
  2537
  current facts ("this"), admitting arbitrary combinations with "then"
wenzelm@14556
  2538
  and derived forms.
kleing@14283
  2539
ballarin@14211
  2540
* Locales:
ballarin@14211
  2541
  - Goal statements involving the context element "includes" no longer
ballarin@14211
  2542
    generate theorems with internal delta predicates (those ending on
ballarin@14211
  2543
    "_axioms") in the premise.
ballarin@14211
  2544
    Resolve particular premise with <locale>.intro to obtain old form.
ballarin@14211
  2545
  - Fixed bug in type inference ("unify_frozen") that prevented mix of target
ballarin@14211
  2546
    specification and "includes" elements in goal statement.
ballarin@14254
  2547
  - Rule sets <locale>.intro and <locale>.axioms no longer declared as
ballarin@14254
  2548
    [intro?] and [elim?] (respectively) by default.
ballarin@14508
  2549
  - Experimental command for instantiation of locales in proof contexts:
ballarin@14551
  2550
        instantiate <label>[<attrs>]: <loc>
ballarin@14508
  2551
    Instantiates locale <loc> and adds all its theorems to the current context
ballarin@14551
  2552
    taking into account their attributes.  Label and attrs are optional
ballarin@14551
  2553
    modifiers, like in theorem declarations.  If present, names of
ballarin@14551
  2554
    instantiated theorems are qualified with <label>, and the attributes
ballarin@14551
  2555
    <attrs> are applied after any attributes these theorems might have already.
ballarin@14551
  2556
      If the locale has assumptions, a chained fact of the form