NEWS
author haftmann
Thu, 15 Apr 2010 12:27:14 +0200
changeset 36147 b43b22f63665
parent 36096 abc6a2ea4b88
child 36162 0bd034a80a9a
permissions -rw-r--r--
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5363
0cf15843b82f isatool install;
wenzelm
parents: 5332
diff changeset
     1
Isabelle NEWS -- history user-relevant changes
0cf15843b82f isatool install;
wenzelm
parents: 5332
diff changeset
     2
==============================================
2553
ed941505cab7 Isabelle NEWS -- history of user-visible changes;
wenzelm
parents:
diff changeset
     3
33993
haftmann
parents: 33873
diff changeset
     4
New in this Isabelle version
haftmann
parents: 33873
diff changeset
     5
----------------------------
haftmann
parents: 33873
diff changeset
     6
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
     7
*** General ***
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
     8
35436
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
     9
* Authentic syntax for *all* logical entities (type classes, type
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    10
constructors, term constants): provides simple and robust
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    11
correspondence between formal entities and concrete syntax.  Within
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    12
the parse tree / AST representations, "constants" are decorated by
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    13
their category (class, type, const) and spelled out explicitly with
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    14
their full internal name.
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    15
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    16
Substantial INCOMPATIBILITY concerning low-level syntax declarations
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    17
and translations (translation rules and translation functions in ML).
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    18
Some hints on upgrading:
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    19
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    20
  - Many existing uses of 'syntax' and 'translations' can be replaced
35436
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    21
    by more modern 'type_notation', 'notation' and 'abbreviation',
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    22
    which are independent of this issue.
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    23
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    24
  - 'translations' require markup within the AST; the term syntax
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    25
    provides the following special forms:
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    26
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    27
      CONST c   -- produces syntax version of constant c from context
35261
wenzelm
parents: 35260
diff changeset
    28
      XCONST c  -- literally c, checked as constant from context
wenzelm
parents: 35260
diff changeset
    29
      c         -- literally c, if declared by 'syntax'
wenzelm
parents: 35260
diff changeset
    30
wenzelm
parents: 35260
diff changeset
    31
    Plain identifiers are treated as AST variables -- occasionally the
wenzelm
parents: 35260
diff changeset
    32
    system indicates accidental variables via the error "rhs contains
wenzelm
parents: 35260
diff changeset
    33
    extra variables".
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    34
35436
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    35
    Type classes and type constructors are marked according to their
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    36
    concrete syntax.  Some old translations rules need to be written
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    37
    for the "type" category, using type constructor application
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    38
    instead of pseudo-term application of the default category
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    39
    "logic".
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    40
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    41
  - 'parse_translation' etc. in ML may use the following
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    42
    antiquotations:
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    43
35436
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    44
      @{class_syntax c}   -- type class c within parse tree / AST
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    45
      @{term_syntax c}    -- type constructor c within parse tree / AST
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    46
      @{const_syntax c}   -- ML version of "CONST c" above
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    47
      @{syntax_const c}   -- literally c (checked wrt. 'syntax' declarations)
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    48
35436
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    49
  - Literal types within 'typed_print_translations', i.e. those *not*
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    50
    represented as pseudo-terms are represented verbatim.  Use @{class
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    51
    c} or @{type_name c} here instead of the above syntax
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    52
    antiquotations.
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    53
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    54
Note that old non-authentic syntax was based on unqualified base
35436
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    55
names, so all of the above "constant" names would coincide.  Recall
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    56
that 'print_syntax' and ML_command "set Syntax.trace_ast" help to
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
    57
diagnose syntax problems.
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    58
35351
7425aece4ee3 allow general mixfix syntax for type constructors;
wenzelm
parents: 35306
diff changeset
    59
* Type constructors admit general mixfix syntax, not just infix.
7425aece4ee3 allow general mixfix syntax for type constructors;
wenzelm
parents: 35306
diff changeset
    60
35613
9d3ff36ad4e1 eliminated Args.bang_facts (legacy feature);
wenzelm
parents: 35436
diff changeset
    61
* Use of cumulative prems via "!" in some proof methods has been
9d3ff36ad4e1 eliminated Args.bang_facts (legacy feature);
wenzelm
parents: 35436
diff changeset
    62
discontinued (legacy feature).
9d3ff36ad4e1 eliminated Args.bang_facts (legacy feature);
wenzelm
parents: 35436
diff changeset
    63
35979
12bb31230550 replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
boehmes
parents: 35845
diff changeset
    64
* References 'trace_simp' and 'debug_simp' have been replaced by
12bb31230550 replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
boehmes
parents: 35845
diff changeset
    65
configuration options stored in the context. Enabling tracing
12bb31230550 replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
boehmes
parents: 35845
diff changeset
    66
(the case of debugging is similar) in proofs works via
12bb31230550 replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
boehmes
parents: 35845
diff changeset
    67
12bb31230550 replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
boehmes
parents: 35845
diff changeset
    68
  using [[trace_simp=true]]
12bb31230550 replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
boehmes
parents: 35845
diff changeset
    69
12bb31230550 replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
boehmes
parents: 35845
diff changeset
    70
Tracing is then active for all invocations of the simplifier
35995
26e820d27e0a re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
boehmes
parents: 35979
diff changeset
    71
in subsequent goal refinement steps. Tracing may also still be
26e820d27e0a re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
boehmes
parents: 35979
diff changeset
    72
enabled or disabled via the ProofGeneral settings menu.
35979
12bb31230550 replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
boehmes
parents: 35845
diff changeset
    73
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
    74
34170
254ac75e4c38 reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents: 34076
diff changeset
    75
*** Pure ***
254ac75e4c38 reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents: 34076
diff changeset
    76
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36096
diff changeset
    77
* Code generator: simple concept for abstract datatypes obeying invariants.
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36096
diff changeset
    78
35765
09e238561460 local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents: 35763
diff changeset
    79
* Local theory specifications may depend on extra type variables that
09e238561460 local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents: 35763
diff changeset
    80
are not present in the result type -- arguments TYPE('a) :: 'a itself
09e238561460 local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents: 35763
diff changeset
    81
are added internally.  For example:
09e238561460 local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents: 35763
diff changeset
    82
09e238561460 local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents: 35763
diff changeset
    83
  definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
09e238561460 local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents: 35763
diff changeset
    84
34170
254ac75e4c38 reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents: 34076
diff changeset
    85
* Code generator: details of internal data cache have no impact on
254ac75e4c38 reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents: 34076
diff changeset
    86
the user space functionality any longer.
254ac75e4c38 reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents: 34076
diff changeset
    87
36093
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 34962
diff changeset
    88
* Methods unfold_locales and intro_locales ignore non-locale subgoals.  This
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 34962
diff changeset
    89
is more appropriate for interpretations with 'where'.  INCOMPATIBILITY.
34170
254ac75e4c38 reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents: 34076
diff changeset
    90
35129
ed24ba6f69aa discontinued unnamed infix syntax;
wenzelm
parents: 35111
diff changeset
    91
* Discontinued unnamed infix syntax (legacy feature for many years) --
35130
0991c84e8dcf renamed InfixName to Infix etc.;
wenzelm
parents: 35129
diff changeset
    92
need to specify constant name and syntax separately.  Internal ML
0991c84e8dcf renamed InfixName to Infix etc.;
wenzelm
parents: 35129
diff changeset
    93
datatype constructors have been renamed from InfixName to Infix etc.
0991c84e8dcf renamed InfixName to Infix etc.;
wenzelm
parents: 35129
diff changeset
    94
Minor INCOMPATIBILITY.
35129
ed24ba6f69aa discontinued unnamed infix syntax;
wenzelm
parents: 35111
diff changeset
    95
35413
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35401
diff changeset
    96
* Commands 'type_notation' and 'no_type_notation' declare type syntax
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35401
diff changeset
    97
within a local theory context, with explicit checking of the
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35401
diff changeset
    98
constructors involved (in contrast to the raw 'syntax' versions).
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35401
diff changeset
    99
35681
8b22a498b034 localized typedecl;
wenzelm
parents: 35613
diff changeset
   100
* Command 'typedecl' now works within a local theory context --
8b22a498b034 localized typedecl;
wenzelm
parents: 35613
diff changeset
   101
without introducing dependencies on parameters or assumptions, which
8b22a498b034 localized typedecl;
wenzelm
parents: 35613
diff changeset
   102
is not possible in Isabelle/Pure.
8b22a498b034 localized typedecl;
wenzelm
parents: 35613
diff changeset
   103
36044
krauss
parents: 36000
diff changeset
   104
* Proof terms: Type substitutions on proof constants now use canonical
krauss
parents: 36000
diff changeset
   105
order of type variables. INCOMPATIBILITY: Tools working with proof
krauss
parents: 36000
diff changeset
   106
terms may need to be adapted.
krauss
parents: 36000
diff changeset
   107
34170
254ac75e4c38 reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents: 34076
diff changeset
   108
33993
haftmann
parents: 33873
diff changeset
   109
*** HOL ***
haftmann
parents: 33873
diff changeset
   110
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36096
diff changeset
   111
* Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36096
diff changeset
   112
provides abstract red-black tree type which is backed by RBT_Impl
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36096
diff changeset
   113
as implementation.  INCOMPATIBILTY.
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36096
diff changeset
   114
35745
1416f568b2b6 command 'typedef' now works within a local theory context;
wenzelm
parents: 35728
diff changeset
   115
* Command 'typedef' now works within a local theory context -- without
1416f568b2b6 command 'typedef' now works within a local theory context;
wenzelm
parents: 35728
diff changeset
   116
introducing dependencies on parameters or assumptions, which is not
1416f568b2b6 command 'typedef' now works within a local theory context;
wenzelm
parents: 35728
diff changeset
   117
possible in Isabelle/Pure/HOL.  Note that the logical environment may
1416f568b2b6 command 'typedef' now works within a local theory context;
wenzelm
parents: 35728
diff changeset
   118
contain multiple interpretations of local typedefs (with different
1416f568b2b6 command 'typedef' now works within a local theory context;
wenzelm
parents: 35728
diff changeset
   119
non-emptiness proofs), even in a global theory context.
1416f568b2b6 command 'typedef' now works within a local theory context;
wenzelm
parents: 35728
diff changeset
   120
35763
765f8adf10f9 removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
wenzelm
parents: 35745
diff changeset
   121
* Theory Library/Coinductive_List has been removed -- superceded by
765f8adf10f9 removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
wenzelm
parents: 35745
diff changeset
   122
AFP/thys/Coinductive.
765f8adf10f9 removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
wenzelm
parents: 35745
diff changeset
   123
35728
haftmann
parents: 35721
diff changeset
   124
* Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
haftmann
parents: 35721
diff changeset
   125
Min, Max from theory Finite_Set.  INCOMPATIBILITY.
haftmann
parents: 35721
diff changeset
   126
35372
ca158c7b1144 renamed theory Rational to Rat
haftmann
parents: 35306
diff changeset
   127
* Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc.
ca158c7b1144 renamed theory Rational to Rat
haftmann
parents: 35306
diff changeset
   128
INCOMPATIBILITY.
ca158c7b1144 renamed theory Rational to Rat
haftmann
parents: 35306
diff changeset
   129
35042
a27b48967b26 NEWS: ax_simps
haftmann
parents: 35039
diff changeset
   130
* New set of rules "ac_simps" provides combined assoc / commute rewrites
a27b48967b26 NEWS: ax_simps
haftmann
parents: 35039
diff changeset
   131
for all interpretations of the appropriate generic locales.
a27b48967b26 NEWS: ax_simps
haftmann
parents: 35039
diff changeset
   132
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35042
diff changeset
   133
* Renamed theory "OrderedGroup" to "Groups" and split theory "Ring_and_Field"
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35042
diff changeset
   134
into theories "Rings" and "Fields";  for more appropriate and more
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35042
diff changeset
   135
consistent names suitable for name prefixes within the HOL theories.
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35042
diff changeset
   136
INCOMPATIBILITY.
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35042
diff changeset
   137
35084
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   138
* Some generic constants have been put to appropriate theories:
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   139
35093
haftmann
parents: 35084
diff changeset
   140
    less_eq, less: Orderings
35264
haftmann
parents: 35130
diff changeset
   141
    zero, one, plus, minus, uminus, times, abs, sgn: Groups
35084
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   142
    inverse, divide: Rings
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   143
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   144
INCOMPATIBILITY.
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   145
35721
f7bbee848403 fixed typo
haftmann
parents: 35681
diff changeset
   146
* Class division_ring also requires proof of fact divide_inverse.  However instantiation
35084
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   147
of parameter divide has also been required previously.  INCOMPATIBILITY.
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   148
35032
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 35027
diff changeset
   149
* More consistent naming of type classes involving orderings (and lattices):
35027
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   150
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   151
    lower_semilattice                   ~> semilattice_inf
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   152
    upper_semilattice                   ~> semilattice_sup
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   153
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   154
    dense_linear_order                  ~> dense_linorder
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   155
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   156
    pordered_ab_group_add               ~> ordered_ab_group_add
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   157
    pordered_ab_group_add_abs           ~> ordered_ab_group_add_abs
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   158
    pordered_ab_semigroup_add           ~> ordered_ab_semigroup_add
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   159
    pordered_ab_semigroup_add_imp_le    ~> ordered_ab_semigroup_add_imp_le
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   160
    pordered_cancel_ab_semigroup_add    ~> ordered_cancel_ab_semigroup_add
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   161
    pordered_cancel_comm_semiring       ~> ordered_cancel_comm_semiring
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   162
    pordered_cancel_semiring            ~> ordered_cancel_semiring
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   163
    pordered_comm_monoid_add            ~> ordered_comm_monoid_add
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   164
    pordered_comm_ring                  ~> ordered_comm_ring
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   165
    pordered_comm_semiring              ~> ordered_comm_semiring
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   166
    pordered_ring                       ~> ordered_ring
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   167
    pordered_ring_abs                   ~> ordered_ring_abs
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   168
    pordered_semiring                   ~> ordered_semiring
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   169
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   170
    ordered_ab_group_add                ~> linordered_ab_group_add
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   171
    ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   172
    ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   173
    ordered_comm_semiring_strict        ~> linordered_comm_semiring_strict
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   174
    ordered_field                       ~> linordered_field
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   175
    ordered_field_no_lb                 ~> linordered_field_no_lb
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   176
    ordered_field_no_ub                 ~> linordered_field_no_ub
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   177
    ordered_field_dense_linear_order    ~> dense_linordered_field
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   178
    ordered_idom                        ~> linordered_idom
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   179
    ordered_ring                        ~> linordered_ring
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   180
    ordered_ring_le_cancel_factor       ~> linordered_ring_le_cancel_factor
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   181
    ordered_ring_less_cancel_factor     ~> linordered_ring_less_cancel_factor
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   182
    ordered_ring_strict                 ~> linordered_ring_strict
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   183
    ordered_semidom                     ~> linordered_semidom
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   184
    ordered_semiring                    ~> linordered_semiring
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   185
    ordered_semiring_1                  ~> linordered_semiring_1
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   186
    ordered_semiring_1_strict           ~> linordered_semiring_1_strict
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   187
    ordered_semiring_strict             ~> linordered_semiring_strict
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   188
35032
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 35027
diff changeset
   189
  The following slightly odd type classes have been moved to
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 35027
diff changeset
   190
  a separate theory Library/Lattice_Algebras.thy:
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 35027
diff changeset
   191
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 35027
diff changeset
   192
    lordered_ab_group_add               ~> lattice_ab_group_add
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 35027
diff changeset
   193
    lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 35027
diff changeset
   194
    lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 35027
diff changeset
   195
    lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 35027
diff changeset
   196
    lordered_ring                       ~> lattice_ring
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 35027
diff changeset
   197
35027
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   198
INCOMPATIBILITY.
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   199
34962
807f6ce0273d HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
haftmann
parents: 34946
diff changeset
   200
* HOLogic.strip_psplit: types are returned in syntactic order, similar
807f6ce0273d HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
haftmann
parents: 34946
diff changeset
   201
to other strip and tuple operations.  INCOMPATIBILITY.
807f6ce0273d HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
haftmann
parents: 34946
diff changeset
   202
34946
haftmann
parents: 34933
diff changeset
   203
* Various old-style primrec specifications in the HOL theories have been
haftmann
parents: 34933
diff changeset
   204
replaced by new-style primrec, especially in theory List.  The corresponding
haftmann
parents: 34933
diff changeset
   205
constants now have authentic syntax.  INCOMPATIBILITY.
haftmann
parents: 34933
diff changeset
   206
35276
haftmann
parents: 35275
diff changeset
   207
* Reorganized theory Multiset: swapped notation of pointwise and multiset order:
haftmann
parents: 35275
diff changeset
   208
  * pointwise ordering is instance of class order with standard syntax <= and <;
haftmann
parents: 35275
diff changeset
   209
  * multiset ordering has syntax <=# and <#; partial order properties are provided
haftmann
parents: 35275
diff changeset
   210
      by means of interpretation with prefix multiset_order.
haftmann
parents: 35275
diff changeset
   211
Less duplication, less historical organization of sections,
35270
haftmann
parents: 35264
diff changeset
   212
conversion from associations lists to multisets, rudimentary code generation.
haftmann
parents: 35264
diff changeset
   213
Use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed.
haftmann
parents: 35264
diff changeset
   214
INCOMPATIBILITY.
34946
haftmann
parents: 34933
diff changeset
   215
35009
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   216
* Reorganized theory Sum_Type; Inl and Inr now have authentic syntax.
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   217
INCOMPATIBILITY.
33993
haftmann
parents: 33873
diff changeset
   218
haftmann
parents: 33873
diff changeset
   219
* Code generation: ML and OCaml code is decorated with signatures.
haftmann
parents: 33873
diff changeset
   220
35009
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   221
* Theory Complete_Lattice: lemmas top_def and bot_def have been
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   222
replaced by the more convenient lemmas Inf_empty and Sup_empty.
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   223
Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   224
by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   225
former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   226
subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   227
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   228
* Theory Finite_Set and List: some lemmas have been generalized from
34076
e3daf3c07381 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents: 34062
diff changeset
   229
sets to lattices:
e3daf3c07381 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents: 34062
diff changeset
   230
34007
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   231
  fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   232
  fun_left_comm_idem_union      ~> fun_left_comm_idem_sup
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   233
  inter_Inter_fold_inter        ~> inf_Inf_fold_inf
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   234
  union_Union_fold_union        ~> sup_Sup_fold_sup
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   235
  Inter_fold_inter              ~> Inf_fold_inf
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   236
  Union_fold_union              ~> Sup_fold_sup
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   237
  inter_INTER_fold_inter        ~> inf_INFI_fold_inf
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   238
  union_UNION_fold_union        ~> sup_SUPR_fold_sup
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   239
  INTER_fold_inter              ~> INFI_fold_inf
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   240
  UNION_fold_union              ~> SUPR_fold_sup
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   241
35009
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   242
* Theory List: added transpose.
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   243
35100
53754ec7360b renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
wenzelm
parents: 35093
diff changeset
   244
* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid
53754ec7360b renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
wenzelm
parents: 35093
diff changeset
   245
clash with new theory Quotient in Main HOL.
53754ec7360b renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
wenzelm
parents: 35093
diff changeset
   246
35810
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   247
* Library/Nat_Bijection.thy is a collection of bijective functions
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   248
between nat and other types, which supersedes the older libraries
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   249
Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy.  INCOMPATIBILITY.
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   250
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   251
  Constants:
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   252
  Nat_Int_Bij.nat2_to_nat         ~> prod_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   253
  Nat_Int_Bij.nat_to_nat2         ~> prod_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   254
  Nat_Int_Bij.int_to_nat_bij      ~> int_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   255
  Nat_Int_Bij.nat_to_int_bij      ~> int_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   256
  Countable.pair_encode           ~> prod_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   257
  NatIso.prod2nat                 ~> prod_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   258
  NatIso.nat2prod                 ~> prod_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   259
  NatIso.sum2nat                  ~> sum_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   260
  NatIso.nat2sum                  ~> sum_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   261
  NatIso.list2nat                 ~> list_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   262
  NatIso.nat2list                 ~> list_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   263
  NatIso.set2nat                  ~> set_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   264
  NatIso.nat2set                  ~> set_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   265
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   266
  Lemmas:
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   267
  Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   268
  Nat_Int_Bij.nat2_to_nat_inj     ~> inj_prod_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   269
  Nat_Int_Bij.nat2_to_nat_surj    ~> surj_prod_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   270
  Nat_Int_Bij.nat_to_nat2_inj     ~> inj_prod_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   271
  Nat_Int_Bij.nat_to_nat2_surj    ~> surj_prod_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   272
  Nat_Int_Bij.i2n_n2i_id          ~> int_encode_inverse
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   273
  Nat_Int_Bij.n2i_i2n_id          ~> int_decode_inverse
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   274
  Nat_Int_Bij.surj_nat_to_int_bij ~> surj_int_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   275
  Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   276
  Nat_Int_Bij.inj_nat_to_int_bij  ~> inj_int_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   277
  Nat_Int_Bij.inj_int_to_nat_bij  ~> inj_int_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   278
  Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   279
  Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   280
33993
haftmann
parents: 33873
diff changeset
   281
haftmann
parents: 33873
diff changeset
   282
*** ML ***
haftmann
parents: 33873
diff changeset
   283
35401
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   284
* Antiquotations for basic formal entities:
35396
041bb8d18916 ML antiquotations for type classes;
wenzelm
parents: 35377
diff changeset
   285
041bb8d18916 ML antiquotations for type classes;
wenzelm
parents: 35377
diff changeset
   286
    @{class NAME}         -- type class
35401
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   287
    @{class_syntax NAME}  -- syntax representation of the above
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   288
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   289
    @{type_name NAME}     -- logical type
35361
4c7c849b70aa more orthogonal antiquotations for type constructors;
wenzelm
parents: 35351
diff changeset
   290
    @{type_abbrev NAME}   -- type abbreviation
4c7c849b70aa more orthogonal antiquotations for type constructors;
wenzelm
parents: 35351
diff changeset
   291
    @{nonterminal NAME}   -- type of concrete syntactic category
4c7c849b70aa more orthogonal antiquotations for type constructors;
wenzelm
parents: 35351
diff changeset
   292
    @{type_syntax NAME}   -- syntax representation of any of the above
4c7c849b70aa more orthogonal antiquotations for type constructors;
wenzelm
parents: 35351
diff changeset
   293
35401
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   294
    @{const_name NAME}    -- logical constant (INCOMPATIBILITY)
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   295
    @{const_abbrev NAME}  -- abbreviated constant
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   296
    @{const_syntax NAME}  -- syntax representation of any of the above
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   297
35111
18cd034922ba added ML antiquotation @{syntax_const};
wenzelm
parents: 35100
diff changeset
   298
* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
18cd034922ba added ML antiquotation @{syntax_const};
wenzelm
parents: 35100
diff changeset
   299
syntax constant (cf. 'syntax' command).
18cd034922ba added ML antiquotation @{syntax_const};
wenzelm
parents: 35100
diff changeset
   300
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 35009
diff changeset
   301
* Renamed old-style Drule.standard to Drule.export_without_context, to
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 35009
diff changeset
   302
emphasize that this is in no way a standard operation.
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 35009
diff changeset
   303
INCOMPATIBILITY.
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 35009
diff changeset
   304
34076
e3daf3c07381 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents: 34062
diff changeset
   305
* Curried take and drop in library.ML; negative length is interpreted
e3daf3c07381 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents: 34062
diff changeset
   306
as infinity (as in chop).  INCOMPATIBILITY.
e3daf3c07381 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents: 34062
diff changeset
   307
e3daf3c07381 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents: 34062
diff changeset
   308
* Subgoal.FOCUS (and variants): resulting goal state is normalized as
e3daf3c07381 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents: 34062
diff changeset
   309
usual for resolution.  Rare INCOMPATIBILITY.
e3daf3c07381 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents: 34062
diff changeset
   310
34259
2ba492b8b6e8 discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
wenzelm
parents: 34255
diff changeset
   311
* Discontinued old TheoryDataFun with its copy/init operation -- data
2ba492b8b6e8 discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
wenzelm
parents: 34255
diff changeset
   312
needs to be pure.  Functor Theory_Data_PP retains the traditional
2ba492b8b6e8 discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
wenzelm
parents: 34255
diff changeset
   313
Pretty.pp argument to merge, which is absent in the standard
2ba492b8b6e8 discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
wenzelm
parents: 34255
diff changeset
   314
Theory_Data version.
2ba492b8b6e8 discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
wenzelm
parents: 34255
diff changeset
   315
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35810
diff changeset
   316
* Renamed varify/unvarify operations to varify_global/unvarify_global
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35810
diff changeset
   317
to emphasize that these only work in a global situation (which is
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35810
diff changeset
   318
quite rare).
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35810
diff changeset
   319
36000
5560b2437789 configuration options admit dynamic default values;
wenzelm
parents: 35995
diff changeset
   320
* Configuration options now admit dynamic default values, depending on
5560b2437789 configuration options admit dynamic default values;
wenzelm
parents: 35995
diff changeset
   321
the context or even global references.
5560b2437789 configuration options admit dynamic default values;
wenzelm
parents: 35995
diff changeset
   322
33993
haftmann
parents: 33873
diff changeset
   323
34238
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   324
*** System ***
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   325
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   326
* Discontinued special HOL_USEDIR_OPTIONS for the main HOL image;
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   327
ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions.  Note that
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   328
proof terms are enabled unconditionally in the new HOL-Proofs image.
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   329
34255
2dd2547acb41 discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents: 34238
diff changeset
   330
* Discontinued old ISABELLE and ISATOOL environment settings (legacy
2dd2547acb41 discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents: 34238
diff changeset
   331
feature since Isabelle2009).  Use ISABELLE_PROCESS and ISABELLE_TOOL,
2dd2547acb41 discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents: 34238
diff changeset
   332
respectively.
2dd2547acb41 discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents: 34238
diff changeset
   333
34238
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   334
33993
haftmann
parents: 33873
diff changeset
   335
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   336
New in Isabelle2009-1 (December 2009)
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   337
-------------------------------------
30904
cc6a6047a10f back to non-release mode;
wenzelm
parents: 30855
diff changeset
   338
31547
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   339
*** General ***
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   340
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   341
* Discontinued old form of "escaped symbols" such as \\<forall>.  Only
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   342
one backslash should be used, even in ML sources.
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   343
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   344
30951
a6e26a248f03 formal declaration of undefined parameters after class instantiation
haftmann
parents: 30949
diff changeset
   345
*** Pure ***
a6e26a248f03 formal declaration of undefined parameters after class instantiation
haftmann
parents: 30949
diff changeset
   346
32846
29941e925c82 News entry: inheritance of mixins; print_interps.
ballarin
parents: 32775
diff changeset
   347
* Locale interpretation propagates mixins along the locale hierarchy.
29941e925c82 News entry: inheritance of mixins; print_interps.
ballarin
parents: 32775
diff changeset
   348
The currently only available mixins are the equations used to map
29941e925c82 News entry: inheritance of mixins; print_interps.
ballarin
parents: 32775
diff changeset
   349
local definitions to terms of the target domain of an interpretation.
29941e925c82 News entry: inheritance of mixins; print_interps.
ballarin
parents: 32775
diff changeset
   350
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   351
* Reactivated diagnostic command 'print_interps'.  Use "print_interps
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   352
loc" to print all interpretations of locale "loc" in the theory.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   353
Interpretations in proofs are not shown.
32846
29941e925c82 News entry: inheritance of mixins; print_interps.
ballarin
parents: 32775
diff changeset
   354
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32846
diff changeset
   355
* Thoroughly revised locales tutorial.  New section on conditional
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32846
diff changeset
   356
interpretation.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32846
diff changeset
   357
33843
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   358
* On instantiation of classes, remaining undefined class parameters
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   359
are formally declared.  INCOMPATIBILITY.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   360
30951
a6e26a248f03 formal declaration of undefined parameters after class instantiation
haftmann
parents: 30949
diff changeset
   361
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   362
*** Document preparation ***
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   363
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   364
* New generalized style concept for printing terms: @{foo (style) ...}
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   365
instead of @{foo_style style ...}  (old form is still retained for
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   366
backward compatibility).  Styles can be also applied for
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   367
antiquotations prop, term_type and typeof.
32891
d403b99287ff new generalized concept for term styles
haftmann
parents: 32846
diff changeset
   368
d403b99287ff new generalized concept for term styles
haftmann
parents: 32846
diff changeset
   369
30930
11010e5f18f0 tightended specification of class semiring_div
haftmann
parents: 30855
diff changeset
   370
*** HOL ***
11010e5f18f0 tightended specification of class semiring_div
haftmann
parents: 30855
diff changeset
   371
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   372
* New proof method "smt" for a combination of first-order logic with
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   373
equality, linear and nonlinear (natural/integer/real) arithmetic, and
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   374
fixed-size bitvectors; there is also basic support for higher-order
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   375
features (esp. lambda abstractions).  It is an incomplete decision
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   376
procedure based on external SMT solvers using the oracle mechanism;
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   377
for the SMT solver Z3, this method is proof-producing.  Certificates
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   378
are provided to avoid calling the external solvers solely for
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   379
re-checking proofs.  Due to a remote SMT service there is no need for
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   380
installing SMT solvers locally.  See src/HOL/SMT.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   381
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   382
* New commands to load and prove verification conditions generated by
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   383
the Boogie program verifier or derived systems (e.g. the Verifying C
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   384
Compiler (VCC) or Spec#).  See src/HOL/Boogie.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   385
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   386
* New counterexample generator tool 'nitpick' based on the Kodkod
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   387
relational model finder.  See src/HOL/Tools/Nitpick and
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   388
src/HOL/Nitpick_Examples.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   389
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   390
* New commands 'code_pred' and 'values' to invoke the predicate
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   391
compiler and to enumerate values of inductive predicates.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   392
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   393
* A tabled implementation of the reflexive transitive closure.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   394
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   395
* New implementation of quickcheck uses generic code generator;
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   396
default generators are provided for all suitable HOL types, records
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   397
and datatypes.  Old quickcheck can be re-activated importing theory
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   398
Library/SML_Quickcheck.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   399
33843
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   400
* New testing tool Mirabelle for automated proof tools.  Applies
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   401
several tools and tactics like sledgehammer, metis, or quickcheck, to
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   402
every proof step in a theory.  To be used in batch mode via the
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   403
"mirabelle" utility.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   404
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   405
* New proof method "sos" (sum of squares) for nonlinear real
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   406
arithmetic (originally due to John Harison). It requires theory
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   407
Library/Sum_Of_Squares.  It is not a complete decision procedure but
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   408
works well in practice on quantifier-free real arithmetic with +, -,
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   409
*, ^, =, <= and <, i.e. boolean combinations of equalities and
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   410
inequalities between polynomials.  It makes use of external
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   411
semidefinite programming solvers.  Method "sos" generates a
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   412
certificate that can be pasted into the proof thus avoiding the need
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   413
to call an external tool every time the proof is checked.  See
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   414
src/HOL/Library/Sum_Of_Squares.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   415
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   416
* New method "linarith" invokes existing linear arithmetic decision
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   417
procedure only.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   418
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   419
* New command 'atp_minimal' reduces result produced by Sledgehammer.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   420
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   421
* New Sledgehammer option "Full Types" in Proof General settings menu.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   422
Causes full type information to be output to the ATPs.  This slows
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   423
ATPs down considerably but eliminates a source of unsound "proofs"
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   424
that fail later.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   425
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   426
* New method "metisFT": A version of metis that uses full type
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   427
information in order to avoid failures of proof reconstruction.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   428
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   429
* New evaluator "approximate" approximates an real valued term using
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   430
the same method as the approximation method.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   431
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   432
* Method "approximate" now supports arithmetic expressions as
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   433
boundaries of intervals and implements interval splitting and Taylor
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   434
series expansion.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   435
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   436
* ML antiquotation @{code_datatype} inserts definition of a datatype
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   437
generated by the code generator; e.g. see src/HOL/Predicate.thy.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   438
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   439
* New theory SupInf of the supremum and infimum operators for sets of
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   440
reals.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   441
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   442
* New theory Probability, which contains a development of measure
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   443
theory, eventually leading to Lebesgue integration and probability.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   444
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   445
* Extended Multivariate Analysis to include derivation and Brouwer's
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   446
fixpoint theorem.
33843
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   447
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   448
* Reorganization of number theory, INCOMPATIBILITY:
33873
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
   449
  - new number theory development for nat and int, in theories Divides
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
   450
    and GCD as well as in new session Number_Theory
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
   451
  - some constants and facts now suffixed with _nat and _int
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
   452
    accordingly
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
   453
  - former session NumberTheory now named Old_Number_Theory, including
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
   454
    theories Legacy_GCD and Primes (prefer Number_Theory if possible)
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   455
  - moved theory Pocklington from src/HOL/Library to
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   456
    src/HOL/Old_Number_Theory
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32463
diff changeset
   457
33873
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
   458
* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
   459
lcm of finite and infinite sets. It is shown that they form a complete
32600
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   460
lattice.
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   461
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   462
* Class semiring_div requires superclass no_zero_divisors and proof of
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   463
div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   464
div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   465
generalized to class semiring_div, subsuming former theorems
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   466
zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   467
zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   468
INCOMPATIBILITY.
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   469
32588
5e06a1634e55 Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents: 32485
diff changeset
   470
* Refinements to lattice classes and sets:
32064
53ca12ff305d refinement of lattice classes
haftmann
parents: 31971
diff changeset
   471
  - less default intro/elim rules in locale variant, more default
53ca12ff305d refinement of lattice classes
haftmann
parents: 31971
diff changeset
   472
    intro/elim rules in class variant: more uniformity
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   473
  - lemma ge_sup_conv renamed to le_sup_iff, in accordance with
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   474
    le_inf_iff
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   475
  - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   476
    sup_aci)
32064
53ca12ff305d refinement of lattice classes
haftmann
parents: 31971
diff changeset
   477
  - renamed ACI to inf_sup_aci
32600
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   478
  - new class "boolean_algebra"
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   479
  - class "complete_lattice" moved to separate theory
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   480
    "Complete_Lattice"; corresponding constants (and abbreviations)
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   481
    renamed and with authentic syntax:
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   482
    Set.Inf ~>    Complete_Lattice.Inf
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   483
    Set.Sup ~>    Complete_Lattice.Sup
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   484
    Set.INFI ~>   Complete_Lattice.INFI
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   485
    Set.SUPR ~>   Complete_Lattice.SUPR
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   486
    Set.Inter ~>  Complete_Lattice.Inter
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   487
    Set.Union ~>  Complete_Lattice.Union
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   488
    Set.INTER ~>  Complete_Lattice.INTER
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   489
    Set.UNION ~>  Complete_Lattice.UNION
32600
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   490
  - authentic syntax for
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   491
    Set.Pow
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   492
    Set.image
32588
5e06a1634e55 Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents: 32485
diff changeset
   493
  - mere abbreviations:
5e06a1634e55 Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents: 32485
diff changeset
   494
    Set.empty               (for bot)
5e06a1634e55 Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents: 32485
diff changeset
   495
    Set.UNIV                (for top)
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   496
    Set.inter               (for inf, formerly Set.Int)
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   497
    Set.union               (for sup, formerly Set.Un)
32588
5e06a1634e55 Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents: 32485
diff changeset
   498
    Complete_Lattice.Inter  (for Inf)
5e06a1634e55 Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents: 32485
diff changeset
   499
    Complete_Lattice.Union  (for Sup)
32606
b5c3a8a75772 INTER and UNION are mere abbreviations for INFI and SUPR
haftmann
parents: 32600
diff changeset
   500
    Complete_Lattice.INTER  (for INFI)
b5c3a8a75772 INTER and UNION are mere abbreviations for INFI and SUPR
haftmann
parents: 32600
diff changeset
   501
    Complete_Lattice.UNION  (for SUPR)
32600
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
   502
  - object-logic definitions as far as appropriate
32217
haftmann
parents: 32216
diff changeset
   503
32691
cdf70f1fc9f9 added note on simp rules
haftmann
parents: 32686
diff changeset
   504
INCOMPATIBILITY.  Care is required when theorems Int_subset_iff or
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   505
Un_subset_iff are explicitly deleted as default simp rules; then also
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   506
their lattice counterparts le_inf_iff and le_sup_iff have to be
32691
cdf70f1fc9f9 added note on simp rules
haftmann
parents: 32686
diff changeset
   507
deleted to achieve the desired effect.
32064
53ca12ff305d refinement of lattice classes
haftmann
parents: 31971
diff changeset
   508
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   509
* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   510
rules by default any longer; the same applies to min_max.inf_absorb1
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   511
etc.  INCOMPATIBILITY.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   512
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   513
* Rules sup_Int_eq and sup_Un_eq are no longer declared as
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   514
pred_set_conv by default.  INCOMPATIBILITY.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   515
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   516
* Power operations on relations and functions are now one dedicated
32706
b68f3afdc137 NEWS; corrected spelling
haftmann
parents: 32697
diff changeset
   517
constant "compow" with infix syntax "^^".  Power operation on
31547
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   518
multiplicative monoids retains syntax "^" and is now defined generic
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   519
in class power.  INCOMPATIBILITY.
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   520
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   521
* Relation composition "R O S" now has a more standard argument order:
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   522
"R O S = {(x, z). EX y. (x, y) : R & (y, z) : S}".  INCOMPATIBILITY,
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   523
rewrite propositions with "S O R" --> "R O S". Proofs may occasionally
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   524
break, since the O_assoc rule was not rewritten like this.  Fix using
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   525
O_assoc[symmetric].  The same applies to the curried version "R OO S".
32427
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
   526
33057
764547b68538 inv_onto -> inv_into
nipkow
parents: 33037
diff changeset
   527
* Function "Inv" is renamed to "inv_into" and function "inv" is now an
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   528
abbreviation for "inv_into UNIV".  Lemmas are renamed accordingly.
32988
d1d4d7a08a66 Inv -> inv_onto, inv abbr. inv_onto UNIV.
nipkow
parents: 32898
diff changeset
   529
INCOMPATIBILITY.
d1d4d7a08a66 Inv -> inv_onto, inv abbr. inv_onto UNIV.
nipkow
parents: 32898
diff changeset
   530
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   531
* Most rules produced by inductive and datatype package have mandatory
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   532
prefixes.  INCOMPATIBILITY.
31790
05c92381363c corrected and unified thm names
nipkow
parents: 31784
diff changeset
   533
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   534
* Changed "DERIV_intros" to a dynamic fact, which can be augmented by
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   535
the attribute of the same name.  Each of the theorems in the list
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   536
DERIV_intros assumes composition with an additional function and
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   537
matches a variable to the derivative, which has to be solved by the
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   538
Simplifier.  Hence (auto intro!: DERIV_intros) computes the derivative
33873
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
   539
of most elementary terms.  Former Maclauren.DERIV_tac and
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
   540
Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros).
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
   541
INCOMPATIBILITY.
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   542
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   543
* Code generator attributes follow the usual underscore convention:
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   544
    code_unfold     replaces    code unfold
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   545
    code_post       replaces    code post
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   546
    etc.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   547
  INCOMPATIBILITY.
31900
7c35d9ad0349 misc tuning;
wenzelm
parents: 31884
diff changeset
   548
33471
5aef13872723 renamed method induct_scheme to induction_schema
krauss
parents: 33470
diff changeset
   549
* Renamed methods:
5aef13872723 renamed method induct_scheme to induction_schema
krauss
parents: 33470
diff changeset
   550
    sizechange -> size_change
5aef13872723 renamed method induct_scheme to induction_schema
krauss
parents: 33470
diff changeset
   551
    induct_scheme -> induction_schema
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   552
  INCOMPATIBILITY.
33673
nipkow
parents: 33649
diff changeset
   553
33843
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   554
* Discontinued abbreviation "arbitrary" of constant "undefined".
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   555
INCOMPATIBILITY, use "undefined" directly.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   556
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   557
* Renamed theorems:
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   558
    Suc_eq_add_numeral_1 -> Suc_eq_plus1
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   559
    Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   560
    Suc_plus1 -> Suc_eq_plus1
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   561
    *anti_sym -> *antisym*
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   562
    vector_less_eq_def -> vector_le_def
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   563
  INCOMPATIBILITY.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   564
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   565
* Added theorem List.map_map as [simp].  Removed List.map_compose.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   566
INCOMPATIBILITY.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   567
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   568
* Removed predicate "M hassize n" (<--> card M = n & finite M).
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   569
INCOMPATIBILITY.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   570
31812
73dc3a98669c NEWS updated
hoelzl
parents: 31810
diff changeset
   571
33825
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   572
*** HOLCF ***
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   573
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   574
* Theory Representable defines a class "rep" of domains that are
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   575
representable (via an ep-pair) in the universal domain type "udom".
33825
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   576
Instances are provided for all type constructors defined in HOLCF.
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   577
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   578
* The 'new_domain' command is a purely definitional version of the
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   579
domain package, for representable domains.  Syntax is identical to the
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   580
old domain package.  The 'new_domain' package also supports indirect
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   581
recursion using previously-defined type constructors.  See
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   582
src/HOLCF/ex/New_Domain.thy for examples.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   583
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   584
* Method "fixrec_simp" unfolds one step of a fixrec-defined constant
33825
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   585
on the left-hand side of an equation, and then performs
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   586
simplification.  Rewriting is done using rules declared with the
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   587
"fixrec_simp" attribute.  The "fixrec_simp" method is intended as a
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   588
replacement for "fixpat"; see src/HOLCF/ex/Fixrec_ex.thy for examples.
33825
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   589
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   590
* The pattern-match compiler in 'fixrec' can now handle constructors
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   591
with HOL function types.  Pattern-match combinators for the Pair
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   592
constructor are pre-configured.
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   593
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   594
* The 'fixrec' package now produces better fixed-point induction rules
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   595
for mutually-recursive definitions:  Induction rules have conclusions
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   596
of the form "P foo bar" instead of "P <foo, bar>".
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   597
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   598
* The constant "sq_le" (with infix syntax "<<" or "\<sqsubseteq>") has
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   599
been renamed to "below".  The name "below" now replaces "less" in many
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   600
theorem names.  (Legacy theorem names using "less" are still supported
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   601
as well.)
33825
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   602
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   603
* The 'fixrec' package now supports "bottom patterns".  Bottom
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   604
patterns can be used to generate strictness rules, or to make
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   605
functions more strict (much like the bang-patterns supported by the
33873
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
   606
Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
   607
examples.
33825
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   608
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
   609
31304
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31001
diff changeset
   610
*** ML ***
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31001
diff changeset
   611
33843
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   612
* Support for Poly/ML 5.3.0, with improved reporting of compiler
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   613
errors and run-time exceptions, including detailed source positions.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   614
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   615
* Structure Name_Space (formerly NameSpace) now manages uniquely
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   616
identified entries, with some additional information such as source
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   617
position, logical grouping etc.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   618
33524
a08e6c1cbc04 updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents: 33472
diff changeset
   619
* Theory and context data is now introduced by the simplified and
a08e6c1cbc04 updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents: 33472
diff changeset
   620
modernized functors Theory_Data, Proof_Data, Generic_Data.  Data needs
a08e6c1cbc04 updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents: 33472
diff changeset
   621
to be pure, but the old TheoryDataFun for mutable data (with explicit
a08e6c1cbc04 updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents: 33472
diff changeset
   622
copy operation) is still available for some time.
a08e6c1cbc04 updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents: 33472
diff changeset
   623
32742
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
   624
* Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
   625
provides a high-level programming interface to synchronized state
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
   626
variables with atomic update.  This works via pure function
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
   627
application within a critical section -- its runtime should be as
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
   628
short as possible; beware of deadlocks if critical code is nested,
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
   629
either directly or indirectly via other synchronized variables!
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
   630
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
   631
* Structure Unsynchronized (cf. src/Pure/ML-Systems/unsynchronized.ML)
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
   632
wraps raw ML references, explicitly indicating their non-thread-safe
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
   633
behaviour.  The Isar toplevel keeps this structure open, to
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
   634
accommodate Proof General as well as quick and dirty interactive
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
   635
experiments with references.
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
   636
32365
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32326
diff changeset
   637
* PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32326
diff changeset
   638
parallel tactical reasoning.
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32326
diff changeset
   639
32427
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
   640
* Tacticals Subgoal.FOCUS, Subgoal.FOCUS_PREMS, Subgoal.FOCUS_PARAMS
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
   641
are similar to SUBPROOF, but are slightly more flexible: only the
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
   642
specified parts of the subgoal are imported into the context, and the
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
   643
body tactic may introduce new subgoals and schematic variables.
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
   644
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
   645
* Old tactical METAHYPS, which does not observe the proof context, has
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
   646
been renamed to Old_Goals.METAHYPS and awaits deletion.  Use SUBPROOF
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
   647
or Subgoal.FOCUS etc.
32216
2f3d65d15149 tacticals FOCUS and FOCUS_PARAMS;
wenzelm
parents: 32151
diff changeset
   648
31971
8c1b845ed105 renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents: 31901
diff changeset
   649
* Renamed functor TableFun to Table, and GraphFun to Graph.  (Since
8c1b845ed105 renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents: 31901
diff changeset
   650
functors have their own ML name space there is no point to mark them
8c1b845ed105 renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents: 31901
diff changeset
   651
separately.)  Minor INCOMPATIBILITY.
8c1b845ed105 renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents: 31901
diff changeset
   652
31901
e280491f36b8 renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 31900
diff changeset
   653
* Renamed NamedThmsFun to Named_Thms.  INCOMPATIBILITY.
e280491f36b8 renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 31900
diff changeset
   654
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   655
* Renamed several structures FooBar to Foo_Bar.  Occasional,
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   656
INCOMPATIBILITY.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   657
33843
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   658
* Operations of structure Skip_Proof no longer require quick_and_dirty
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   659
mode, which avoids critical setmp.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   660
31306
a74ee84288a0 eliminated old Attrib.add_attributes (and Attrib.syntax);
wenzelm
parents: 31304
diff changeset
   661
* Eliminated old Attrib.add_attributes, Method.add_methods and related
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   662
combinators for "args".  INCOMPATIBILITY, need to use simplified
31306
a74ee84288a0 eliminated old Attrib.add_attributes (and Attrib.syntax);
wenzelm
parents: 31304
diff changeset
   663
Attrib/Method.setup introduced in Isabelle2009.
31304
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31001
diff changeset
   664
32151
2f65c45c2e7e Proper context for simpset_of, claset_of, clasimpset_of.
wenzelm
parents: 32136
diff changeset
   665
* Proper context for simpset_of, claset_of, clasimpset_of.  May fall
2f65c45c2e7e Proper context for simpset_of, claset_of, clasimpset_of.
wenzelm
parents: 32136
diff changeset
   666
back on global_simpset_of, global_claset_of, global_clasimpset_of as
2f65c45c2e7e Proper context for simpset_of, claset_of, clasimpset_of.
wenzelm
parents: 32136
diff changeset
   667
last resort.  INCOMPATIBILITY.
2f65c45c2e7e Proper context for simpset_of, claset_of, clasimpset_of.
wenzelm
parents: 32136
diff changeset
   668
32092
6a5995438266 Display.pretty_thm now requires a proper context;
wenzelm
parents: 32079
diff changeset
   669
* Display.pretty_thm now requires a proper context (cf. former
6a5995438266 Display.pretty_thm now requires a proper context;
wenzelm
parents: 32079
diff changeset
   670
ProofContext.pretty_thm).  May fall back on Display.pretty_thm_global
6a5995438266 Display.pretty_thm now requires a proper context;
wenzelm
parents: 32079
diff changeset
   671
or even Display.pretty_thm_without_context as last resort.
6a5995438266 Display.pretty_thm now requires a proper context;
wenzelm
parents: 32079
diff changeset
   672
INCOMPATIBILITY.
6a5995438266 Display.pretty_thm now requires a proper context;
wenzelm
parents: 32079
diff changeset
   673
32433
11661f4327bb discontinued Display.pretty_ctyp/cterm etc.;
wenzelm
parents: 32427
diff changeset
   674
* Discontinued Display.pretty_ctyp/cterm etc.  INCOMPATIBILITY, use
11661f4327bb discontinued Display.pretty_ctyp/cterm etc.;
wenzelm
parents: 32427
diff changeset
   675
Syntax.pretty_typ/term directly, preferably with proper context
11661f4327bb discontinued Display.pretty_ctyp/cterm etc.;
wenzelm
parents: 32427
diff changeset
   676
instead of global theory.
11661f4327bb discontinued Display.pretty_ctyp/cterm etc.;
wenzelm
parents: 32427
diff changeset
   677
31304
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31001
diff changeset
   678
31308
3fd52453ae81 discontinued support for Poly/ML 4.x versions;
wenzelm
parents: 31306
diff changeset
   679
*** System ***
3fd52453ae81 discontinued support for Poly/ML 4.x versions;
wenzelm
parents: 31306
diff changeset
   680
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   681
* Further fine tuning of parallel proof checking, scales up to 8 cores
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   682
(max. speedup factor 5.0).  See also Goal.parallel_proofs in ML and
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   683
usedir option -q.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   684
32326
9d70ecf11b7a etc/components;
wenzelm
parents: 32270
diff changeset
   685
* Support for additional "Isabelle components" via etc/components, see
9d70ecf11b7a etc/components;
wenzelm
parents: 32270
diff changeset
   686
also the system manual.
9d70ecf11b7a etc/components;
wenzelm
parents: 32270
diff changeset
   687
9d70ecf11b7a etc/components;
wenzelm
parents: 32270
diff changeset
   688
* The isabelle makeall tool now operates on all components with
9d70ecf11b7a etc/components;
wenzelm
parents: 32270
diff changeset
   689
IsaMakefile, not just hardwired "logics".
9d70ecf11b7a etc/components;
wenzelm
parents: 32270
diff changeset
   690
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   691
* Removed "compress" option from isabelle-process and isabelle usedir;
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   692
this is always enabled.
33818
aa00c583f594 added NEWS item for wwwfind
kleing
parents: 33759
diff changeset
   693
31308
3fd52453ae81 discontinued support for Poly/ML 4.x versions;
wenzelm
parents: 31306
diff changeset
   694
* Discontinued support for Poly/ML 4.x versions.
3fd52453ae81 discontinued support for Poly/ML 4.x versions;
wenzelm
parents: 31306
diff changeset
   695
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   696
* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   697
on a given logic image.  This requires the lighttpd webserver and is
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   698
currently supported on Linux only.
32061
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 31997
diff changeset
   699
31308
3fd52453ae81 discontinued support for Poly/ML 4.x versions;
wenzelm
parents: 31306
diff changeset
   700
31304
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31001
diff changeset
   701
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   702
New in Isabelle2009 (April 2009)
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   703
--------------------------------
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27067
diff changeset
   704
27599
ca23ef50c178 added command 'linear_undo';
wenzelm
parents: 27556
diff changeset
   705
*** General ***
ca23ef50c178 added command 'linear_undo';
wenzelm
parents: 27556
diff changeset
   706
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   707
* Simplified main Isabelle executables, with less surprises on
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   708
case-insensitive file-systems (such as Mac OS).
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   709
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   710
  - The main Isabelle tool wrapper is now called "isabelle" instead of
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   711
    "isatool."
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   712
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   713
  - The former "isabelle" alias for "isabelle-process" has been
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   714
    removed (should rarely occur to regular users).
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   715
28915
0642cbb60c98 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents: 28914
diff changeset
   716
  - The former "isabelle-interface" and its alias "Isabelle" have been
0642cbb60c98 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents: 28914
diff changeset
   717
    removed (interfaces are now regular Isabelle tools).
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   718
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   719
Within scripts and make files, the Isabelle environment variables
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   720
ISABELLE_TOOL and ISABELLE_PROCESS replace old ISATOOL and ISABELLE,
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   721
respectively.  (The latter are still available as legacy feature.)
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   722
28915
0642cbb60c98 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents: 28914
diff changeset
   723
The old isabelle-interface wrapper could react in confusing ways if
0642cbb60c98 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents: 28914
diff changeset
   724
the interface was uninstalled or changed otherwise.  Individual
0642cbb60c98 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents: 28914
diff changeset
   725
interface tool configuration is now more explicit, see also the
0642cbb60c98 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents: 28914
diff changeset
   726
Isabelle system manual.  In particular, Proof General is now available
0642cbb60c98 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents: 28914
diff changeset
   727
via "isabelle emacs".
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   728
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   729
INCOMPATIBILITY, need to adapt derivative scripts.  Users may need to
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   730
purge installed copies of Isabelle executables and re-run "isabelle
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   731
install -p ...", or use symlinks.
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
   732
28914
f993cbffc42a default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents: 28856
diff changeset
   733
* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   734
old ~/isabelle, which was slightly non-standard and apt to cause
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   735
surprises on case-insensitive file-systems (such as Mac OS).
28914
f993cbffc42a default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents: 28856
diff changeset
   736
f993cbffc42a default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents: 28856
diff changeset
   737
INCOMPATIBILITY, need to move existing ~/isabelle/etc,
f993cbffc42a default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents: 28856
diff changeset
   738
~/isabelle/heaps, ~/isabelle/browser_info to the new place.  Special
f993cbffc42a default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents: 28856
diff changeset
   739
care is required when using older releases of Isabelle.  Note that
f993cbffc42a default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents: 28856
diff changeset
   740
ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   741
Isabelle distribution, in order to use the new ~/.isabelle uniformly.
28914
f993cbffc42a default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents: 28856
diff changeset
   742
29161
9903e84a9c9c * Proofs of are run in parallel on multi-core systems;
wenzelm
parents: 29145
diff changeset
   743
* Proofs of fully specified statements are run in parallel on
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   744
multi-core systems.  A speedup factor of 2.5 to 3.2 can be expected on
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   745
a regular 4-core machine, if the initial heap space is made reasonably
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   746
large (cf. Poly/ML option -H).  (Requires Poly/ML 5.2.1 or later.)
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   747
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   748
* The main reference manuals ("isar-ref", "implementation", and
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   749
"system") have been updated and extended.  Formally checked references
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   750
as hyperlinks are now available uniformly.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   751
30163
faf95eb3f375 * New prover for coherent logic (see src/Tools/coherent.ML).
wenzelm
parents: 30106
diff changeset
   752
27599
ca23ef50c178 added command 'linear_undo';
wenzelm
parents: 27556
diff changeset
   753
*** Pure ***
ca23ef50c178 added command 'linear_undo';
wenzelm
parents: 27556
diff changeset
   754
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   755
* Complete re-implementation of locales.  INCOMPATIBILITY in several
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   756
respects.  The most important changes are listed below.  See the
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   757
Tutorial on Locales ("locales" manual) for details.
29253
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   758
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   759
- In locale expressions, instantiation replaces renaming.  Parameters
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   760
must be declared in a for clause.  To aid compatibility with previous
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   761
parameter inheritance, in locale declarations, parameters that are not
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   762
'touched' (instantiation position "_" or omitted) are implicitly added
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   763
with their syntax at the beginning of the for clause.
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   764
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   765
- Syntax from abbreviations and definitions in locales is available in
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   766
locale expressions and context elements.  The latter is particularly
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   767
useful in locale declarations.
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   768
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   769
- More flexible mechanisms to qualify names generated by locale
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   770
expressions.  Qualifiers (prefixes) may be specified in locale
30728
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
   771
expressions, and can be marked as mandatory (syntax: "name!:") or
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
   772
optional (syntax "name?:").  The default depends for plain "name:"
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
   773
depends on the situation where a locale expression is used: in
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
   774
commands 'locale' and 'sublocale' prefixes are optional, in
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   775
'interpretation' and 'interpret' prefixes are mandatory.  The old
30728
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
   776
implicit qualifiers derived from the parameter names of a locale are
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
   777
no longer generated.
30106
351fc2f8493d tuned NEWS;
wenzelm
parents: 30085
diff changeset
   778
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   779
- Command "sublocale l < e" replaces "interpretation l < e".  The
30106
351fc2f8493d tuned NEWS;
wenzelm
parents: 30085
diff changeset
   780
instantiation clause in "interpretation" and "interpret" (square
351fc2f8493d tuned NEWS;
wenzelm
parents: 30085
diff changeset
   781
brackets) is no longer available.  Use locale expressions.
29253
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
   782
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   783
- When converting proof scripts, mandatory qualifiers in
30728
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
   784
'interpretation' and 'interpret' should be retained by default, even
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   785
if this is an INCOMPATIBILITY compared to former behavior.  In the
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   786
worst case, use the "name?:" form for non-mandatory ones.  Qualifiers
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   787
in locale expressions range over a single locale instance only.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   788
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   789
- Dropped locale element "includes".  This is a major INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   790
In existing theorem specifications replace the includes element by the
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   791
respective context elements of the included locale, omitting those
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   792
that are already present in the theorem specification.  Multiple
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   793
assume elements of a locale should be replaced by a single one
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   794
involving the locale predicate.  In the proof body, declarations (most
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   795
notably theorems) may be regained by interpreting the respective
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   796
locales in the proof context as required (command "interpret").
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   797
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   798
If using "includes" in replacement of a target solely because the
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   799
parameter types in the theorem are not as general as in the target,
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   800
consider declaring a new locale with additional type constraints on
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   801
the parameters (context element "constrains").
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   802
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   803
- Discontinued "locale (open)".  INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   804
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   805
- Locale interpretation commands no longer attempt to simplify goal.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   806
INCOMPATIBILITY: in rare situations the generated goal differs.  Use
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   807
methods intro_locales and unfold_locales to clarify.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   808
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   809
- Locale interpretation commands no longer accept interpretation
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   810
attributes.  INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   811
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   812
* Class declaration: so-called "base sort" must not be given in import
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   813
list any longer, but is inferred from the specification.  Particularly
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   814
in HOL, write
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   815
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   816
    class foo = ...
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   817
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   818
instead of
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   819
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   820
    class foo = type + ...
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   821
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   822
* Class target: global versions of theorems stemming do not carry a
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   823
parameter prefix any longer.  INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   824
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   825
* Class 'instance' command no longer accepts attached definitions.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   826
INCOMPATIBILITY, use proper 'instantiation' target instead.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   827
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   828
* Recovered hiding of consts, which was accidentally broken in
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   829
Isabelle2007.  Potential INCOMPATIBILITY, ``hide const c'' really
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   830
makes c inaccessible; consider using ``hide (open) const c'' instead.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   831
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   832
* Slightly more coherent Pure syntax, with updated documentation in
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   833
isar-ref manual.  Removed locales meta_term_syntax and
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   834
meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   835
INCOMPATIBILITY in rare situations.  Note that &&& should not be used
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   836
directly in regular applications.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   837
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   838
* There is a new syntactic category "float_const" for signed decimal
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   839
fractions (e.g. 123.45 or -123.45).
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   840
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   841
* Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   842
interface with 'setup' command instead.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   843
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   844
* Command 'local_setup' is similar to 'setup', but operates on a local
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   845
theory context.
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27067
diff changeset
   846
28114
2637fb838f74 axiomatization is now global-only;
wenzelm
parents: 28103
diff changeset
   847
* The 'axiomatization' command now only works within a global theory
2637fb838f74 axiomatization is now global-only;
wenzelm
parents: 28103
diff changeset
   848
context.  INCOMPATIBILITY.
2637fb838f74 axiomatization is now global-only;
wenzelm
parents: 28103
diff changeset
   849
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   850
* Goal-directed proof now enforces strict proof irrelevance wrt. sort
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   851
hypotheses.  Sorts required in the course of reasoning need to be
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   852
covered by the constraints in the initial statement, completed by the
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   853
type instance information of the background theory.  Non-trivial sort
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   854
hypotheses, which rarely occur in practice, may be specified via
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   855
vacuous propositions of the form SORT_CONSTRAINT('a::c).  For example:
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   856
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   857
  lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ...
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   858
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   859
The result contains an implicit sort hypotheses as before --
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   860
SORT_CONSTRAINT premises are eliminated as part of the canonical rule
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   861
normalization.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   862
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   863
* Generalized Isar history, with support for linear undo, direct state
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   864
addressing etc.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   865
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   866
* Changed defaults for unify configuration options:
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   867
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   868
  unify_trace_bound = 50 (formerly 25)
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   869
  unify_search_bound = 60 (formerly 30)
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   870
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   871
* Different bookkeeping for code equations (INCOMPATIBILITY):
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   872
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   873
  a) On theory merge, the last set of code equations for a particular
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   874
     constant is taken (in accordance with the policy applied by other
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   875
     parts of the code generator framework).
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   876
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   877
  b) Code equations stemming from explicit declarations (e.g. code
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   878
     attribute) gain priority over default code equations stemming
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   879
     from definition, primrec, fun etc.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   880
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   881
* Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   882
30965
e0938d929bfd dropped duplication
haftmann
parents: 30964
diff changeset
   883
* Unified theorem tables for both code generators.  Thus [code
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   884
func] has disappeared and only [code] remains.  INCOMPATIBILITY.
30577
wenzelm
parents: 30562
diff changeset
   885
wenzelm
parents: 30562
diff changeset
   886
* Command 'find_consts' searches for constants based on type and name
wenzelm
parents: 30562
diff changeset
   887
patterns, e.g.
29883
14841d4c808e added find_consts to NEWS and CONTRIBUTORS
kleing
parents: 29862
diff changeset
   888
14841d4c808e added find_consts to NEWS and CONTRIBUTORS
kleing
parents: 29862
diff changeset
   889
    find_consts "_ => bool"
14841d4c808e added find_consts to NEWS and CONTRIBUTORS
kleing
parents: 29862
diff changeset
   890
30106
351fc2f8493d tuned NEWS;
wenzelm
parents: 30085
diff changeset
   891
By default, matching is against subtypes, but it may be restricted to
30728
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
   892
the whole type.  Searching by name is possible.  Multiple queries are
30106
351fc2f8493d tuned NEWS;
wenzelm
parents: 30085
diff changeset
   893
conjunctive and queries may be negated by prefixing them with a
351fc2f8493d tuned NEWS;
wenzelm
parents: 30085
diff changeset
   894
hyphen:
29883
14841d4c808e added find_consts to NEWS and CONTRIBUTORS
kleing
parents: 29862
diff changeset
   895
14841d4c808e added find_consts to NEWS and CONTRIBUTORS
kleing
parents: 29862
diff changeset
   896
    find_consts strict: "_ => bool" name: "Int" -"int => int"
29861
3c348f5873f3 updated NEWS etc with "solves" criterion and auto_solves
kleing
parents: 29823
diff changeset
   897
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   898
* New 'find_theorems' criterion "solves" matches theorems that
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   899
directly solve the current goal (modulo higher-order unification).
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   900
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   901
* Auto solve feature for main theorem statements: whenever a new goal
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   902
is stated, "find_theorems solves" is called; any theorems that could
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   903
solve the lemma directly are listed as part of the goal state.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   904
Cf. associated options in Proof General Isabelle settings menu,
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   905
enabled by default, with reasonable timeout for pathological cases of
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   906
higher-order unification.
30415
9501af91c4a3 Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents: 30399
diff changeset
   907
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27067
diff changeset
   908
27381
19ae7064f00f @{lemma}: 'by' keyword;
wenzelm
parents: 27380
diff changeset
   909
*** Document preparation ***
19ae7064f00f @{lemma}: 'by' keyword;
wenzelm
parents: 27380
diff changeset
   910
19ae7064f00f @{lemma}: 'by' keyword;
wenzelm
parents: 27380
diff changeset
   911
* Antiquotation @{lemma} now imitates a regular terminal proof,
27392
wenzelm
parents: 27391
diff changeset
   912
demanding keyword 'by' and supporting the full method expression
27519
59b54d80d2ae slightly improved @{lemma} (both for latex and ML);
wenzelm
parents: 27485
diff changeset
   913
syntax just like the Isar command 'by'.
27381
19ae7064f00f @{lemma}: 'by' keyword;
wenzelm
parents: 27380
diff changeset
   914
19ae7064f00f @{lemma}: 'by' keyword;
wenzelm
parents: 27380
diff changeset
   915
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27067
diff changeset
   916
*** HOL ***
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27067
diff changeset
   917
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   918
* Integrated main parts of former image HOL-Complex with HOL.  Entry
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   919
points Main and Complex_Main remain as before.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   920
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   921
* Logic image HOL-Plain provides a minimal HOL with the most important
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   922
tools available (inductive, datatype, primrec, ...).  This facilitates
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   923
experimentation and tool development.  Note that user applications
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   924
(and library theories) should never refer to anything below theory
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   925
Main, as before.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   926
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   927
* Logic image HOL-Main stops at theory Main, and thus facilitates
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   928
experimentation due to shorter build times.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   929
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   930
* Logic image HOL-NSA contains theories of nonstandard analysis which
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   931
were previously part of former HOL-Complex.  Entry point Hyperreal
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   932
remains valid, but theories formerly using Complex_Main should now use
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   933
new entry point Hypercomplex.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   934
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   935
* Generic ATP manager for Sledgehammer, based on ML threads instead of
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   936
Posix processes.  Avoids potentially expensive forking of the ML
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   937
process.  New thread-based implementation also works on non-Unix
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   938
platforms (Cygwin).  Provers are no longer hardwired, but defined
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   939
within the theory via plain ML wrapper functions.  Basic Sledgehammer
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   940
commands are covered in the isar-ref manual.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   941
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   942
* Wrapper scripts for remote SystemOnTPTP service allows to use
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   943
sledgehammer without local ATP installation (Vampire etc.). Other
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   944
provers may be included via suitable ML wrappers, see also
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   945
src/HOL/ATP_Linkup.thy.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   946
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   947
* ATP selection (E/Vampire/Spass) is now via Proof General's settings
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   948
menu.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   949
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   950
* The metis method no longer fails because the theorem is too trivial
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   951
(contains the empty clause).
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   952
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   953
* The metis method now fails in the usual manner, rather than raising
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   954
an exception, if it determines that it cannot prove the theorem.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   955
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   956
* Method "coherent" implements a prover for coherent logic (see also
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   957
src/Tools/coherent.ML).
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   958
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   959
* Constants "undefined" and "default" replace "arbitrary".  Usually
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   960
"undefined" is the right choice to replace "arbitrary", though
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   961
logically there is no difference.  INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   962
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   963
* Command "value" now integrates different evaluation mechanisms.  The
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   964
result of the first successful evaluation mechanism is printed.  In
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   965
square brackets a particular named evaluation mechanisms may be
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   966
specified (currently, [SML], [code] or [nbe]).  See further
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   967
src/HOL/ex/Eval_Examples.thy.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   968
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   969
* Normalization by evaluation now allows non-leftlinear equations.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   970
Declare with attribute [code nbe].
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   971
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   972
* Methods "case_tac" and "induct_tac" now refer to the very same rules
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   973
as the structured Isar versions "cases" and "induct", cf. the
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   974
corresponding "cases" and "induct" attributes.  Mutual induction rules
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   975
are now presented as a list of individual projections
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   976
(e.g. foo_bar.inducts for types foo and bar); the old format with
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   977
explicit HOL conjunction is no longer supported.  INCOMPATIBILITY, in
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   978
rare situations a different rule is selected --- notably nested tuple
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   979
elimination instead of former prod.exhaust: use explicit (case_tac t
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   980
rule: prod.exhaust) here.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   981
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   982
* Attributes "cases", "induct", "coinduct" support "del" option.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   983
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   984
* Removed fact "case_split_thm", which duplicates "case_split".
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   985
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   986
* The option datatype has been moved to a new theory Option.  Renamed
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   987
option_map to Option.map, and o2s to Option.set, INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   988
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   989
* New predicate "strict_mono" classifies strict functions on partial
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   990
orders.  With strict functions on linear orders, reasoning about
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   991
(in)equalities is facilitated by theorems "strict_mono_eq",
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   992
"strict_mono_less_eq" and "strict_mono_less".
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   993
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   994
* Some set operations are now proper qualified constants with
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
   995
authentic syntax.  INCOMPATIBILITY:
30304
d8e4cd2ac2a1 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents: 30085
diff changeset
   996
d8e4cd2ac2a1 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents: 30085
diff changeset
   997
    op Int ~>   Set.Int
d8e4cd2ac2a1 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents: 30085
diff changeset
   998
    op Un ~>    Set.Un
d8e4cd2ac2a1 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents: 30085
diff changeset
   999
    INTER ~>    Set.INTER
d8e4cd2ac2a1 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents: 30085
diff changeset
  1000
    UNION ~>    Set.UNION
d8e4cd2ac2a1 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents: 30085
diff changeset
  1001
    Inter ~>    Set.Inter
d8e4cd2ac2a1 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents: 30085
diff changeset
  1002
    Union ~>    Set.Union
d8e4cd2ac2a1 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents: 30085
diff changeset
  1003
    {} ~>       Set.empty
d8e4cd2ac2a1 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents: 30085
diff changeset
  1004
    UNIV ~>     Set.UNIV
d8e4cd2ac2a1 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents: 30085
diff changeset
  1005
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1006
* Class complete_lattice with operations Inf, Sup, INFI, SUPR now in
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1007
theory Set.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1008
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1009
* Auxiliary class "itself" has disappeared -- classes without any
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1010
parameter are treated as expected by the 'class' command.
29797
08ef36ed2f8a handling type classes without parameters
haftmann
parents: 29788
diff changeset
  1011
29823
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29810
diff changeset
  1012
* Leibnitz's Series for Pi and the arcus tangens and logarithm series.
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29810
diff changeset
  1013
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1014
* Common decision procedures (Cooper, MIR, Ferrack, Approximation,
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1015
Dense_Linear_Order) are now in directory HOL/Decision_Procs.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1016
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1017
* Theory src/HOL/Decision_Procs/Approximation provides the new proof
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1018
method "approximation".  It proves formulas on real values by using
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1019
interval arithmetic.  In the formulas are also the transcendental
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1020
functions sin, cos, tan, atan, ln, exp and the constant pi are
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1021
allowed. For examples see
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1022
src/HOL/Descision_Procs/ex/Approximation_Ex.thy.
29823
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29810
diff changeset
  1023
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29810
diff changeset
  1024
* Theory "Reflection" now resides in HOL/Library.
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 29628
diff changeset
  1025
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1026
* Entry point to Word library now simply named "Word".
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1027
INCOMPATIBILITY.
29628
d9294387ab0e entry point for Word library now named Word
haftmann
parents: 29616
diff changeset
  1028
29197
6d4cb27ed19c adapted HOL source structure to distribution layout
haftmann
parents: 29182
diff changeset
  1029
* Made source layout more coherent with logical distribution
6d4cb27ed19c adapted HOL source structure to distribution layout
haftmann
parents: 29182
diff changeset
  1030
structure:
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1031
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1032
    src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1033
    src/HOL/Library/Code_Message.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1034
    src/HOL/Library/GCD.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1035
    src/HOL/Library/Order_Relation.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1036
    src/HOL/Library/Parity.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1037
    src/HOL/Library/Univ_Poly.thy ~> src/HOL/
30176
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1038
    src/HOL/Real/ContNotDenum.thy ~> src/HOL/Library/
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1039
    src/HOL/Real/Lubs.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1040
    src/HOL/Real/PReal.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1041
    src/HOL/Real/Rational.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1042
    src/HOL/Real/RComplete.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1043
    src/HOL/Real/RealDef.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1044
    src/HOL/Real/RealPow.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1045
    src/HOL/Real/Real.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1046
    src/HOL/Complex/Complex_Main.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1047
    src/HOL/Complex/Complex.thy ~> src/HOL/
30176
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1048
    src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/Library/
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1049
    src/HOL/Complex/Fundamental_Theorem_Algebra.thy ~> src/HOL/Library/
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1050
    src/HOL/Hyperreal/Deriv.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1051
    src/HOL/Hyperreal/Fact.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1052
    src/HOL/Hyperreal/Integration.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1053
    src/HOL/Hyperreal/Lim.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1054
    src/HOL/Hyperreal/Ln.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1055
    src/HOL/Hyperreal/Log.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1056
    src/HOL/Hyperreal/MacLaurin.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1057
    src/HOL/Hyperreal/NthRoot.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1058
    src/HOL/Hyperreal/Series.thy ~> src/HOL/
29197
6d4cb27ed19c adapted HOL source structure to distribution layout
haftmann
parents: 29182
diff changeset
  1059
    src/HOL/Hyperreal/SEQ.thy ~> src/HOL/
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1060
    src/HOL/Hyperreal/Taylor.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1061
    src/HOL/Hyperreal/Transcendental.thy ~> src/HOL/
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1062
    src/HOL/Real/Float ~> src/HOL/Library/
29197
6d4cb27ed19c adapted HOL source structure to distribution layout
haftmann
parents: 29182
diff changeset
  1063
    src/HOL/Real/HahnBanach ~> src/HOL/HahnBanach
6d4cb27ed19c adapted HOL source structure to distribution layout
haftmann
parents: 29182
diff changeset
  1064
    src/HOL/Real/RealVector.thy ~> src/HOL/
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1065
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1066
    src/HOL/arith_data.ML ~> src/HOL/Tools
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1067
    src/HOL/hologic.ML ~> src/HOL/Tools
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1068
    src/HOL/simpdata.ML ~> src/HOL/Tools
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1069
    src/HOL/int_arith1.ML ~> src/HOL/Tools/int_arith.ML
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1070
    src/HOL/int_factor_simprocs.ML ~> src/HOL/Tools
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1071
    src/HOL/nat_simprocs.ML ~> src/HOL/Tools
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1072
    src/HOL/Real/float_arith.ML ~> src/HOL/Tools
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1073
    src/HOL/Real/float_syntax.ML ~> src/HOL/Tools
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1074
    src/HOL/Real/rat_arith.ML ~> src/HOL/Tools
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1075
    src/HOL/Real/real_arith.ML ~> src/HOL/Tools
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28915
diff changeset
  1076
29398
89813bbf0f3e NEWS and CONTRIBUTORS
haftmann
parents: 29253
diff changeset
  1077
    src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL
89813bbf0f3e NEWS and CONTRIBUTORS
haftmann
parents: 29253
diff changeset
  1078
    src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL
89813bbf0f3e NEWS and CONTRIBUTORS
haftmann
parents: 29253
diff changeset
  1079
    src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL
89813bbf0f3e NEWS and CONTRIBUTORS
haftmann
parents: 29253
diff changeset
  1080
    src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL
89813bbf0f3e NEWS and CONTRIBUTORS
haftmann
parents: 29253
diff changeset
  1081
    src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL
89813bbf0f3e NEWS and CONTRIBUTORS
haftmann
parents: 29253
diff changeset
  1082
    src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL
89813bbf0f3e NEWS and CONTRIBUTORS
haftmann
parents: 29253
diff changeset
  1083
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1084
* If methods "eval" and "evaluation" encounter a structured proof
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1085
state with !!/==>, only the conclusion is evaluated to True (if
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1086
possible), avoiding strange error messages.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1087
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1088
* Method "sizechange" automates termination proofs using (a
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1089
modification of) the size-change principle.  Requires SAT solver.  See
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1090
src/HOL/ex/Termination.thy for examples.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1091
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1092
* Simplifier: simproc for let expressions now unfolds if bound
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1093
variable occurs at most once in let expression body.  INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1094
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1095
* Method "arith": Linear arithmetic now ignores all inequalities when
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1096
fast_arith_neq_limit is exceeded, instead of giving up entirely.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1097
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1098
* New attribute "arith" for facts that should always be used
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1099
automatically by arithmetic. It is intended to be used locally in
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1100
proofs, e.g.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1101
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1102
  assumes [arith]: "x > 0"
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1103
30706
e20227b5e6a3 NEWS: [arith]
nipkow
parents: 30609
diff changeset
  1104
Global usage is discouraged because of possible performance impact.
e20227b5e6a3 NEWS: [arith]
nipkow
parents: 30609
diff changeset
  1105
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1106
* New classes "top" and "bot" with corresponding operations "top" and
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1107
"bot" in theory Orderings; instantiation of class "complete_lattice"
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1108
requires instantiation of classes "top" and "bot".  INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1109
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1110
* Changed definition lemma "less_fun_def" in order to provide an
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1111
instance for preorders on functions; use lemma "less_le" instead.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1112
INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1113
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1114
* Theory Orderings: class "wellorder" moved here, with explicit
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1115
induction rule "less_induct" as assumption.  For instantiation of
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1116
"wellorder" by means of predicate "wf", use rule wf_wellorderI.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1117
INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1118
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1119
* Theory Orderings: added class "preorder" as superclass of "order".
27793
29ad1d91a5a3 tuned formatting;
wenzelm
parents: 27761
diff changeset
  1120
INCOMPATIBILITY: Instantiation proofs for order, linorder
29ad1d91a5a3 tuned formatting;
wenzelm
parents: 27761
diff changeset
  1121
etc. slightly changed.  Some theorems named order_class.* now named
29ad1d91a5a3 tuned formatting;
wenzelm
parents: 27761
diff changeset
  1122
preorder_class.*.
29ad1d91a5a3 tuned formatting;
wenzelm
parents: 27761
diff changeset
  1123
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1124
* Theory Relation: renamed "refl" to "refl_on", "reflexive" to "refl,
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1125
"diag" to "Id_on".
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1126
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1127
* Theory Finite_Set: added a new fold combinator of type
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1128
28855
5d21a3e7303c *** empty log message ***
nipkow
parents: 28741
diff changeset
  1129
  ('a => 'b => 'b) => 'b => 'a set => 'b
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1130
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1131
Occasionally this is more convenient than the old fold combinator
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1132
which is now defined in terms of the new one and renamed to
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1133
fold_image.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1134
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1135
* Theories Ring_and_Field and OrderedGroup: The lemmas "group_simps"
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1136
and "ring_simps" have been replaced by "algebra_simps" (which can be
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1137
extended with further lemmas!).  At the moment both still exist but
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1138
the former will disappear at some point.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1139
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1140
* Theory Power: Lemma power_Suc is now declared as a simp rule in
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1141
class recpower.  Type-specific simp rules for various recpower types
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1142
have been removed.  INCOMPATIBILITY, rename old lemmas as follows:
30273
ecd6f0ca62ea declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents: 30250
diff changeset
  1143
ecd6f0ca62ea declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents: 30250
diff changeset
  1144
rat_power_0    -> power_0
ecd6f0ca62ea declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents: 30250
diff changeset
  1145
rat_power_Suc  -> power_Suc
ecd6f0ca62ea declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents: 30250
diff changeset
  1146
realpow_0      -> power_0
ecd6f0ca62ea declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents: 30250
diff changeset
  1147
realpow_Suc    -> power_Suc
ecd6f0ca62ea declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents: 30250
diff changeset
  1148
complexpow_0   -> power_0
ecd6f0ca62ea declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents: 30250
diff changeset
  1149
complexpow_Suc -> power_Suc
ecd6f0ca62ea declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents: 30250
diff changeset
  1150
power_poly_0   -> power_0
ecd6f0ca62ea declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents: 30250
diff changeset
  1151
power_poly_Suc -> power_Suc
ecd6f0ca62ea declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents: 30250
diff changeset
  1152
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1153
* Theories Ring_and_Field and Divides: Definition of "op dvd" has been
27793
29ad1d91a5a3 tuned formatting;
wenzelm
parents: 27761
diff changeset
  1154
moved to separate class dvd in Ring_and_Field; a couple of lemmas on
29ad1d91a5a3 tuned formatting;
wenzelm
parents: 27761
diff changeset
  1155
dvd has been generalized to class comm_semiring_1.  Likewise a bunch
29ad1d91a5a3 tuned formatting;
wenzelm
parents: 27761
diff changeset
  1156
of lemmas from Divides has been generalized from nat to class
29ad1d91a5a3 tuned formatting;
wenzelm
parents: 27761
diff changeset
  1157
semiring_div.  INCOMPATIBILITY.  This involves the following theorem
29ad1d91a5a3 tuned formatting;
wenzelm
parents: 27761
diff changeset
  1158
renames resulting from duplicate elimination:
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27599
diff changeset
  1159
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27599
diff changeset
  1160
    dvd_def_mod ~>          dvd_eq_mod_eq_0
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27599
diff changeset
  1161
    zero_dvd_iff ~>         dvd_0_left_iff
28559
55c003a5600a tuned default rules of (dvd)
haftmann
parents: 28522
diff changeset
  1162
    dvd_0 ~>                dvd_0_right
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27599
diff changeset
  1163
    DIVISION_BY_ZERO_DIV ~> div_by_0
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27599
diff changeset
  1164
    DIVISION_BY_ZERO_MOD ~> mod_by_0
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27599
diff changeset
  1165
    mult_div ~>             div_mult_self2_is_id
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27599
diff changeset
  1166
    mult_mod ~>             mod_mult_self2_is_0
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27599
diff changeset
  1167
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1168
* Theory IntDiv: removed many lemmas that are instances of class-based
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1169
generalizations (from Divides and Ring_and_Field).  INCOMPATIBILITY,
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1170
rename old lemmas as follows:
30044
nipkow
parents: 29883
diff changeset
  1171
nipkow
parents: 29883
diff changeset
  1172
dvd_diff               -> nat_dvd_diff
nipkow
parents: 29883
diff changeset
  1173
dvd_zminus_iff         -> dvd_minus_iff
30224
79136ce06bdb removed and renamed redundant lemmas
nipkow
parents: 30200
diff changeset
  1174
mod_add1_eq            -> mod_add_eq
79136ce06bdb removed and renamed redundant lemmas
nipkow
parents: 30200
diff changeset
  1175
mod_mult1_eq           -> mod_mult_right_eq
79136ce06bdb removed and renamed redundant lemmas
nipkow
parents: 30200
diff changeset
  1176
mod_mult1_eq'          -> mod_mult_left_eq
79136ce06bdb removed and renamed redundant lemmas
nipkow
parents: 30200
diff changeset
  1177
mod_mult_distrib_mod   -> mod_mult_eq
30044
nipkow
parents: 29883
diff changeset
  1178
nat_mod_add_left_eq    -> mod_add_left_eq
nipkow
parents: 29883
diff changeset
  1179
nat_mod_add_right_eq   -> mod_add_right_eq
nipkow
parents: 29883
diff changeset
  1180
nat_mod_div_trivial    -> mod_div_trivial
nipkow
parents: 29883
diff changeset
  1181
nat_mod_mod_trivial    -> mod_mod_trivial
nipkow
parents: 29883
diff changeset
  1182
zdiv_zadd_self1        -> div_add_self1
nipkow
parents: 29883
diff changeset
  1183
zdiv_zadd_self2        -> div_add_self2
30181
05629f28f0f7 removed redundant lemmas
nipkow
parents: 30176
diff changeset
  1184
zdiv_zmult_self1       -> div_mult_self2_is_id
30044
nipkow
parents: 29883
diff changeset
  1185
zdiv_zmult_self2       -> div_mult_self1_is_id
nipkow
parents: 29883
diff changeset
  1186
zdvd_triv_left         -> dvd_triv_left
nipkow
parents: 29883
diff changeset
  1187
zdvd_triv_right        -> dvd_triv_right
nipkow
parents: 29883
diff changeset
  1188
zdvd_zmult_cancel_disj -> dvd_mult_cancel_left
30085
nipkow
parents: 30044
diff changeset
  1189
zmod_eq0_zdvd_iff      -> dvd_eq_mod_eq_0[symmetric]
30044
nipkow
parents: 29883
diff changeset
  1190
zmod_zadd_left_eq      -> mod_add_left_eq
nipkow
parents: 29883
diff changeset
  1191
zmod_zadd_right_eq     -> mod_add_right_eq
nipkow
parents: 29883
diff changeset
  1192
zmod_zadd_self1        -> mod_add_self1
nipkow
parents: 29883
diff changeset
  1193
zmod_zadd_self2        -> mod_add_self2
30224
79136ce06bdb removed and renamed redundant lemmas
nipkow
parents: 30200
diff changeset
  1194
zmod_zadd1_eq          -> mod_add_eq
30044
nipkow
parents: 29883
diff changeset
  1195
zmod_zdiff1_eq         -> mod_diff_eq
nipkow
parents: 29883
diff changeset
  1196
zmod_zdvd_zmod         -> mod_mod_cancel
nipkow
parents: 29883
diff changeset
  1197
zmod_zmod_cancel       -> mod_mod_cancel
nipkow
parents: 29883
diff changeset
  1198
zmod_zmult_self1       -> mod_mult_self2_is_0
nipkow
parents: 29883
diff changeset
  1199
zmod_zmult_self2       -> mod_mult_self1_is_0
nipkow
parents: 29883
diff changeset
  1200
zmod_1                 -> mod_by_1
nipkow
parents: 29883
diff changeset
  1201
zdiv_1                 -> div_by_1
nipkow
parents: 29883
diff changeset
  1202
zdvd_abs1              -> abs_dvd_iff
nipkow
parents: 29883
diff changeset
  1203
zdvd_abs2              -> dvd_abs_iff
nipkow
parents: 29883
diff changeset
  1204
zdvd_refl              -> dvd_refl
nipkow
parents: 29883
diff changeset
  1205
zdvd_trans             -> dvd_trans
nipkow
parents: 29883
diff changeset
  1206
zdvd_zadd              -> dvd_add
nipkow
parents: 29883
diff changeset
  1207
zdvd_zdiff             -> dvd_diff
nipkow
parents: 29883
diff changeset
  1208
zdvd_zminus_iff        -> dvd_minus_iff
nipkow
parents: 29883
diff changeset
  1209
zdvd_zminus2_iff       -> minus_dvd_iff
nipkow
parents: 29883
diff changeset
  1210
zdvd_zmultD            -> dvd_mult_right
nipkow
parents: 29883
diff changeset
  1211
zdvd_zmultD2           -> dvd_mult_left
nipkow
parents: 29883
diff changeset
  1212
zdvd_zmult_mono        -> mult_dvd_mono
nipkow
parents: 29883
diff changeset
  1213
zdvd_0_right           -> dvd_0_right
nipkow
parents: 29883
diff changeset
  1214
zdvd_0_left            -> dvd_0_left_iff
nipkow
parents: 29883
diff changeset
  1215
zdvd_1_left            -> one_dvd
nipkow
parents: 29883
diff changeset
  1216
zminus_dvd_iff         -> minus_dvd_iff
nipkow
parents: 29883
diff changeset
  1217
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1218
* Theory Rational: 'Fract k 0' now equals '0'.  INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1219
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1220
* The real numbers offer decimal input syntax: 12.34 is translated
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1221
into 1234/10^2. This translation is not reversed upon output.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1222
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1223
* Theory Library/Polynomial defines an abstract type 'a poly of
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1224
univariate polynomials with coefficients of type 'a.  In addition to
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1225
the standard ring operations, it also supports div and mod.  Code
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1226
generation is also supported, using list-style constructors.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1227
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1228
* Theory Library/Inner_Product defines a class of real_inner for real
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1229
inner product spaces, with an overloaded operation inner :: 'a => 'a
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1230
=> real.  Class real_inner is a subclass of real_normed_vector from
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1231
theory RealVector.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1232
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1233
* Theory Library/Product_Vector provides instances for the product
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1234
type 'a * 'b of several classes from RealVector and Inner_Product.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1235
Definitions of addition, subtraction, scalar multiplication, norms,
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1236
and inner products are included.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1237
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1238
* Theory Library/Bit defines the field "bit" of integers modulo 2.  In
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1239
addition to the field operations, numerals and case syntax are also
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1240
supported.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1241
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1242
* Theory Library/Diagonalize provides constructive version of Cantor's
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1243
first diagonalization argument.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1244
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1245
* Theory Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,
27599
ca23ef50c178 added command 'linear_undo';
wenzelm
parents: 27556
diff changeset
  1246
zlcm (for int); carried together from various gcd/lcm developements in
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1247
the HOL Distribution.  Constants zgcd and zlcm replace former igcd and
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1248
ilcm; corresponding theorems renamed accordingly.  INCOMPATIBILITY,
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1249
may recover tupled syntax as follows:
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27551
diff changeset
  1250
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27551
diff changeset
  1251
    hide (open) const gcd
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27551
diff changeset
  1252
    abbreviation gcd where
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27551
diff changeset
  1253
      "gcd == (%(a, b). GCD.gcd a b)"
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27551
diff changeset
  1254
    notation (output)
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27551
diff changeset
  1255
      GCD.gcd ("gcd '(_, _')")
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27551
diff changeset
  1256
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1257
The same works for lcm, zgcd, zlcm.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1258
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1259
* Theory Library/Nat_Infinity: added addition, numeral syntax and more
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1260
instantiations for algebraic structures.  Removed some duplicate
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1261
theorems.  Changes in simp rules.  INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1262
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1263
* ML antiquotation @{code} takes a constant as argument and generates
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27599
diff changeset
  1264
corresponding code in background and inserts name of the corresponding
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27599
diff changeset
  1265
resulting ML value/function/datatype constructor binding in place.
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27599
diff changeset
  1266
All occurrences of @{code} with a single ML block are generated
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27599
diff changeset
  1267
simultaneously.  Provides a generic and safe interface for
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1268
instrumentalizing code generation.  See
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1269
src/HOL/Decision_Procs/Ferrack.thy for a more ambitious application.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1270
In future you ought to refrain from ad-hoc compiling generated SML
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1271
code on the ML toplevel.  Note that (for technical reasons) @{code}
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1272
cannot refer to constants for which user-defined serializations are
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1273
set.  Refer to the corresponding ML counterpart directly in that
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1274
cases.
27122
63d92a5e3784 proper news header;
wenzelm
parents: 27104
diff changeset
  1275
63d92a5e3784 proper news header;
wenzelm
parents: 27104
diff changeset
  1276
* Command 'rep_datatype': instead of theorem names the command now
63d92a5e3784 proper news header;
wenzelm
parents: 27104
diff changeset
  1277
takes a list of terms denoting the constructors of the type to be
63d92a5e3784 proper news header;
wenzelm
parents: 27104
diff changeset
  1278
represented as datatype.  The characteristic theorems have to be
63d92a5e3784 proper news header;
wenzelm
parents: 27104
diff changeset
  1279
proven.  INCOMPATIBILITY.  Also observe that the following theorems
63d92a5e3784 proper news header;
wenzelm
parents: 27104
diff changeset
  1280
have disappeared in favour of existing ones:
63d92a5e3784 proper news header;
wenzelm
parents: 27104
diff changeset
  1281
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27067
diff changeset
  1282
    unit_induct                 ~> unit.induct
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27067
diff changeset
  1283
    prod_induct                 ~> prod.induct
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27067
diff changeset
  1284
    sum_induct                  ~> sum.induct
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27067
diff changeset
  1285
    Suc_Suc_eq                  ~> nat.inject
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27067
diff changeset
  1286
    Suc_not_Zero Zero_not_Suc   ~> nat.distinct
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27067
diff changeset
  1287
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27067
diff changeset
  1288
27696
15b65db66751 Unit_inv_l, Unit_inv_r made [simp];
ballarin
parents: 27681
diff changeset
  1289
*** HOL-Algebra ***
15b65db66751 Unit_inv_l, Unit_inv_r made [simp];
ballarin
parents: 27681
diff changeset
  1290
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27704
diff changeset
  1291
* New locales for orders and lattices where the equivalence relation
30106
351fc2f8493d tuned NEWS;
wenzelm
parents: 30085
diff changeset
  1292
is not restricted to equality.  INCOMPATIBILITY: all order and lattice
351fc2f8493d tuned NEWS;
wenzelm
parents: 30085
diff changeset
  1293
locales use a record structure with field eq for the equivalence.
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27704
diff changeset
  1294
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27704
diff changeset
  1295
* New theory of factorial domains.
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 27704
diff changeset
  1296
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1297
* Units_l_inv and Units_r_inv are now simp rules by default.
27696
15b65db66751 Unit_inv_l, Unit_inv_r made [simp];
ballarin
parents: 27681
diff changeset
  1298
INCOMPATIBILITY.  Simplifier proof that require deletion of l_inv
15b65db66751 Unit_inv_l, Unit_inv_r made [simp];
ballarin
parents: 27681
diff changeset
  1299
and/or r_inv will now also require deletion of these lemmas.
15b65db66751 Unit_inv_l, Unit_inv_r made [simp];
ballarin
parents: 27681
diff changeset
  1300
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1301
* Renamed the following theorems, INCOMPATIBILITY:
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1302
27696
15b65db66751 Unit_inv_l, Unit_inv_r made [simp];
ballarin
parents: 27681
diff changeset
  1303
UpperD ~> Upper_memD
15b65db66751 Unit_inv_l, Unit_inv_r made [simp];
ballarin
parents: 27681
diff changeset
  1304
LowerD ~> Lower_memD
15b65db66751 Unit_inv_l, Unit_inv_r made [simp];
ballarin
parents: 27681
diff changeset
  1305
least_carrier ~> least_closed
15b65db66751 Unit_inv_l, Unit_inv_r made [simp];
ballarin
parents: 27681
diff changeset
  1306
greatest_carrier ~> greatest_closed
15b65db66751 Unit_inv_l, Unit_inv_r made [simp];
ballarin
parents: 27681
diff changeset
  1307
greatest_Lower_above ~> greatest_Lower_below
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27713
diff changeset
  1308
one_zero ~> carrier_one_zero
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27713
diff changeset
  1309
one_not_zero ~> carrier_one_not_zero  (collision with assumption)
27696
15b65db66751 Unit_inv_l, Unit_inv_r made [simp];
ballarin
parents: 27681
diff changeset
  1310
27793
29ad1d91a5a3 tuned formatting;
wenzelm
parents: 27761
diff changeset
  1311
30849
0e5ec6d2c1d9 some HOL-Nominal news;
wenzelm
parents: 30847
diff changeset
  1312
*** HOL-Nominal ***
0e5ec6d2c1d9 some HOL-Nominal news;
wenzelm
parents: 30847
diff changeset
  1313
30855
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1314
* Nominal datatypes can now contain type-variables.
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1315
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1316
* Commands 'nominal_inductive' and 'equivariance' work with local
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1317
theory targets.
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1318
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1319
* Nominal primrec can now works with local theory targets and its
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1320
specification syntax now conforms to the general format as seen in
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1321
'inductive' etc.
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1322
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1323
* Method "perm_simp" honours the standard simplifier attributes
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1324
(no_asm), (no_asm_use) etc.
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1325
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1326
* The new predicate #* is defined like freshness, except that on the
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1327
left hand side can be a set or list of atoms.
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1328
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1329
* Experimental command 'nominal_inductive2' derives strong induction
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1330
principles for inductive definitions.  In contrast to
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1331
'nominal_inductive', which can only deal with a fixed number of
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1332
binders, it can deal with arbitrary expressions standing for sets of
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1333
atoms to be avoided.  The only inductive definition we have at the
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1334
moment that needs this generalisation is the typing rule for Lets in
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1335
the algorithm W:
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1336
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1337
 Gamma |- t1 : T1   (x,close Gamma T1)::Gamma |- t2 : T2   x#Gamma
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1338
 -----------------------------------------------------------------
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1339
         Gamma |- Let x be t1 in t2 : T2
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1340
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1341
In this rule one wants to avoid all the binders that are introduced by
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1342
"close Gamma T1".  We are looking for other examples where this
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1343
feature might be useful.  Please let us know.
30849
0e5ec6d2c1d9 some HOL-Nominal news;
wenzelm
parents: 30847
diff changeset
  1344
0e5ec6d2c1d9 some HOL-Nominal news;
wenzelm
parents: 30847
diff changeset
  1345
30176
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1346
*** HOLCF ***
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1347
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1348
* Reimplemented the simplification procedure for proving continuity
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1349
subgoals.  The new simproc is extensible; users can declare additional
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1350
continuity introduction rules with the attribute [cont2cont].
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1351
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1352
* The continuity simproc now uses a different introduction rule for
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1353
solving continuity subgoals on terms with lambda abstractions.  In
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1354
some rare cases the new simproc may fail to solve subgoals that the
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1355
old one could solve, and "simp add: cont2cont_LAM" may be necessary.
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1356
Potential INCOMPATIBILITY.
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1357
30847
wenzelm
parents: 30845
diff changeset
  1358
* Command 'fixrec': specification syntax now conforms to the general
30855
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1359
format as seen in 'inductive' etc.  See src/HOLCF/ex/Fixrec_ex.thy for
c22436e6d350 some more HOL-Nominal news;
wenzelm
parents: 30849
diff changeset
  1360
examples.  INCOMPATIBILITY.
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1361
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1362
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1363
*** ZF ***
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1364
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1365
* Proof of Zorn's Lemma for partial orders.
30176
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1366
78610979b3c6 add news for HOLCF; fixed some typos and inaccuracies
huffman
parents: 30163
diff changeset
  1367
27246
df85326af57c * Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents: 27200
diff changeset
  1368
*** ML ***
28088
723735f2d73a * Name bindings in higher specification mechanisms;
wenzelm
parents: 28085
diff changeset
  1369
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1370
* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1371
Poly/ML 5.2.1 or later.  Important note: the TimeLimit facility
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1372
depends on multithreading, so timouts will not work before Poly/ML
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1373
5.2.1!
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1374
29161
9903e84a9c9c * Proofs of are run in parallel on multi-core systems;
wenzelm
parents: 29145
diff changeset
  1375
* High-level support for concurrent ML programming, see
9903e84a9c9c * Proofs of are run in parallel on multi-core systems;
wenzelm
parents: 29145
diff changeset
  1376
src/Pure/Cuncurrent.  The data-oriented model of "future values" is
9903e84a9c9c * Proofs of are run in parallel on multi-core systems;
wenzelm
parents: 29145
diff changeset
  1377
particularly convenient to organize independent functional
9903e84a9c9c * Proofs of are run in parallel on multi-core systems;
wenzelm
parents: 29145
diff changeset
  1378
computations.  The concept of "synchronized variables" provides a
9903e84a9c9c * Proofs of are run in parallel on multi-core systems;
wenzelm
parents: 29145
diff changeset
  1379
higher-order interface for components with shared state, avoiding the
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1380
delicate details of mutexes and condition variables.  (Requires
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1381
Poly/ML 5.2.1 or later.)
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1382
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1383
* ML bindings produced via Isar commands are stored within the Isar
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1384
context (theory or proof).  Consequently, commands like 'use' and 'ML'
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1385
become thread-safe and work with undo as expected (concerning
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1386
top-level bindings, not side-effects on global references).
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1387
INCOMPATIBILITY, need to provide proper Isar context when invoking the
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1388
compiler at runtime; really global bindings need to be given outside a
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1389
theory.  (Requires Poly/ML 5.2 or later.)
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1390
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1391
* Command 'ML_prf' is analogous to 'ML' but works within a proof
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1392
context.  Top-level ML bindings are stored within the proof context in
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1393
a purely sequential fashion, disregarding the nested proof structure.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1394
ML bindings introduced by 'ML_prf' are discarded at the end of the
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1395
proof.  (Requires Poly/ML 5.2 or later.)
29161
9903e84a9c9c * Proofs of are run in parallel on multi-core systems;
wenzelm
parents: 29145
diff changeset
  1396
30530
03c120763ea8 simplified attribute and method setup;
wenzelm
parents: 30461
diff changeset
  1397
* Simplified ML attribute and method setup, cf. functions Attrib.setup
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741