NEWS
author bulwahn
Thu, 09 Sep 2010 14:38:14 +0200
changeset 39250 548a3e5521ab
parent 39215 7b2631c91a95
child 39277 f263522ab226
permissions -rw-r--r--
changing String.literal to a type instead of a datatype
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
37383
22757d15cd86 back to non-release mode;
wenzelm
parents: 37352
diff changeset
     4
New in this Isabelle version
22757d15cd86 back to non-release mode;
wenzelm
parents: 37352
diff changeset
     5
----------------------------
22757d15cd86 back to non-release mode;
wenzelm
parents: 37352
diff changeset
     6
37536
c62aa9281101 explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents: 37484
diff changeset
     7
*** General ***
c62aa9281101 explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents: 37484
diff changeset
     8
c62aa9281101 explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents: 37484
diff changeset
     9
* Explicit treatment of UTF8 sequences as Isabelle symbols, such that
c62aa9281101 explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents: 37484
diff changeset
    10
a Unicode character is treated as a single symbol, not a sequence of
c62aa9281101 explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents: 37484
diff changeset
    11
non-ASCII bytes as before.  Since Isabelle/ML string literals may
c62aa9281101 explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents: 37484
diff changeset
    12
contain symbols without further backslash escapes, Unicode can now be
c62aa9281101 explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents: 37484
diff changeset
    13
used here as well.  Recall that Symbol.explode in ML provides a
c62aa9281101 explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents: 37484
diff changeset
    14
consistent view on symbols, while raw explode (or String.explode)
c62aa9281101 explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents: 37484
diff changeset
    15
merely give a byte-oriented representation.
c62aa9281101 explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents: 37484
diff changeset
    16
38135
2b9bfa0b44f1 theory loading: only the master source file is looked-up in the implicit load path;
wenzelm
parents: 38110
diff changeset
    17
* Theory loading: only the master source file is looked-up in the
2b9bfa0b44f1 theory loading: only the master source file is looked-up in the implicit load path;
wenzelm
parents: 38110
diff changeset
    18
implicit load path, all other files are addressed relatively to its
2b9bfa0b44f1 theory loading: only the master source file is looked-up in the implicit load path;
wenzelm
parents: 38110
diff changeset
    19
directory.  Minor INCOMPATIBILITY, subtle change in semantics.
2b9bfa0b44f1 theory loading: only the master source file is looked-up in the implicit load path;
wenzelm
parents: 38110
diff changeset
    20
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37868
diff changeset
    21
* Special treatment of ML file names has been discontinued.
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37868
diff changeset
    22
Historically, optional extensions .ML or .sml were added on demand --
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37868
diff changeset
    23
at the cost of clarity of file dependencies.  Recall that Isabelle/ML
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37868
diff changeset
    24
files exclusively use the .ML extension.  Minor INCOMPATIBILTY.
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37868
diff changeset
    25
38980
af73cf0dc31f turned show_question_marks into proper configuration option;
wenzelm
parents: 38864
diff changeset
    26
* Various options that affect pretty printing etc. are now properly
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38708
diff changeset
    27
handled within the context via configuration options, instead of
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38708
diff changeset
    28
unsynchronized references.  There are both ML Config.T entities and
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38708
diff changeset
    29
Isar declaration attributes to access these.
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38708
diff changeset
    30
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39105
diff changeset
    31
  ML (Config.T)                 Isar (attribute)
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39105
diff changeset
    32
39128
93a7365fb4ee turned eta_contract into proper configuration option;
wenzelm
parents: 39126
diff changeset
    33
  eta_contract                  eta_contract
39137
ccb53edd59f0 turned show_brackets into proper configuration option;
wenzelm
parents: 39134
diff changeset
    34
  show_brackets                 show_brackets
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39128
diff changeset
    35
  show_sorts                    show_sorts
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39128
diff changeset
    36
  show_types                    show_types
39126
ee117c5b3b75 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents: 39125
diff changeset
    37
  show_question_marks           show_question_marks
ee117c5b3b75 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents: 39125
diff changeset
    38
  show_consts                   show_consts
ee117c5b3b75 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents: 39125
diff changeset
    39
ee117c5b3b75 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents: 39125
diff changeset
    40
  Syntax.ambiguity_level        syntax_ambiguity_level
ee117c5b3b75 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents: 39125
diff changeset
    41
ee117c5b3b75 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents: 39125
diff changeset
    42
  Goal_Display.goals_limit      goals_limit
ee117c5b3b75 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents: 39125
diff changeset
    43
  Goal_Display.show_main_goal   show_main_goal
ee117c5b3b75 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents: 39125
diff changeset
    44
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39105
diff changeset
    45
  Thy_Output.display            thy_output_display
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39105
diff changeset
    46
  Thy_Output.quotes             thy_output_quotes
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39105
diff changeset
    47
  Thy_Output.indent             thy_output_indent
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39105
diff changeset
    48
  Thy_Output.source             thy_output_source
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39105
diff changeset
    49
  Thy_Output.break              thy_output_break
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39105
diff changeset
    50
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39105
diff changeset
    51
Note that corresponding "..._default" references in ML may be only
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38708
diff changeset
    52
changed globally at the ROOT session setup, but *not* within a theory.
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38708
diff changeset
    53
37536
c62aa9281101 explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents: 37484
diff changeset
    54
38110
2c1913d1b945 Documentation of 'interpret' updated.
ballarin
parents: 37939
diff changeset
    55
*** Pure ***
2c1913d1b945 Documentation of 'interpret' updated.
ballarin
parents: 37939
diff changeset
    56
2c1913d1b945 Documentation of 'interpret' updated.
ballarin
parents: 37939
diff changeset
    57
* Interpretation command 'interpret' accepts a list of equations like
2c1913d1b945 Documentation of 'interpret' updated.
ballarin
parents: 37939
diff changeset
    58
'interpretation' does.
2c1913d1b945 Documentation of 'interpret' updated.
ballarin
parents: 37939
diff changeset
    59
2c1913d1b945 Documentation of 'interpret' updated.
ballarin
parents: 37939
diff changeset
    60
* Diagnostic command 'print_interps' prints interpretations in proofs
2c1913d1b945 Documentation of 'interpret' updated.
ballarin
parents: 37939
diff changeset
    61
in addition to interpretations in theories.
2c1913d1b945 Documentation of 'interpret' updated.
ballarin
parents: 37939
diff changeset
    62
38708
8915e3ce8655 discontinued obsolete 'global' and 'local' commands;
wenzelm
parents: 38656
diff changeset
    63
* Discontinued obsolete 'global' and 'local' commands to manipulate
8915e3ce8655 discontinued obsolete 'global' and 'local' commands;
wenzelm
parents: 38656
diff changeset
    64
the theory name space.  Rare INCOMPATIBILITY.  The ML functions
8915e3ce8655 discontinued obsolete 'global' and 'local' commands;
wenzelm
parents: 38656
diff changeset
    65
Sign.root_path and Sign.local_path may be applied directly where this
8915e3ce8655 discontinued obsolete 'global' and 'local' commands;
wenzelm
parents: 38656
diff changeset
    66
feature is still required for historical reasons.
8915e3ce8655 discontinued obsolete 'global' and 'local' commands;
wenzelm
parents: 38656
diff changeset
    67
39215
haftmann
parents: 39199
diff changeset
    68
* Discontinued ancient 'constdefs' command.  INCOMPATIBILITY, use
haftmann
parents: 39199
diff changeset
    69
'definition' instead.
haftmann
parents: 39199
diff changeset
    70
38110
2c1913d1b945 Documentation of 'interpret' updated.
ballarin
parents: 37939
diff changeset
    71
37387
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
    72
*** HOL ***
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
    73
39250
548a3e5521ab changing String.literal to a type instead of a datatype
bulwahn
parents: 39215
diff changeset
    74
* String.literal is a type, but not a datatype. INCOMPATIBILITY.
548a3e5521ab changing String.literal to a type instead of a datatype
bulwahn
parents: 39215
diff changeset
    75
 
39199
720112792ba0 renamed expand_*_eq in HOLCF as well
nipkow
parents: 39164
diff changeset
    76
* Renamed lemmas: expand_fun_eq -> ext_iff, expand_set_eq -> set_ext_iff
720112792ba0 renamed expand_*_eq in HOLCF as well
nipkow
parents: 39164
diff changeset
    77
38857
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 38815
diff changeset
    78
* Renamed class eq and constant eq (for code generation) to class equal
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 38815
diff changeset
    79
and constant equal, plus renaming of related facts and various tuning.
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 38815
diff changeset
    80
INCOMPATIBILITY.
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 38815
diff changeset
    81
38814
4d575fbfc920 official support for Scala
haftmann
parents: 38795
diff changeset
    82
* Scala (2.8 or higher) has been added to the target languages of
4d575fbfc920 official support for Scala
haftmann
parents: 38795
diff changeset
    83
the code generator.
4d575fbfc920 official support for Scala
haftmann
parents: 38795
diff changeset
    84
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 38622
diff changeset
    85
* Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 38622
diff changeset
    86
38622
86fc906dcd86 split and enriched theory SetsAndFunctions
haftmann
parents: 38559
diff changeset
    87
* Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
86fc906dcd86 split and enriched theory SetsAndFunctions
haftmann
parents: 38559
diff changeset
    88
canonical names for instance definitions for functions; various improvements.
86fc906dcd86 split and enriched theory SetsAndFunctions
haftmann
parents: 38559
diff changeset
    89
INCOMPATIBILITY.
86fc906dcd86 split and enriched theory SetsAndFunctions
haftmann
parents: 38559
diff changeset
    90
38545
haftmann
parents: 38537
diff changeset
    91
* Records: logical foundation type for records do not carry a '_type' suffix
haftmann
parents: 38537
diff changeset
    92
any longer.  INCOMPATIBILITY.
haftmann
parents: 38537
diff changeset
    93
38535
9f64860c6ec0 preemptive NEWS
haftmann
parents: 38461
diff changeset
    94
* Code generation for records: more idiomatic representation of record types.
9f64860c6ec0 preemptive NEWS
haftmann
parents: 38461
diff changeset
    95
Warning: records are not covered by ancient SML code generation any longer.
38537
6a78c972de27 more helpful NEWS entry
haftmann
parents: 38535
diff changeset
    96
INCOMPATIBILITY.  In cases of need, a suitable rep_datatype declaration
6a78c972de27 more helpful NEWS entry
haftmann
parents: 38535
diff changeset
    97
helps to succeed then:
6a78c972de27 more helpful NEWS entry
haftmann
parents: 38535
diff changeset
    98
6a78c972de27 more helpful NEWS entry
haftmann
parents: 38535
diff changeset
    99
  record 'a foo = ...
6a78c972de27 more helpful NEWS entry
haftmann
parents: 38535
diff changeset
   100
  ...
6a78c972de27 more helpful NEWS entry
haftmann
parents: 38535
diff changeset
   101
  rep_datatype foo_ext ...
38535
9f64860c6ec0 preemptive NEWS
haftmann
parents: 38461
diff changeset
   102
38461
75fc4087764e NEWS and CONTRIBUTORS
haftmann
parents: 38347
diff changeset
   103
* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
75fc4087764e NEWS and CONTRIBUTORS
haftmann
parents: 38347
diff changeset
   104
INCOMPATIBILITY.
75fc4087764e NEWS and CONTRIBUTORS
haftmann
parents: 38347
diff changeset
   105
75fc4087764e NEWS and CONTRIBUTORS
haftmann
parents: 38347
diff changeset
   106
* Quickcheck in locales considers interpretations of that locale for
75fc4087764e NEWS and CONTRIBUTORS
haftmann
parents: 38347
diff changeset
   107
counter example search.
75fc4087764e NEWS and CONTRIBUTORS
haftmann
parents: 38347
diff changeset
   108
38347
haftmann
parents: 38135
diff changeset
   109
* Theory Library/Monad_Syntax provides do-syntax for monad types.  Syntax
haftmann
parents: 38135
diff changeset
   110
in Library/State_Monad has been changed to avoid ambiguities.
haftmann
parents: 38135
diff changeset
   111
INCOMPATIBILITY.
haftmann
parents: 38135
diff changeset
   112
38461
75fc4087764e NEWS and CONTRIBUTORS
haftmann
parents: 38347
diff changeset
   113
* Code generator: export_code without explicit file declaration prints
37820
ffaca9167c16 export_code without file prints to standard output
haftmann
parents: 37735
diff changeset
   114
to standard output.  INCOMPATIBILITY.
ffaca9167c16 export_code without file prints to standard output
haftmann
parents: 37735
diff changeset
   115
37679
03217132b792 "prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect
haftmann
parents: 37666
diff changeset
   116
* Abolished symbol type names:  "prod" and "sum" replace "*" and "+"
37681
6ec40bc934e1 fixed spelling
haftmann
parents: 37679
diff changeset
   117
respectively.  INCOMPATIBILITY.
37679
03217132b792 "prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect
haftmann
parents: 37666
diff changeset
   118
37591
d3daea901123 merged constants "split" and "prod_case"
haftmann
parents: 37536
diff changeset
   119
* Constant "split" has been merged with constant "prod_case";  names
d3daea901123 merged constants "split" and "prod_case"
haftmann
parents: 37536
diff changeset
   120
of ML functions, facts etc. involving split have been retained so far,
d3daea901123 merged constants "split" and "prod_case"
haftmann
parents: 37536
diff changeset
   121
though.  INCOMPATIBILITY.
d3daea901123 merged constants "split" and "prod_case"
haftmann
parents: 37536
diff changeset
   122
37595
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   123
* Dropped old infix syntax "mem" for List.member;  use "in set"
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   124
instead.  INCOMPATIBILITY.
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   125
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   126
* Refactoring of code-generation specific operations in List.thy
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   127
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   128
  constants
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   129
    null ~> List.null
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   130
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   131
  facts
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   132
    mem_iff ~> member_def
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   133
    null_empty ~> null_def
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   134
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   135
INCOMPATIBILITY.  Note that these were not suppossed to be used
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   136
regularly unless for striking reasons;  their main purpose was code
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   137
generation.
9591362629e3 dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents: 37484
diff changeset
   138
37387
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
   139
* Some previously unqualified names have been qualified:
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
   140
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
   141
  types
38556
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 38546
diff changeset
   142
    bool ~> HOL.bool
37387
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
   143
    nat ~> Nat.nat
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
   144
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
   145
  constants
38556
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 38546
diff changeset
   146
    Trueprop ~> HOL.Trueprop
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 38546
diff changeset
   147
    True ~> HOL.True
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 38546
diff changeset
   148
    False ~> HOL.False
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38788
diff changeset
   149
    op & ~> HOL.conj
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38788
diff changeset
   150
    op | ~> HOL.disj
38788
haftmann
parents: 38708
diff changeset
   151
    op --> ~> HOL.implies
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38858
diff changeset
   152
    op = ~> HOL.eq
38556
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 38546
diff changeset
   153
    Not ~> HOL.Not
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 38546
diff changeset
   154
    The ~> HOL.The
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 38546
diff changeset
   155
    All ~> HOL.All
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 38546
diff changeset
   156
    Ex ~> HOL.Ex
dc92eee56ed7 deglobalized named HOL constants
haftmann
parents: 38546
diff changeset
   157
    Ex1 ~> HOL.Ex1
38524
haftmann
parents: 38522
diff changeset
   158
    Let ~> HOL.Let
haftmann
parents: 38522
diff changeset
   159
    If ~> HOL.If
37387
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
   160
    Ball ~> Set.Ball
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
   161
    Bex ~> Set.Bex
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
   162
    Suc ~> Nat.Suc
37389
09467cdfa198 qualified type "*"; qualified constants Pair, fst, snd, split
haftmann
parents: 37387
diff changeset
   163
    Pair ~> Product_Type.Pair
09467cdfa198 qualified type "*"; qualified constants Pair, fst, snd, split
haftmann
parents: 37387
diff changeset
   164
    fst ~> Product_Type.fst
09467cdfa198 qualified type "*"; qualified constants Pair, fst, snd, split
haftmann
parents: 37387
diff changeset
   165
    snd ~> Product_Type.snd
37387
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
   166
    curry ~> Product_Type.curry
37679
03217132b792 "prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect
haftmann
parents: 37666
diff changeset
   167
    op : ~> Set.member
03217132b792 "prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect
haftmann
parents: 37666
diff changeset
   168
    Collect ~> Set.Collect
37387
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
   169
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 37383
diff changeset
   170
INCOMPATIBILITY.
37383
22757d15cd86 back to non-release mode;
wenzelm
parents: 37352
diff changeset
   171
37411
c88c44156083 removed simplifier congruence rule of "prod_case"
haftmann
parents: 37389
diff changeset
   172
* Removed simplifier congruence rule of "prod_case", as has for long
38524
haftmann
parents: 38522
diff changeset
   173
been the case with "split".  INCOMPATIBILITY.
37411
c88c44156083 removed simplifier congruence rule of "prod_case"
haftmann
parents: 37389
diff changeset
   174
37423
haftmann
parents: 37389
diff changeset
   175
* Datatype package: theorems generated for executable equality
haftmann
parents: 37389
diff changeset
   176
(class eq) carry proper names and are treated as default code
haftmann
parents: 37389
diff changeset
   177
equations.
haftmann
parents: 37389
diff changeset
   178
39150
c4ff5fd8db99 removed duplicate lemma
krauss
parents: 39128
diff changeset
   179
* Removed lemma Option.is_none_none (Duplicate of is_none_def).
c4ff5fd8db99 removed duplicate lemma
krauss
parents: 39128
diff changeset
   180
INCOMPATIBILITY.
c4ff5fd8db99 removed duplicate lemma
krauss
parents: 39128
diff changeset
   181
37423
haftmann
parents: 37389
diff changeset
   182
* List.thy: use various operations from the Haskell prelude when
haftmann
parents: 37389
diff changeset
   183
generating Haskell code.
haftmann
parents: 37389
diff changeset
   184
38524
haftmann
parents: 38522
diff changeset
   185
* code_simp.ML and method code_simp: simplification with rules determined
haftmann
parents: 38522
diff changeset
   186
by code generator.
37442
037ee7b712b2 added code_simp infrastructure
haftmann
parents: 37433
diff changeset
   187
037ee7b712b2 added code_simp infrastructure
haftmann
parents: 37433
diff changeset
   188
* code generator: do not print function definitions for case
037ee7b712b2 added code_simp infrastructure
haftmann
parents: 37433
diff changeset
   189
combinators any longer.
037ee7b712b2 added code_simp infrastructure
haftmann
parents: 37433
diff changeset
   190
37666
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   191
* Multivariate Analysis: Introduced a type class for euclidean space. Most
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   192
theorems are now stated in terms of euclidean spaces instead of finite
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   193
cartesian products.
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   194
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   195
  types
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   196
    real ^ 'n ~>  'a::real_vector
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   197
              ~>  'a::euclidean_space
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   198
              ~>  'a::ordered_euclidean_space
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   199
        (depends on your needs)
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   200
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   201
  constants
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   202
     _ $ _        ~> _ $$ _
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   203
     \<chi> x. _  ~> \<chi>\<chi> x. _
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   204
     CARD('n)     ~> DIM('a)
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   205
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   206
Also note that the indices are now natural numbers and not from some finite
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   207
type. Finite cartesian products of euclidean spaces, products of euclidean
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   208
spaces the real and complex numbers are instantiated to be euclidean_spaces.
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   209
e31fd427c285 Updated NEWS
hoelzl
parents: 37608
diff changeset
   210
INCOMPATIBILITY.
37383
22757d15cd86 back to non-release mode;
wenzelm
parents: 37352
diff changeset
   211
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   212
* Probability: Introduced pinfreal as real numbers with infinity. Use pinfreal
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   213
as value for measures. Introduces Lebesgue Measure based on the integral in
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   214
Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   215
spaces.
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   216
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   217
 INCOMPATIBILITY.
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38642
diff changeset
   218
37735
26e673df3fd0 added NEWS entry
bulwahn
parents: 37681
diff changeset
   219
* Inductive package: offers new command "inductive_simps" to automatically
38461
75fc4087764e NEWS and CONTRIBUTORS
haftmann
parents: 38347
diff changeset
   220
derive instantiated and simplified equations for inductive predicates,
75fc4087764e NEWS and CONTRIBUTORS
haftmann
parents: 38347
diff changeset
   221
similar to inductive_cases.
37735
26e673df3fd0 added NEWS entry
bulwahn
parents: 37681
diff changeset
   222
39077
hoelzl
parents: 38864
diff changeset
   223
* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a
hoelzl
parents: 38864
diff changeset
   224
generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
hoelzl
parents: 38864
diff changeset
   225
The theorems bij_def and surj_def are unchanged.
37383
22757d15cd86 back to non-release mode;
wenzelm
parents: 37352
diff changeset
   226
38522
de7984a7172b deglobalization
haftmann
parents: 38461
diff changeset
   227
*** FOL ***
de7984a7172b deglobalization
haftmann
parents: 38461
diff changeset
   228
de7984a7172b deglobalization
haftmann
parents: 38461
diff changeset
   229
* All constant names are now qualified.  INCOMPATIBILITY.
de7984a7172b deglobalization
haftmann
parents: 38461
diff changeset
   230
de7984a7172b deglobalization
haftmann
parents: 38461
diff changeset
   231
de7984a7172b deglobalization
haftmann
parents: 38461
diff changeset
   232
*** ZF ***
de7984a7172b deglobalization
haftmann
parents: 38461
diff changeset
   233
de7984a7172b deglobalization
haftmann
parents: 38461
diff changeset
   234
* All constant names are now qualified.  INCOMPATIBILITY.
de7984a7172b deglobalization
haftmann
parents: 38461
diff changeset
   235
de7984a7172b deglobalization
haftmann
parents: 38461
diff changeset
   236
37868
59eed00bfd8e ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents: 37820
diff changeset
   237
*** ML ***
59eed00bfd8e ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents: 37820
diff changeset
   238
38980
af73cf0dc31f turned show_question_marks into proper configuration option;
wenzelm
parents: 38864
diff changeset
   239
* Configuration option show_question_marks only affects regular pretty
af73cf0dc31f turned show_question_marks into proper configuration option;
wenzelm
parents: 38864
diff changeset
   240
printing of types and terms, not raw Term.string_of_vname.
af73cf0dc31f turned show_question_marks into proper configuration option;
wenzelm
parents: 38864
diff changeset
   241
39164
e7e12555e763 ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents: 39154
diff changeset
   242
* ML_Context.thm and ML_Context.thms are no longer pervasive.  Rare
e7e12555e763 ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents: 39154
diff changeset
   243
INCOMPATIBILITY, superseded by static antiquotations @{thm} and
e7e12555e763 ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents: 39154
diff changeset
   244
@{thms} for most purposes.
e7e12555e763 ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents: 39154
diff changeset
   245
38980
af73cf0dc31f turned show_question_marks into proper configuration option;
wenzelm
parents: 38864
diff changeset
   246
* ML structure Unsynchronized never opened, not even in Isar
af73cf0dc31f turned show_question_marks into proper configuration option;
wenzelm
parents: 38864
diff changeset
   247
interaction mode as before.  Old Unsynchronized.set etc. have been
af73cf0dc31f turned show_question_marks into proper configuration option;
wenzelm
parents: 38864
diff changeset
   248
discontinued -- use plain := instead.  This should be *rare* anyway,
af73cf0dc31f turned show_question_marks into proper configuration option;
wenzelm
parents: 38864
diff changeset
   249
since modern tools always work via official context data, notably
af73cf0dc31f turned show_question_marks into proper configuration option;
wenzelm
parents: 38864
diff changeset
   250
configuration options.
af73cf0dc31f turned show_question_marks into proper configuration option;
wenzelm
parents: 38864
diff changeset
   251
37868
59eed00bfd8e ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents: 37820
diff changeset
   252
* ML antiquotations @{theory} and @{theory_ref} refer to named
59eed00bfd8e ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents: 37820
diff changeset
   253
theories from the ancestry of the current context, not any accidental
59eed00bfd8e ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents: 37820
diff changeset
   254
theory loader state as before.  Potential INCOMPATIBILITY, subtle
59eed00bfd8e ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents: 37820
diff changeset
   255
change in semantics.
59eed00bfd8e ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents: 37820
diff changeset
   256
59eed00bfd8e ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents: 37820
diff changeset
   257
38470
484e483eb606 discontinued support for Poly/ML 5.0 and 5.1 versions;
wenzelm
parents: 38461
diff changeset
   258
*** System ***
484e483eb606 discontinued support for Poly/ML 5.0 and 5.1 versions;
wenzelm
parents: 38461
diff changeset
   259
484e483eb606 discontinued support for Poly/ML 5.0 and 5.1 versions;
wenzelm
parents: 38461
diff changeset
   260
* Discontinued support for Poly/ML 5.0 and 5.1 versions.
484e483eb606 discontinued support for Poly/ML 5.0 and 5.1 versions;
wenzelm
parents: 38461
diff changeset
   261
484e483eb606 discontinued support for Poly/ML 5.0 and 5.1 versions;
wenzelm
parents: 38461
diff changeset
   262
37868
59eed00bfd8e ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents: 37820
diff changeset
   263
37144
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   264
New in Isabelle2009-2 (June 2010)
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   265
---------------------------------
33993
haftmann
parents: 33873
diff changeset
   266
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   267
*** General ***
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   268
35436
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   269
* Authentic syntax for *all* logical entities (type classes, type
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   270
constructors, term constants): provides simple and robust
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   271
correspondence between formal entities and concrete syntax.  Within
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   272
the parse tree / AST representations, "constants" are decorated by
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   273
their category (class, type, const) and spelled out explicitly with
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   274
their full internal name.
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   275
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   276
Substantial INCOMPATIBILITY concerning low-level syntax declarations
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   277
and translations (translation rules and translation functions in ML).
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   278
Some hints on upgrading:
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   279
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   280
  - Many existing uses of 'syntax' and 'translations' can be replaced
35436
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   281
    by more modern 'type_notation', 'notation' and 'abbreviation',
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   282
    which are independent of this issue.
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   283
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   284
  - 'translations' require markup within the AST; the term syntax
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   285
    provides the following special forms:
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   286
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   287
      CONST c   -- produces syntax version of constant c from context
35261
wenzelm
parents: 35260
diff changeset
   288
      XCONST c  -- literally c, checked as constant from context
wenzelm
parents: 35260
diff changeset
   289
      c         -- literally c, if declared by 'syntax'
wenzelm
parents: 35260
diff changeset
   290
wenzelm
parents: 35260
diff changeset
   291
    Plain identifiers are treated as AST variables -- occasionally the
wenzelm
parents: 35260
diff changeset
   292
    system indicates accidental variables via the error "rhs contains
wenzelm
parents: 35260
diff changeset
   293
    extra variables".
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   294
35436
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   295
    Type classes and type constructors are marked according to their
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   296
    concrete syntax.  Some old translations rules need to be written
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   297
    for the "type" category, using type constructor application
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   298
    instead of pseudo-term application of the default category
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   299
    "logic".
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   300
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   301
  - 'parse_translation' etc. in ML may use the following
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   302
    antiquotations:
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   303
35436
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   304
      @{class_syntax c}   -- type class c within parse tree / AST
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   305
      @{term_syntax c}    -- type constructor c within parse tree / AST
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   306
      @{const_syntax c}   -- ML version of "CONST c" above
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   307
      @{syntax_const c}   -- literally c (checked wrt. 'syntax' declarations)
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   308
35436
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   309
  - Literal types within 'typed_print_translations', i.e. those *not*
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   310
    represented as pseudo-terms are represented verbatim.  Use @{class
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   311
    c} or @{type_name c} here instead of the above syntax
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   312
    antiquotations.
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   313
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   314
Note that old non-authentic syntax was based on unqualified base
35436
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   315
names, so all of the above "constant" names would coincide.  Recall
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   316
that 'print_syntax' and ML_command "set Syntax.trace_ast" help to
38b291bb4a98 authentic syntax for *all* logical entities;
wenzelm
parents: 35413
diff changeset
   317
diagnose syntax problems.
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   318
35351
7425aece4ee3 allow general mixfix syntax for type constructors;
wenzelm
parents: 35306
diff changeset
   319
* Type constructors admit general mixfix syntax, not just infix.
7425aece4ee3 allow general mixfix syntax for type constructors;
wenzelm
parents: 35306
diff changeset
   320
36508
03d2a2d0ee4a allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents: 36461
diff changeset
   321
* Concrete syntax may be attached to local entities without a proof
03d2a2d0ee4a allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents: 36461
diff changeset
   322
body, too.  This works via regular mixfix annotations for 'fix',
03d2a2d0ee4a allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents: 36461
diff changeset
   323
'def', 'obtain' etc. or via the explicit 'write' command, which is
03d2a2d0ee4a allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents: 36461
diff changeset
   324
similar to the 'notation' command in theory specifications.
03d2a2d0ee4a allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents: 36461
diff changeset
   325
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   326
* Discontinued unnamed infix syntax (legacy feature for many years) --
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   327
need to specify constant name and syntax separately.  Internal ML
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   328
datatype constructors have been renamed from InfixName to Infix etc.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   329
Minor INCOMPATIBILITY.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   330
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   331
* Schematic theorem statements need to be explicitly markup as such,
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   332
via commands 'schematic_lemma', 'schematic_theorem',
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   333
'schematic_corollary'.  Thus the relevance of the proof is made
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   334
syntactically clear, which impacts performance in a parallel or
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   335
asynchronous interactive environment.  Minor INCOMPATIBILITY.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   336
35613
9d3ff36ad4e1 eliminated Args.bang_facts (legacy feature);
wenzelm
parents: 35436
diff changeset
   337
* Use of cumulative prems via "!" in some proof methods has been
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   338
discontinued (old legacy feature).
35613
9d3ff36ad4e1 eliminated Args.bang_facts (legacy feature);
wenzelm
parents: 35436
diff changeset
   339
35979
12bb31230550 replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
boehmes
parents: 35845
diff changeset
   340
* References 'trace_simp' and 'debug_simp' have been replaced by
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   341
configuration options stored in the context. Enabling tracing (the
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   342
case of debugging is similar) in proofs works via
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   343
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   344
  using [[trace_simp = true]]
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   345
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   346
Tracing is then active for all invocations of the simplifier in
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   347
subsequent goal refinement steps. Tracing may also still be enabled or
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   348
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
   349
36177
8e0770d2e499 separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents: 36162
diff changeset
   350
* Separate commands 'hide_class', 'hide_type', 'hide_const',
8e0770d2e499 separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents: 36162
diff changeset
   351
'hide_fact' replace the former 'hide' KIND command.  Minor
8e0770d2e499 separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents: 36162
diff changeset
   352
INCOMPATIBILITY.
8e0770d2e499 separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents: 36162
diff changeset
   353
37298
1f3ca94ccb84 improved parallelism of proof term normalization;
wenzelm
parents: 37273
diff changeset
   354
* Improved parallelism of proof term normalization: usedir -p2 -q0 is
1f3ca94ccb84 improved parallelism of proof term normalization;
wenzelm
parents: 37273
diff changeset
   355
more efficient than combinations with -q1 or -q2.
1f3ca94ccb84 improved parallelism of proof term normalization;
wenzelm
parents: 37273
diff changeset
   356
35260
41e82c1b5586 NEWS: authentic syntax for *all* term constants;
wenzelm
parents: 35130
diff changeset
   357
34170
254ac75e4c38 reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents: 34076
diff changeset
   358
*** Pure ***
254ac75e4c38 reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents: 34076
diff changeset
   359
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   360
* Proofterms record type-class reasoning explicitly, using the
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   361
"unconstrain" operation internally.  This eliminates all sort
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   362
constraints from a theorem and proof, introducing explicit
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   363
OFCLASS-premises.  On the proof term level, this operation is
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   364
automatically applied at theorem boundaries, such that closed proofs
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   365
are always free of sort constraints.  INCOMPATIBILITY for tools that
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   366
inspect proof terms.
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36096
diff changeset
   367
35765
09e238561460 local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents: 35763
diff changeset
   368
* Local theory specifications may depend on extra type variables that
09e238561460 local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents: 35763
diff changeset
   369
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
   370
are added internally.  For example:
09e238561460 local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents: 35763
diff changeset
   371
09e238561460 local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents: 35763
diff changeset
   372
  definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
09e238561460 local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents: 35763
diff changeset
   373
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   374
* Predicates of locales introduced by classes carry a mandatory
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   375
"class" prefix.  INCOMPATIBILITY.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   376
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   377
* Vacuous class specifications observe default sort.  INCOMPATIBILITY.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   378
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   379
* Old 'axclass' command has been discontinued.  INCOMPATIBILITY, use
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   380
'class' instead.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   381
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   382
* Command 'code_reflect' allows to incorporate generated ML code into
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   383
runtime environment; replaces immature code_datatype antiquotation.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   384
INCOMPATIBILITY.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   385
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   386
* Code generator: simple concept for abstract datatypes obeying
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   387
invariants.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   388
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   389
* Code generator: details of internal data cache have no impact on the
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   390
user space functionality any longer.
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   391
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   392
* Methods "unfold_locales" and "intro_locales" ignore non-locale
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   393
subgoals.  This is more appropriate for interpretations with 'where'.
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   394
INCOMPATIBILITY.
34170
254ac75e4c38 reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents: 34076
diff changeset
   395
36356
5ab0f8859f9f command 'example_proof' opens an empty proof body;
wenzelm
parents: 36348
diff changeset
   396
* Command 'example_proof' opens an empty proof body.  This allows to
5ab0f8859f9f command 'example_proof' opens an empty proof body;
wenzelm
parents: 36348
diff changeset
   397
experiment with Isar, without producing any persistent result.
5ab0f8859f9f command 'example_proof' opens an empty proof body;
wenzelm
parents: 36348
diff changeset
   398
35413
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35401
diff changeset
   399
* Commands 'type_notation' and 'no_type_notation' declare type syntax
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35401
diff changeset
   400
within a local theory context, with explicit checking of the
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35401
diff changeset
   401
constructors involved (in contrast to the raw 'syntax' versions).
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35401
diff changeset
   402
36178
0e5c133b48b6 keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
wenzelm
parents: 36177
diff changeset
   403
* Commands 'types' and 'typedecl' now work within a local theory
0e5c133b48b6 keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
wenzelm
parents: 36177
diff changeset
   404
context -- without introducing dependencies on parameters or
0e5c133b48b6 keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
wenzelm
parents: 36177
diff changeset
   405
assumptions, which is not possible in Isabelle/Pure.
35681
8b22a498b034 localized typedecl;
wenzelm
parents: 35613
diff changeset
   406
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   407
* Command 'defaultsort' has been renamed to 'default_sort', it works
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   408
within a local theory context.  Minor INCOMPATIBILITY.
36454
f2b5bcc61a8c command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;
wenzelm
parents: 36446
diff changeset
   409
34170
254ac75e4c38 reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents: 34076
diff changeset
   410
33993
haftmann
parents: 33873
diff changeset
   411
*** HOL ***
haftmann
parents: 33873
diff changeset
   412
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   413
* Command 'typedef' now works within a local theory context -- without
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   414
introducing dependencies on parameters or assumptions, which is not
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   415
possible in Isabelle/Pure/HOL.  Note that the logical environment may
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   416
contain multiple interpretations of local typedefs (with different
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   417
non-emptiness proofs), even in a global theory context.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   418
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   419
* New package for quotient types.  Commands 'quotient_type' and
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   420
'quotient_definition' may be used for defining types and constants by
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   421
quotient constructions.  An example is the type of integers created by
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   422
quotienting pairs of natural numbers:
37380
35815ce9218a final tuning;
wenzelm
parents: 37375
diff changeset
   423
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   424
  fun
37380
35815ce9218a final tuning;
wenzelm
parents: 37375
diff changeset
   425
    intrel :: "(nat * nat) => (nat * nat) => bool"
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   426
  where
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   427
    "intrel (x, y) (u, v) = (x + v = u + y)"
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   428
37380
35815ce9218a final tuning;
wenzelm
parents: 37375
diff changeset
   429
  quotient_type int = "nat * nat" / intrel
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   430
    by (auto simp add: equivp_def expand_fun_eq)
37380
35815ce9218a final tuning;
wenzelm
parents: 37375
diff changeset
   431
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   432
  quotient_definition
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   433
    "0::int" is "(0::nat, 0::nat)"
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   434
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   435
The method "lifting" can be used to lift of theorems from the
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   436
underlying "raw" type to the quotient type.  The example
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   437
src/HOL/Quotient_Examples/FSet.thy includes such a quotient
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   438
construction and provides a reasoning infrastructure for finite sets.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   439
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   440
* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   441
clash with new theory Quotient in Main HOL.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   442
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   443
* Moved the SMT binding into the main HOL session, eliminating
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   444
separate HOL-SMT session.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   445
37020
6c699a8e6927 turned old-style mem into an input abbreviation
haftmann
parents: 36979
diff changeset
   446
* List membership infix mem operation is only an input abbreviation.
6c699a8e6927 turned old-style mem into an input abbreviation
haftmann
parents: 36979
diff changeset
   447
INCOMPATIBILITY.
6c699a8e6927 turned old-style mem into an input abbreviation
haftmann
parents: 36979
diff changeset
   448
37144
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   449
* Theory Library/Word.thy has been removed.  Use library Word/Word.thy
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   450
for future developements; former Library/Word.thy is still present in
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   451
the AFP entry RSAPPS.
36963
9a017146675f dropped old Library/Word.thy and toy example ex/Adder.thy
haftmann
parents: 36953
diff changeset
   452
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   453
* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   454
longer shadowed.  INCOMPATIBILITY.
36808
cbeb3484fa07 theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
haftmann
parents: 36714
diff changeset
   455
36836
49156805321c removed lemma real_sq_order; use power2_le_imp_le instead
huffman
parents: 36830
diff changeset
   456
* Dropped theorem duplicate comp_arith; use semiring_norm instead.
49156805321c removed lemma real_sq_order; use power2_le_imp_le instead
huffman
parents: 36830
diff changeset
   457
INCOMPATIBILITY.
49156805321c removed lemma real_sq_order; use power2_le_imp_le instead
huffman
parents: 36830
diff changeset
   458
49156805321c removed lemma real_sq_order; use power2_le_imp_le instead
huffman
parents: 36830
diff changeset
   459
* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
49156805321c removed lemma real_sq_order; use power2_le_imp_le instead
huffman
parents: 36830
diff changeset
   460
INCOMPATIBILITY.
36714
ae84ddf03c58 dropped duplicate comp_arith
haftmann
parents: 36645
diff changeset
   461
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   462
* Dropped normalizing_semiring etc; use the facts in semiring classes
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   463
instead.  INCOMPATIBILITY.
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   464
36979
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   465
* Dropped several real-specific versions of lemmas about floor and
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   466
ceiling; use the generic lemmas from theory "Archimedean_Field"
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   467
instead.  INCOMPATIBILITY.
36979
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   468
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   469
  floor_number_of_eq         ~> floor_number_of
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   470
  le_floor_eq_number_of      ~> number_of_le_floor
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   471
  le_floor_eq_zero           ~> zero_le_floor
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   472
  le_floor_eq_one            ~> one_le_floor
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   473
  floor_less_eq_number_of    ~> floor_less_number_of
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   474
  floor_less_eq_zero         ~> floor_less_zero
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   475
  floor_less_eq_one          ~> floor_less_one
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   476
  less_floor_eq_number_of    ~> number_of_less_floor
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   477
  less_floor_eq_zero         ~> zero_less_floor
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   478
  less_floor_eq_one          ~> one_less_floor
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   479
  floor_le_eq_number_of      ~> floor_le_number_of
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   480
  floor_le_eq_zero           ~> floor_le_zero
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   481
  floor_le_eq_one            ~> floor_le_one
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   482
  floor_subtract_number_of   ~> floor_diff_number_of
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   483
  floor_subtract_one         ~> floor_diff_one
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   484
  ceiling_number_of_eq       ~> ceiling_number_of
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   485
  ceiling_le_eq_number_of    ~> ceiling_le_number_of
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   486
  ceiling_le_zero_eq         ~> ceiling_le_zero
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   487
  ceiling_le_eq_one          ~> ceiling_le_one
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   488
  less_ceiling_eq_number_of  ~> number_of_less_ceiling
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   489
  less_ceiling_eq_zero       ~> zero_less_ceiling
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   490
  less_ceiling_eq_one        ~> one_less_ceiling
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   491
  ceiling_less_eq_number_of  ~> ceiling_less_number_of
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   492
  ceiling_less_eq_zero       ~> ceiling_less_zero
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   493
  ceiling_less_eq_one        ~> ceiling_less_one
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   494
  le_ceiling_eq_number_of    ~> number_of_le_ceiling
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   495
  le_ceiling_eq_zero         ~> zero_le_ceiling
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   496
  le_ceiling_eq_one          ~> one_le_ceiling
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   497
  ceiling_subtract_number_of ~> ceiling_diff_number_of
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   498
  ceiling_subtract_one       ~> ceiling_diff_one
da7c06ab3169 remove several redundant lemmas about floor and ceiling
huffman
parents: 36972
diff changeset
   499
37144
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   500
* Theory "Finite_Set": various folding_XXX locales facilitate the
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   501
application of the various fold combinators on finite sets.
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   502
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   503
* Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   504
provides abstract red-black tree type which is backed by "RBT_Impl" as
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   505
implementation.  INCOMPATIBILTY.
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36096
diff changeset
   506
36830
7902dc7ea11d fix spelling of 'superseded'
huffman
parents: 36829
diff changeset
   507
* Theory Library/Coinductive_List has been removed -- superseded by
35763
765f8adf10f9 removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
wenzelm
parents: 35745
diff changeset
   508
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
   509
36829
909d2680e122 NEWS: removed theory PReal
huffman
parents: 36828
diff changeset
   510
* Theory PReal, including the type "preal" and related operations, has
909d2680e122 NEWS: removed theory PReal
huffman
parents: 36828
diff changeset
   511
been removed.  INCOMPATIBILITY.
909d2680e122 NEWS: removed theory PReal
huffman
parents: 36828
diff changeset
   512
37380
35815ce9218a final tuning;
wenzelm
parents: 37375
diff changeset
   513
* Real: new development using Cauchy Sequences.
35815ce9218a final tuning;
wenzelm
parents: 37375
diff changeset
   514
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   515
* Split off theory "Big_Operators" containing setsum, setprod,
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   516
Inf_fin, Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   517
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   518
* Theory "Rational" renamed to "Rat", for consistency with "Nat",
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   519
"Int" etc.  INCOMPATIBILITY.
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   520
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   521
* Constant Rat.normalize needs to be qualified.  INCOMPATIBILITY.
37143
2a5182751151 constant Rat.normalize needs to be qualified;
wenzelm
parents: 37087
diff changeset
   522
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   523
* New set of rules "ac_simps" provides combined assoc / commute
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   524
rewrites for all interpretations of the appropriate generic locales.
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   525
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   526
* Renamed theory "OrderedGroup" to "Groups" and split theory
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   527
"Ring_and_Field" into theories "Rings" and "Fields"; for more
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   528
appropriate and more consistent names suitable for name prefixes
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   529
within the HOL theories.  INCOMPATIBILITY.
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35042
diff changeset
   530
35084
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   531
* Some generic constants have been put to appropriate theories:
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   532
  - less_eq, less: Orderings
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   533
  - zero, one, plus, minus, uminus, times, abs, sgn: Groups
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   534
  - inverse, divide: Rings
35084
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   535
INCOMPATIBILITY.
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   536
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   537
* More consistent naming of type classes involving orderings (and
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   538
lattices):
35027
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   539
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   540
    lower_semilattice                   ~> semilattice_inf
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   541
    upper_semilattice                   ~> semilattice_sup
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   542
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   543
    dense_linear_order                  ~> dense_linorder
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   544
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   545
    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
   546
    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
   547
    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
   548
    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
   549
    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
   550
    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
   551
    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
   552
    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
   553
    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
   554
    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
   555
    pordered_ring                       ~> ordered_ring
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   556
    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
   557
    pordered_semiring                   ~> ordered_semiring
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   558
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   559
    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
   560
    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
   561
    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
   562
    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
   563
    ordered_field                       ~> linordered_field
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   564
    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
   565
    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
   566
    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
   567
    ordered_idom                        ~> linordered_idom
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   568
    ordered_ring                        ~> linordered_ring
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   569
    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
   570
    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
   571
    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
   572
    ordered_semidom                     ~> linordered_semidom
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   573
    ordered_semiring                    ~> linordered_semiring
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   574
    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
   575
    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
   576
    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
   577
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   578
  The following slightly odd type classes have been moved to a
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   579
  separate theory Library/Lattice_Algebras:
35032
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 35027
diff changeset
   580
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 35027
diff changeset
   581
    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
   582
    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
   583
    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
   584
    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
   585
    lordered_ring                       ~> lattice_ring
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 35027
diff changeset
   586
35027
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   587
INCOMPATIBILITY.
ed7d12bcf8f8 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   588
36416
9459be72b89e NEWS and CONTRIBUTORS
haftmann
parents: 36356
diff changeset
   589
* Refined field classes:
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   590
  - classes division_ring_inverse_zero, field_inverse_zero,
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   591
    linordered_field_inverse_zero include rule inverse 0 = 0 --
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   592
    subsumes former division_by_zero class;
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   593
  - numerous lemmas have been ported from field to division_ring.
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   594
INCOMPATIBILITY.
36416
9459be72b89e NEWS and CONTRIBUTORS
haftmann
parents: 36356
diff changeset
   595
9459be72b89e NEWS and CONTRIBUTORS
haftmann
parents: 36356
diff changeset
   596
* Refined algebra theorem collections:
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   597
  - dropped theorem group group_simps, use algebra_simps instead;
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   598
  - dropped theorem group ring_simps, use field_simps instead;
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   599
  - proper theorem collection field_simps subsumes former theorem
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   600
    groups field_eq_simps and field_simps;
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   601
  - dropped lemma eq_minus_self_iff which is a duplicate for
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   602
    equal_neg_zero.
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   603
INCOMPATIBILITY.
35009
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   604
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   605
* 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
   606
sets to lattices:
e3daf3c07381 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents: 34062
diff changeset
   607
34007
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   608
  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
   609
  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
   610
  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
   611
  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
   612
  Inter_fold_inter              ~> Inf_fold_inf
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   613
  Union_fold_union              ~> Sup_fold_sup
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   614
  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
   615
  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
   616
  INTER_fold_inter              ~> INFI_fold_inf
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   617
  UNION_fold_union              ~> SUPR_fold_sup
aea892559fc5 tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents: 33994
diff changeset
   618
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   619
* Theory "Complete_Lattice": lemmas top_def and bot_def have been
36416
9459be72b89e NEWS and CONTRIBUTORS
haftmann
parents: 36356
diff changeset
   620
replaced by the more convenient lemmas Inf_empty and Sup_empty.
9459be72b89e NEWS and CONTRIBUTORS
haftmann
parents: 36356
diff changeset
   621
Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
9459be72b89e NEWS and CONTRIBUTORS
haftmann
parents: 36356
diff changeset
   622
by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace
9459be72b89e NEWS and CONTRIBUTORS
haftmann
parents: 36356
diff changeset
   623
former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right
9459be72b89e NEWS and CONTRIBUTORS
haftmann
parents: 36356
diff changeset
   624
subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.
9459be72b89e NEWS and CONTRIBUTORS
haftmann
parents: 36356
diff changeset
   625
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   626
* Reorganized theory Multiset: swapped notation of pointwise and
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   627
multiset order:
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   628
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   629
  - pointwise ordering is instance of class order with standard syntax
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   630
    <= and <;
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   631
  - multiset ordering has syntax <=# and <#; partial order properties
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   632
    are provided by means of interpretation with prefix
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   633
    multiset_order;
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   634
  - less duplication, less historical organization of sections,
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   635
    conversion from associations lists to multisets, rudimentary code
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   636
    generation;
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   637
  - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   638
    if needed.
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   639
36903
489c1fbbb028 Multiset: renamed, added and tuned lemmas;
nipkow
parents: 36857
diff changeset
   640
Renamed:
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   641
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   642
  multiset_eq_conv_count_eq  ~>  multiset_ext_iff
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   643
  multi_count_ext  ~>  multiset_ext
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   644
  diff_union_inverse2  ~>  diff_union_cancelR
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   645
36857
59ed53700145 minor tuning;
wenzelm
parents: 36856
diff changeset
   646
INCOMPATIBILITY.
36416
9459be72b89e NEWS and CONTRIBUTORS
haftmann
parents: 36356
diff changeset
   647
36903
489c1fbbb028 Multiset: renamed, added and tuned lemmas;
nipkow
parents: 36857
diff changeset
   648
* Theory Permutation: replaced local "remove" by List.remove1.
489c1fbbb028 Multiset: renamed, added and tuned lemmas;
nipkow
parents: 36857
diff changeset
   649
36416
9459be72b89e NEWS and CONTRIBUTORS
haftmann
parents: 36356
diff changeset
   650
* Code generation: ML and OCaml code is decorated with signatures.
9459be72b89e NEWS and CONTRIBUTORS
haftmann
parents: 36356
diff changeset
   651
35009
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   652
* Theory List: added transpose.
5408e5207131 misc tuning;
wenzelm
parents: 34974
diff changeset
   653
35810
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   654
* Library/Nat_Bijection.thy is a collection of bijective functions
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   655
between nat and other types, which supersedes the older libraries
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   656
Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy.  INCOMPATIBILITY.
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   657
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   658
  Constants:
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   659
  Nat_Int_Bij.nat2_to_nat         ~> prod_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   660
  Nat_Int_Bij.nat_to_nat2         ~> prod_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   661
  Nat_Int_Bij.int_to_nat_bij      ~> int_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   662
  Nat_Int_Bij.nat_to_int_bij      ~> int_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   663
  Countable.pair_encode           ~> prod_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   664
  NatIso.prod2nat                 ~> prod_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   665
  NatIso.nat2prod                 ~> prod_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   666
  NatIso.sum2nat                  ~> sum_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   667
  NatIso.nat2sum                  ~> sum_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   668
  NatIso.list2nat                 ~> list_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   669
  NatIso.nat2list                 ~> list_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   670
  NatIso.set2nat                  ~> set_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   671
  NatIso.nat2set                  ~> set_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   672
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   673
  Lemmas:
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   674
  Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   675
  Nat_Int_Bij.nat2_to_nat_inj     ~> inj_prod_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   676
  Nat_Int_Bij.nat2_to_nat_surj    ~> surj_prod_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   677
  Nat_Int_Bij.nat_to_nat2_inj     ~> inj_prod_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   678
  Nat_Int_Bij.nat_to_nat2_surj    ~> surj_prod_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   679
  Nat_Int_Bij.i2n_n2i_id          ~> int_encode_inverse
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   680
  Nat_Int_Bij.n2i_i2n_id          ~> int_decode_inverse
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   681
  Nat_Int_Bij.surj_nat_to_int_bij ~> surj_int_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   682
  Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   683
  Nat_Int_Bij.inj_nat_to_int_bij  ~> inj_int_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   684
  Nat_Int_Bij.inj_int_to_nat_bij  ~> inj_int_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   685
  Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   686
  Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode
a50237ec0ecd NEWS: Nat_Bijection library
huffman
parents: 35765
diff changeset
   687
36929
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   688
* Sledgehammer:
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   689
  - Renamed ATP commands:
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   690
    atp_info     ~> sledgehammer running_atps
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   691
    atp_kill     ~> sledgehammer kill_atps
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   692
    atp_messages ~> sledgehammer messages
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   693
    atp_minimize ~> sledgehammer minimize
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   694
    print_atps   ~> sledgehammer available_atps
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   695
    INCOMPATIBILITY.
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   696
  - Added user's manual ("isabelle doc sledgehammer").
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   697
  - Added option syntax and "sledgehammer_params" to customize
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   698
    Sledgehammer's behavior.  See the manual for details.
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   699
  - Modified the Isar proof reconstruction code so that it produces
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   700
    direct proofs rather than proofs by contradiction.  (This feature
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   701
    is still experimental.)
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   702
  - Made Isar proof reconstruction work for SPASS, remote ATPs, and in
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   703
    full-typed mode.
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   704
  - Added support for TPTP syntax for SPASS via the "spass_tptp" ATP.
6b8b4f519190 added some Sledgehammer news
blanchet
parents: 36928
diff changeset
   705
36928
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   706
* Nitpick:
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   707
  - Added and implemented "binary_ints" and "bits" options.
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   708
  - Added "std" option and implemented support for nonstandard models.
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   709
  - Added and implemented "finitize" option to improve the precision
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   710
    of infinite datatypes based on a monotonicity analysis.
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   711
  - Added support for quotient types.
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   712
  - Added support for "specification" and "ax_specification"
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   713
    constructs.
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   714
  - Added support for local definitions (for "function" and
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   715
    "termination" proofs).
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   716
  - Added support for term postprocessors.
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   717
  - Optimized "Multiset.multiset" and "FinFun.finfun".
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   718
  - Improved efficiency of "destroy_constrs" optimization.
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   719
  - Fixed soundness bugs related to "destroy_constrs" optimization and
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   720
    record getters.
37272
e0940e692abb update NEWS
blanchet
parents: 37264
diff changeset
   721
  - Fixed soundness bug related to higher-order constructors.
e0940e692abb update NEWS
blanchet
parents: 37264
diff changeset
   722
  - Fixed soundness bug when "full_descrs" is enabled.
36928
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   723
  - Improved precision of set constructs.
37260
dde817e6dfb1 added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents: 37158
diff changeset
   724
  - Added "atoms" option.
36928
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   725
  - Added cache to speed up repeated Kodkod invocations on the same
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   726
    problems.
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   727
  - Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   728
    "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   729
    "SAT4J_Light".  INCOMPATIBILITY.
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   730
  - Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   731
    "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.
37264
8b931fb51cc6 removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
blanchet
parents: 37260
diff changeset
   732
  - Removed "nitpick_intro" attribute.  INCOMPATIBILITY.
36928
637100169bc7 document Nitpick changes
blanchet
parents: 36903
diff changeset
   733
37361
250f487b3034 Documented changes in induct, cases, and nominal_induct method.
berghofe
parents: 37352
diff changeset
   734
* Method "induct" now takes instantiations of the form t, where t is not
250f487b3034 Documented changes in induct, cases, and nominal_induct method.
berghofe
parents: 37352
diff changeset
   735
  a variable, as a shorthand for "x == t", where x is a fresh variable.
250f487b3034 Documented changes in induct, cases, and nominal_induct method.
berghofe
parents: 37352
diff changeset
   736
  If this is not intended, t has to be enclosed in parentheses.
250f487b3034 Documented changes in induct, cases, and nominal_induct method.
berghofe
parents: 37352
diff changeset
   737
  By default, the equalities generated by definitional instantiations
250f487b3034 Documented changes in induct, cases, and nominal_induct method.
berghofe
parents: 37352
diff changeset
   738
  are pre-simplified, which may cause parameters of inductive cases
250f487b3034 Documented changes in induct, cases, and nominal_induct method.
berghofe
parents: 37352
diff changeset
   739
  to disappear, or may even delete some of the inductive cases.
250f487b3034 Documented changes in induct, cases, and nominal_induct method.
berghofe
parents: 37352
diff changeset
   740
  Use "induct (no_simp)" instead of "induct" to restore the old
250f487b3034 Documented changes in induct, cases, and nominal_induct method.
berghofe
parents: 37352
diff changeset
   741
  behaviour. The (no_simp) option is also understood by the "cases"
250f487b3034 Documented changes in induct, cases, and nominal_induct method.
berghofe
parents: 37352
diff changeset
   742
  and "nominal_induct" methods, which now perform pre-simplification, too.
250f487b3034 Documented changes in induct, cases, and nominal_induct method.
berghofe
parents: 37352
diff changeset
   743
  INCOMPATIBILITY.
250f487b3034 Documented changes in induct, cases, and nominal_induct method.
berghofe
parents: 37352
diff changeset
   744
33993
haftmann
parents: 33873
diff changeset
   745
36828
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   746
*** HOLCF ***
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   747
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   748
* Variable names in lemmas generated by the domain package have
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   749
changed; the naming scheme is now consistent with the HOL datatype
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   750
package.  Some proof scripts may be affected, INCOMPATIBILITY.
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   751
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   752
* The domain package no longer defines the function "foo_copy" for
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   753
recursive domain "foo".  The reach lemma is now stated directly in
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   754
terms of "foo_take".  Lemmas and proofs that mention "foo_copy" must
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   755
be reformulated in terms of "foo_take", INCOMPATIBILITY.
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   756
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   757
* Most definedness lemmas generated by the domain package (previously
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   758
of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   759
like "foo$x = UU <-> x = UU", which works better as a simp rule.
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   760
Proofs that used definedness lemmas as intro rules may break,
36828
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   761
potential INCOMPATIBILITY.
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   762
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   763
* Induction and casedist rules generated by the domain package now
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   764
declare proper case_names (one called "bottom", and one named for each
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   765
constructor).  INCOMPATIBILITY.
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   766
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   767
* For mutually-recursive domains, separate "reach" and "take_lemma"
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   768
rules are generated for each domain, INCOMPATIBILITY.
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   769
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   770
  foo_bar.reach       ~> foo.reach  bar.reach
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   771
  foo_bar.take_lemmas ~> foo.take_lemma  bar.take_lemma
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   772
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   773
* Some lemmas generated by the domain package have been renamed for
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   774
consistency with the datatype package, INCOMPATIBILITY.
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   775
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   776
  foo.ind        ~> foo.induct
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   777
  foo.finite_ind ~> foo.finite_induct
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   778
  foo.coind      ~> foo.coinduct
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   779
  foo.casedist   ~> foo.exhaust
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   780
  foo.exhaust    ~> foo.nchotomy
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   781
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   782
* For consistency with other definition packages, the fixrec package
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   783
now generates qualified theorem names, INCOMPATIBILITY.
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   784
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   785
  foo_simps  ~> foo.simps
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   786
  foo_unfold ~> foo.unfold
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   787
  foo_induct ~> foo.induct
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   788
37087
dd47971b9875 NEWS: removed fixrec_simp attribute
huffman
parents: 37020
diff changeset
   789
* The "fixrec_simp" attribute has been removed.  The "fixrec_simp"
dd47971b9875 NEWS: removed fixrec_simp attribute
huffman
parents: 37020
diff changeset
   790
method and internal fixrec proofs now use the default simpset instead.
dd47971b9875 NEWS: removed fixrec_simp attribute
huffman
parents: 37020
diff changeset
   791
INCOMPATIBILITY.
dd47971b9875 NEWS: removed fixrec_simp attribute
huffman
parents: 37020
diff changeset
   792
36828
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   793
* The "contlub" predicate has been removed.  Proof scripts should use
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   794
lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   795
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   796
* The "admw" predicate has been removed, INCOMPATIBILITY.
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   797
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   798
* The constants cpair, cfst, and csnd have been removed in favor of
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   799
Pair, fst, and snd from Isabelle/HOL, INCOMPATIBILITY.
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   800
6a47f043d498 collected NEWS updates for HOLCF
huffman
parents: 36811
diff changeset
   801
33993
haftmann
parents: 33873
diff changeset
   802
*** ML ***
haftmann
parents: 33873
diff changeset
   803
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   804
* Antiquotations for basic formal entities:
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   805
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   806
    @{class NAME}         -- type class
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   807
    @{class_syntax NAME}  -- syntax representation of the above
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   808
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   809
    @{type_name NAME}     -- logical type
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   810
    @{type_abbrev NAME}   -- type abbreviation
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   811
    @{nonterminal NAME}   -- type of concrete syntactic category
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   812
    @{type_syntax NAME}   -- syntax representation of any of the above
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   813
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   814
    @{const_name NAME}    -- logical constant (INCOMPATIBILITY)
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   815
    @{const_abbrev NAME}  -- abbreviated constant
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   816
    @{const_syntax NAME}  -- syntax representation of any of the above
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   817
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   818
* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   819
syntax constant (cf. 'syntax' command).
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   820
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   821
* Antiquotation @{make_string} inlines a function to print arbitrary
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   822
values similar to the ML toplevel.  The result is compiler dependent
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   823
and may fall back on "?" in certain situations.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   824
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   825
* Diagnostic commands 'ML_val' and 'ML_command' may refer to
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   826
antiquotations @{Isar.state} and @{Isar.goal}.  This replaces impure
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   827
Isar.state() and Isar.goal(), which belong to the old TTY loop and do
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   828
not work with the asynchronous Isar document model.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   829
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   830
* Configuration options now admit dynamic default values, depending on
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   831
the context or even global references.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   832
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   833
* SHA1.digest digests strings according to SHA-1 (see RFC 3174).  It
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   834
uses an efficient external library if available (for Poly/ML).
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   835
37144
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   836
* Renamed some important ML structures, while keeping the old names
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   837
for some time as aliases within the structure Legacy:
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   838
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   839
  OuterKeyword  ~>  Keyword
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   840
  OuterLex      ~>  Token
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   841
  OuterParse    ~>  Parse
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   842
  OuterSyntax   ~>  Outer_Syntax
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37158
diff changeset
   843
  PrintMode     ~>  Print_Mode
37144
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   844
  SpecParse     ~>  Parse_Spec
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37158
diff changeset
   845
  ThyInfo       ~>  Thy_Info
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37158
diff changeset
   846
  ThyLoad       ~>  Thy_Load
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37158
diff changeset
   847
  ThyOutput     ~>  Thy_Output
37145
01aa36932739 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
wenzelm
parents: 37144
diff changeset
   848
  TypeInfer     ~>  Type_Infer
37144
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   849
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   850
Note that "open Legacy" simplifies porting of sources, but forgetting
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   851
to remove it again will complicate porting again in the future.
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   852
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   853
* Most operations that refer to a global context are named
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   854
accordingly, e.g. Simplifier.global_context or
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   855
ProofContext.init_global.  There are some situations where a global
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   856
context actually works, but under normal circumstances one needs to
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   857
pass the proper local context through the code!
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   858
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   859
* Discontinued old TheoryDataFun with its copy/init operation -- data
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   860
needs to be pure.  Functor Theory_Data_PP retains the traditional
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   861
Pretty.pp argument to merge, which is absent in the standard
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   862
Theory_Data version.
36429
9d6b3be996d4 monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
wenzelm
parents: 36416
diff changeset
   863
37144
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   864
* Sorts.certify_sort and derived "cert" operations for types and terms
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   865
no longer minimize sorts.  Thus certification at the boundary of the
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   866
inference kernel becomes invariant under addition of class relations,
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   867
which is an important monotonicity principle.  Sorts are now minimized
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   868
in the syntax layer only, at the boundary between the end-user and the
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   869
system.  Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   870
explicitly in rare situations.
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   871
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
   872
* 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
   873
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
   874
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
   875
34076
e3daf3c07381 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents: 34062
diff changeset
   876
* 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
   877
usual for resolution.  Rare INCOMPATIBILITY.
e3daf3c07381 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents: 34062
diff changeset
   878
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
   879
* 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
   880
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
   881
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
   882
37144
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   883
* Curried take and drop in library.ML; negative length is interpreted
fd6308b4df72 misc updates for release;
wenzelm
parents: 37143
diff changeset
   884
as infinity (as in chop).  Subtle INCOMPATIBILITY.
36961
7b14afc02fc4 do not open Legacy by default;
wenzelm
parents: 36959
diff changeset
   885
37351
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   886
* Proof terms: type substitutions on proof constants now use canonical
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   887
order of type variables.  INCOMPATIBILITY for tools working with proof
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   888
terms.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   889
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   890
* Raw axioms/defs may no longer carry sort constraints, and raw defs
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   891
may no longer carry premises.  User-level specifications are
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   892
transformed accordingly by Thm.add_axiom/add_def.
f34699c3e98e more NEWS;
wenzelm
parents: 37316
diff changeset
   893
33993
haftmann
parents: 33873
diff changeset
   894
34238
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   895
*** System ***
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   896
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   897
* Discontinued special HOL_USEDIR_OPTIONS for the main HOL image;
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   898
ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions.  Note that
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   899
proof terms are enabled unconditionally in the new HOL-Proofs image.
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   900
34255
2dd2547acb41 discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents: 34238
diff changeset
   901
* Discontinued old ISABELLE and ISATOOL environment settings (legacy
2dd2547acb41 discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents: 34238
diff changeset
   902
feature since Isabelle2009).  Use ISABELLE_PROCESS and ISABELLE_TOOL,
2dd2547acb41 discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents: 34238
diff changeset
   903
respectively.
2dd2547acb41 discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents: 34238
diff changeset
   904
36201
07d4f74abd12 polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents: 36178
diff changeset
   905
* Old lib/scripts/polyml-platform is superseded by the
07d4f74abd12 polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents: 36178
diff changeset
   906
ISABELLE_PLATFORM setting variable, which defaults to the 32 bit
07d4f74abd12 polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents: 36178
diff changeset
   907
variant, even on a 64 bit machine.  The following example setting
07d4f74abd12 polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents: 36178
diff changeset
   908
prefers 64 bit if available:
07d4f74abd12 polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents: 36178
diff changeset
   909
07d4f74abd12 polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents: 36178
diff changeset
   910
  ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
07d4f74abd12 polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents: 36178
diff changeset
   911
37218
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents: 37216
diff changeset
   912
* The preliminary Isabelle/jEdit application demonstrates the emerging
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents: 37216
diff changeset
   913
Isabelle/Scala layer for advanced prover interaction and integration.
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents: 37216
diff changeset
   914
See src/Tools/jEdit or "isabelle jedit" provided by the properly built
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents: 37216
diff changeset
   915
component.
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents: 37216
diff changeset
   916
37375
02592ec68afb NEWS: IsabelleText font;
wenzelm
parents: 37361
diff changeset
   917
* "IsabelleText" is a Unicode font derived from Bitstream Vera Mono
02592ec68afb NEWS: IsabelleText font;
wenzelm
parents: 37361
diff changeset
   918
and Bluesky TeX fonts.  It provides the usual Isabelle symbols,
02592ec68afb NEWS: IsabelleText font;
wenzelm
parents: 37361
diff changeset
   919
similar to the default assignment of the document preparation system
02592ec68afb NEWS: IsabelleText font;
wenzelm
parents: 37361
diff changeset
   920
(cf. isabellesym.sty).  The Isabelle/Scala class Isabelle_System
02592ec68afb NEWS: IsabelleText font;
wenzelm
parents: 37361
diff changeset
   921
provides some operations for direct access to the font without asking
02592ec68afb NEWS: IsabelleText font;
wenzelm
parents: 37361
diff changeset
   922
the user for manual installation.
02592ec68afb NEWS: IsabelleText font;
wenzelm
parents: 37361
diff changeset
   923
34238
b28be884edda discontinued special HOL_USEDIR_OPTIONS;
wenzelm
parents: 34170
diff changeset
   924
33993
haftmann
parents: 33873
diff changeset
   925
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   926
New in Isabelle2009-1 (December 2009)
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   927
-------------------------------------
30904
cc6a6047a10f back to non-release mode;
wenzelm
parents: 30855
diff changeset
   928
31547
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   929
*** General ***
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   930
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   931
* Discontinued old form of "escaped symbols" such as \\<forall>.  Only
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   932
one backslash should be used, even in ML sources.
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   933
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
   934
30951
a6e26a248f03 formal declaration of undefined parameters after class instantiation
haftmann
parents: 30949
diff changeset
   935
*** Pure ***
a6e26a248f03 formal declaration of undefined parameters after class instantiation
haftmann
parents: 30949
diff changeset
   936
32846
29941e925c82 News entry: inheritance of mixins; print_interps.
ballarin
parents: 32775
diff changeset
   937
* Locale interpretation propagates mixins along the locale hierarchy.
29941e925c82 News entry: inheritance of mixins; print_interps.
ballarin
parents: 32775
diff changeset
   938
The currently only available mixins are the equations used to map
29941e925c82 News entry: inheritance of mixins; print_interps.
ballarin
parents: 32775
diff changeset
   939
local definitions to terms of the target domain of an interpretation.
29941e925c82 News entry: inheritance of mixins; print_interps.
ballarin
parents: 32775
diff changeset
   940
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   941
* Reactivated diagnostic command 'print_interps'.  Use "print_interps
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   942
loc" to print all interpretations of locale "loc" in the theory.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   943
Interpretations in proofs are not shown.
32846
29941e925c82 News entry: inheritance of mixins; print_interps.
ballarin
parents: 32775
diff changeset
   944
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32846
diff changeset
   945
* Thoroughly revised locales tutorial.  New section on conditional
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32846
diff changeset
   946
interpretation.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32846
diff changeset
   947
33843
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   948
* On instantiation of classes, remaining undefined class parameters
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   949
are formally declared.  INCOMPATIBILITY.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   950
30951
a6e26a248f03 formal declaration of undefined parameters after class instantiation
haftmann
parents: 30949
diff changeset
   951
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   952
*** Document preparation ***
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   953
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   954
* New generalized style concept for printing terms: @{foo (style) ...}
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   955
instead of @{foo_style style ...}  (old form is still retained for
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   956
backward compatibility).  Styles can be also applied for
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   957
antiquotations prop, term_type and typeof.
32891
d403b99287ff new generalized concept for term styles
haftmann
parents: 32846
diff changeset
   958
d403b99287ff new generalized concept for term styles
haftmann
parents: 32846
diff changeset
   959
30930
11010e5f18f0 tightended specification of class semiring_div
haftmann
parents: 30855
diff changeset
   960
*** HOL ***
11010e5f18f0 tightended specification of class semiring_div
haftmann
parents: 30855
diff changeset
   961
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   962
* 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
   963
equality, linear and nonlinear (natural/integer/real) arithmetic, and
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   964
fixed-size bitvectors; there is also basic support for higher-order
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   965
features (esp. lambda abstractions).  It is an incomplete decision
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   966
procedure based on external SMT solvers using the oracle mechanism;
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   967
for the SMT solver Z3, this method is proof-producing.  Certificates
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   968
are provided to avoid calling the external solvers solely for
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   969
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
   970
installing SMT solvers locally.  See src/HOL/SMT.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   971
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   972
* New commands to load and prove verification conditions generated by
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   973
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
   974
Compiler (VCC) or Spec#).  See src/HOL/Boogie.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   975
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   976
* New counterexample generator tool 'nitpick' based on the Kodkod
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   977
relational model finder.  See src/HOL/Tools/Nitpick and
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   978
src/HOL/Nitpick_Examples.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
   979
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   980
* New commands 'code_pred' and 'values' to invoke the predicate
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   981
compiler and to enumerate values of inductive predicates.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   982
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   983
* A tabled implementation of the reflexive transitive closure.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   984
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   985
* New implementation of quickcheck uses generic code generator;
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   986
default generators are provided for all suitable HOL types, records
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   987
and datatypes.  Old quickcheck can be re-activated importing theory
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   988
Library/SML_Quickcheck.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
   989
33843
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   990
* New testing tool Mirabelle for automated proof tools.  Applies
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   991
several tools and tactics like sledgehammer, metis, or quickcheck, to
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   992
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
   993
"mirabelle" utility.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   994
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   995
* New proof method "sos" (sum of squares) for nonlinear real
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   996
arithmetic (originally due to John Harison). It requires theory
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   997
Library/Sum_Of_Squares.  It is not a complete decision procedure but
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   998
works well in practice on quantifier-free real arithmetic with +, -,
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
   999
*, ^, =, <= and <, i.e. boolean combinations of equalities and
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1000
inequalities between polynomials.  It makes use of external
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1001
semidefinite programming solvers.  Method "sos" generates a
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1002
certificate that can be pasted into the proof thus avoiding the need
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1003
to call an external tool every time the proof is checked.  See
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1004
src/HOL/Library/Sum_Of_Squares.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1005
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1006
* New method "linarith" invokes existing linear arithmetic decision
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1007
procedure only.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1008
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1009
* New command 'atp_minimal' reduces result produced by Sledgehammer.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1010
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1011
* New Sledgehammer option "Full Types" in Proof General settings menu.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1012
Causes full type information to be output to the ATPs.  This slows
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1013
ATPs down considerably but eliminates a source of unsound "proofs"
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1014
that fail later.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1015
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1016
* New method "metisFT": A version of metis that uses full type
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1017
information in order to avoid failures of proof reconstruction.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1018
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1019
* New evaluator "approximate" approximates an real valued term using
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1020
the same method as the approximation method.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1021
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1022
* Method "approximate" now supports arithmetic expressions as
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1023
boundaries of intervals and implements interval splitting and Taylor
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1024
series expansion.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1025
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1026
* ML antiquotation @{code_datatype} inserts definition of a datatype
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1027
generated by the code generator; e.g. see src/HOL/Predicate.thy.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1028
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1029
* New theory SupInf of the supremum and infimum operators for sets of
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1030
reals.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1031
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1032
* New theory Probability, which contains a development of measure
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1033
theory, eventually leading to Lebesgue integration and probability.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1034
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1035
* Extended Multivariate Analysis to include derivation and Brouwer's
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1036
fixpoint theorem.
33843
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1037
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1038
* Reorganization of number theory, INCOMPATIBILITY:
33873
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
  1039
  - new number theory development for nat and int, in theories Divides
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
  1040
    and GCD as well as in new session Number_Theory
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
  1041
  - some constants and facts now suffixed with _nat and _int
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
  1042
    accordingly
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
  1043
  - former session NumberTheory now named Old_Number_Theory, including
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
  1044
    theories Legacy_GCD and Primes (prefer Number_Theory if possible)
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1045
  - moved theory Pocklington from src/HOL/Library to
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1046
    src/HOL/Old_Number_Theory
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32463
diff changeset
  1047
33873
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
  1048
* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
  1049
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
  1050
lattice.
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1051
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1052
* Class semiring_div requires superclass no_zero_divisors and proof of
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1053
div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1054
div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1055
generalized to class semiring_div, subsuming former theorems
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1056
zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1057
zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1058
INCOMPATIBILITY.
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1059
32588
5e06a1634e55 Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents: 32485
diff changeset
  1060
* Refinements to lattice classes and sets:
32064
53ca12ff305d refinement of lattice classes
haftmann
parents: 31971
diff changeset
  1061
  - less default intro/elim rules in locale variant, more default
53ca12ff305d refinement of lattice classes
haftmann
parents: 31971
diff changeset
  1062
    intro/elim rules in class variant: more uniformity
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1063
  - 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
  1064
    le_inf_iff
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1065
  - 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
  1066
    sup_aci)
32064
53ca12ff305d refinement of lattice classes
haftmann
parents: 31971
diff changeset
  1067
  - renamed ACI to inf_sup_aci
32600
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1068
  - new class "boolean_algebra"
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1069
  - class "complete_lattice" moved to separate theory
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1070
    "Complete_Lattice"; corresponding constants (and abbreviations)
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1071
    renamed and with authentic syntax:
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1072
    Set.Inf ~>    Complete_Lattice.Inf
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1073
    Set.Sup ~>    Complete_Lattice.Sup
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1074
    Set.INFI ~>   Complete_Lattice.INFI
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1075
    Set.SUPR ~>   Complete_Lattice.SUPR
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1076
    Set.Inter ~>  Complete_Lattice.Inter
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1077
    Set.Union ~>  Complete_Lattice.Union
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1078
    Set.INTER ~>  Complete_Lattice.INTER
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1079
    Set.UNION ~>  Complete_Lattice.UNION
32600
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1080
  - authentic syntax for
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1081
    Set.Pow
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1082
    Set.image
32588
5e06a1634e55 Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents: 32485
diff changeset
  1083
  - mere abbreviations:
5e06a1634e55 Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents: 32485
diff changeset
  1084
    Set.empty               (for bot)
5e06a1634e55 Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents: 32485
diff changeset
  1085
    Set.UNIV                (for top)
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1086
    Set.inter               (for inf, formerly Set.Int)
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1087
    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
  1088
    Complete_Lattice.Inter  (for Inf)
5e06a1634e55 Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents: 32485
diff changeset
  1089
    Complete_Lattice.Union  (for Sup)
32606
b5c3a8a75772 INTER and UNION are mere abbreviations for INFI and SUPR
haftmann
parents: 32600
diff changeset
  1090
    Complete_Lattice.INTER  (for INFI)
b5c3a8a75772 INTER and UNION are mere abbreviations for INFI and SUPR
haftmann
parents: 32600
diff changeset
  1091
    Complete_Lattice.UNION  (for SUPR)
32600
1b3b0cc604ce tuned NEWS, added CONTRIBUTORS
haftmann
parents: 32597
diff changeset
  1092
  - object-logic definitions as far as appropriate
32217
haftmann
parents: 32216
diff changeset
  1093
32691
cdf70f1fc9f9 added note on simp rules
haftmann
parents: 32686
diff changeset
  1094
INCOMPATIBILITY.  Care is required when theorems Int_subset_iff or
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1095
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
  1096
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
  1097
deleted to achieve the desired effect.
32064
53ca12ff305d refinement of lattice classes
haftmann
parents: 31971
diff changeset
  1098
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1099
* 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
  1100
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
  1101
etc.  INCOMPATIBILITY.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1102
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1103
* 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
  1104
pred_set_conv by default.  INCOMPATIBILITY.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1105
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1106
* Power operations on relations and functions are now one dedicated
32706
b68f3afdc137 NEWS; corrected spelling
haftmann
parents: 32697
diff changeset
  1107
constant "compow" with infix syntax "^^".  Power operation on
31547
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
  1108
multiplicative monoids retains syntax "^" and is now defined generic
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
  1109
in class power.  INCOMPATIBILITY.
398c0f48a99e discontinued escaped symbols;
wenzelm
parents: 31481
diff changeset
  1110
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1111
* 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
  1112
"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
  1113
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
  1114
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
  1115
O_assoc[symmetric].  The same applies to the curried version "R OO S".
32427
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
  1116
33057
764547b68538 inv_onto -> inv_into
nipkow
parents: 33037
diff changeset
  1117
* 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
  1118
abbreviation for "inv_into UNIV".  Lemmas are renamed accordingly.
32988
d1d4d7a08a66 Inv -> inv_onto, inv abbr. inv_onto UNIV.
nipkow
parents: 32898
diff changeset
  1119
INCOMPATIBILITY.
d1d4d7a08a66 Inv -> inv_onto, inv abbr. inv_onto UNIV.
nipkow
parents: 32898
diff changeset
  1120
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1121
* Most rules produced by inductive and datatype package have mandatory
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1122
prefixes.  INCOMPATIBILITY.
31790
05c92381363c corrected and unified thm names
nipkow
parents: 31784
diff changeset
  1123
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1124
* 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
  1125
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
  1126
DERIV_intros assumes composition with an additional function and
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1127
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
  1128
Simplifier.  Hence (auto intro!: DERIV_intros) computes the derivative
33873
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
  1129
of most elementary terms.  Former Maclauren.DERIV_tac and
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
  1130
Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros).
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
  1131
INCOMPATIBILITY.
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1132
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1133
* Code generator attributes follow the usual underscore convention:
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1134
    code_unfold     replaces    code unfold
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1135
    code_post       replaces    code post
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1136
    etc.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1137
  INCOMPATIBILITY.
31900
7c35d9ad0349 misc tuning;
wenzelm
parents: 31884
diff changeset
  1138
33471
5aef13872723 renamed method induct_scheme to induction_schema
krauss
parents: 33470
diff changeset
  1139
* Renamed methods:
5aef13872723 renamed method induct_scheme to induction_schema
krauss
parents: 33470
diff changeset
  1140
    sizechange -> size_change
5aef13872723 renamed method induct_scheme to induction_schema
krauss
parents: 33470
diff changeset
  1141
    induct_scheme -> induction_schema
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1142
  INCOMPATIBILITY.
33673
nipkow
parents: 33649
diff changeset
  1143
33843
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1144
* Discontinued abbreviation "arbitrary" of constant "undefined".
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1145
INCOMPATIBILITY, use "undefined" directly.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1146
33860
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1147
* Renamed theorems:
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1148
    Suc_eq_add_numeral_1 -> Suc_eq_plus1
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1149
    Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1150
    Suc_plus1 -> Suc_eq_plus1
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1151
    *anti_sym -> *antisym*
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1152
    vector_less_eq_def -> vector_le_def
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1153
  INCOMPATIBILITY.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1154
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1155
* Added theorem List.map_map as [simp].  Removed List.map_compose.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1156
INCOMPATIBILITY.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1157
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1158
* Removed predicate "M hassize n" (<--> card M = n & finite M).
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1159
INCOMPATIBILITY.
dcd9affbd106 tuned NEWS
haftmann
parents: 33849
diff changeset
  1160
31812
73dc3a98669c NEWS updated
hoelzl
parents: 31810
diff changeset
  1161
33825
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1162
*** HOLCF ***
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1163
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1164
* Theory Representable defines a class "rep" of domains that are
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1165
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
  1166
Instances are provided for all type constructors defined in HOLCF.
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1167
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1168
* The 'new_domain' command is a purely definitional version of the
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1169
domain package, for representable domains.  Syntax is identical to the
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1170
old domain package.  The 'new_domain' package also supports indirect
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1171
recursion using previously-defined type constructors.  See
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1172
src/HOLCF/ex/New_Domain.thy for examples.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1173
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1174
* 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
  1175
on the left-hand side of an equation, and then performs
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1176
simplification.  Rewriting is done using rules declared with the
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1177
"fixrec_simp" attribute.  The "fixrec_simp" method is intended as a
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1178
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
  1179
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1180
* The pattern-match compiler in 'fixrec' can now handle constructors
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1181
with HOL function types.  Pattern-match combinators for the Pair
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1182
constructor are pre-configured.
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1183
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1184
* The 'fixrec' package now produces better fixed-point induction rules
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1185
for mutually-recursive definitions:  Induction rules have conclusions
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1186
of the form "P foo bar" instead of "P <foo, bar>".
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1187
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1188
* The constant "sq_le" (with infix syntax "<<" or "\<sqsubseteq>") has
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1189
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
  1190
theorem names.  (Legacy theorem names using "less" are still supported
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1191
as well.)
33825
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1192
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1193
* The 'fixrec' package now supports "bottom patterns".  Bottom
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1194
patterns can be used to generate strictness rules, or to make
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1195
functions more strict (much like the bang-patterns supported by the
33873
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
  1196
Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for
e9120a7b2779 more tuning for release;
wenzelm
parents: 33860
diff changeset
  1197
examples.
33825
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1198
5dac897d91ce NEWS: HOLCF changes since the last release
huffman
parents: 33818
diff changeset
  1199
31304
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31001
diff changeset
  1200
*** ML ***
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31001
diff changeset
  1201
33843
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1202
* Support for Poly/ML 5.3.0, with improved reporting of compiler
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1203
errors and run-time exceptions, including detailed source positions.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1204
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1205
* Structure Name_Space (formerly NameSpace) now manages uniquely
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1206
identified entries, with some additional information such as source
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1207
position, logical grouping etc.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1208
33524
a08e6c1cbc04 updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents: 33472
diff changeset
  1209
* 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
  1210
modernized functors Theory_Data, Proof_Data, Generic_Data.  Data needs
a08e6c1cbc04 updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents: 33472
diff changeset
  1211
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
  1212
copy operation) is still available for some time.
a08e6c1cbc04 updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents: 33472
diff changeset
  1213
32742
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
  1214
* Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
  1215
provides a high-level programming interface to synchronized state
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
  1216
variables with atomic update.  This works via pure function
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
  1217
application within a critical section -- its runtime should be as
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
  1218
short as possible; beware of deadlocks if critical code is nested,
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
  1219
either directly or indirectly via other synchronized variables!
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
  1220
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
  1221
* Structure Unsynchronized (cf. src/Pure/ML-Systems/unsynchronized.ML)
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
  1222
wraps raw ML references, explicitly indicating their non-thread-safe
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
  1223
behaviour.  The Isar toplevel keeps this structure open, to
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
  1224
accommodate Proof General as well as quick and dirty interactive
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
  1225
experiments with references.
58e5f4ae52a6 Synchronized and Unsynchronized;
wenzelm
parents: 32706
diff changeset
  1226
32365
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32326
diff changeset
  1227
* PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32326
diff changeset
  1228
parallel tactical reasoning.
9b74d0339c44 added PARALLEL_CHOICE, PARALLEL_GOALS;
wenzelm
parents: 32326
diff changeset
  1229
32427
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
  1230
* Tacticals Subgoal.FOCUS, Subgoal.FOCUS_PREMS, Subgoal.FOCUS_PARAMS
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
  1231
are similar to SUBPROOF, but are slightly more flexible: only the
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
  1232
specified parts of the subgoal are imported into the context, and the
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
  1233
body tactic may introduce new subgoals and schematic variables.
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
  1234
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
  1235
* Old tactical METAHYPS, which does not observe the proof context, has
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
  1236
been renamed to Old_Goals.METAHYPS and awaits deletion.  Use SUBPROOF
0a94e1f264ce misc updates and tuning;
wenzelm
parents: 32388
diff changeset
  1237
or Subgoal.FOCUS etc.
32216
2f3d65d15149 tacticals FOCUS and FOCUS_PARAMS;
wenzelm
parents: 32151
diff changeset
  1238
31971
8c1b845ed105 renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents: 31901
diff changeset
  1239
* 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
  1240
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
  1241
separately.)  Minor INCOMPATIBILITY.
8c1b845ed105 renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents: 31901
diff changeset
  1242
31901
e280491f36b8 renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 31900
diff changeset
  1243
* Renamed NamedThmsFun to Named_Thms.  INCOMPATIBILITY.
e280491f36b8 renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 31900
diff changeset
  1244
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1245
* Renamed several structures FooBar to Foo_Bar.  Occasional,
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1246
INCOMPATIBILITY.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1247
33843
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1248
* Operations of structure Skip_Proof no longer require quick_and_dirty
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1249
mode, which avoids critical setmp.
23d09560d56d more NEWS, more tuning for release;
wenzelm
parents: 33842
diff changeset
  1250
31306
a74ee84288a0 eliminated old Attrib.add_attributes (and Attrib.syntax);
wenzelm
parents: 31304
diff changeset
  1251
* Eliminated old Attrib.add_attributes, Method.add_methods and related
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1252
combinators for "args".  INCOMPATIBILITY, need to use simplified
31306
a74ee84288a0 eliminated old Attrib.add_attributes (and Attrib.syntax);
wenzelm
parents: 31304
diff changeset
  1253
Attrib/Method.setup introduced in Isabelle2009.
31304
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31001
diff changeset
  1254
32151
2f65c45c2e7e Proper context for simpset_of, claset_of, clasimpset_of.
wenzelm
parents: 32136
diff changeset
  1255
* 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
  1256
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
  1257
last resort.  INCOMPATIBILITY.
2f65c45c2e7e Proper context for simpset_of, claset_of, clasimpset_of.
wenzelm
parents: 32136
diff changeset
  1258
32092
6a5995438266 Display.pretty_thm now requires a proper context;
wenzelm
parents: 32079
diff changeset
  1259
* Display.pretty_thm now requires a proper context (cf. former
6a5995438266 Display.pretty_thm now requires a proper context;
wenzelm
parents: 32079
diff changeset
  1260
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
  1261
or even Display.pretty_thm_without_context as last resort.
6a5995438266 Display.pretty_thm now requires a proper context;
wenzelm
parents: 32079
diff changeset
  1262
INCOMPATIBILITY.
6a5995438266 Display.pretty_thm now requires a proper context;
wenzelm
parents: 32079
diff changeset
  1263
32433
11661f4327bb discontinued Display.pretty_ctyp/cterm etc.;
wenzelm
parents: 32427
diff changeset
  1264
* Discontinued Display.pretty_ctyp/cterm etc.  INCOMPATIBILITY, use
11661f4327bb discontinued Display.pretty_ctyp/cterm etc.;
wenzelm
parents: 32427
diff changeset
  1265
Syntax.pretty_typ/term directly, preferably with proper context
11661f4327bb discontinued Display.pretty_ctyp/cterm etc.;
wenzelm
parents: 32427
diff changeset
  1266
instead of global theory.
11661f4327bb discontinued Display.pretty_ctyp/cterm etc.;
wenzelm
parents: 32427
diff changeset
  1267
31304
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31001
diff changeset
  1268
31308
3fd52453ae81 discontinued support for Poly/ML 4.x versions;
wenzelm
parents: 31306
diff changeset
  1269
*** System ***
3fd52453ae81 discontinued support for Poly/ML 4.x versions;
wenzelm
parents: 31306
diff changeset
  1270
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1271
* 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
  1272
(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
  1273
usedir option -q.
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1274
32326
9d70ecf11b7a etc/components;
wenzelm
parents: 32270
diff changeset
  1275
* Support for additional "Isabelle components" via etc/components, see
9d70ecf11b7a etc/components;
wenzelm
parents: 32270
diff changeset
  1276
also the system manual.
9d70ecf11b7a etc/components;
wenzelm
parents: 32270
diff changeset
  1277
9d70ecf11b7a etc/components;
wenzelm
parents: 32270
diff changeset
  1278
* The isabelle makeall tool now operates on all components with
9d70ecf11b7a etc/components;
wenzelm
parents: 32270
diff changeset
  1279
IsaMakefile, not just hardwired "logics".
9d70ecf11b7a etc/components;
wenzelm
parents: 32270
diff changeset
  1280
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1281
* Removed "compress" option from isabelle-process and isabelle usedir;
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1282
this is always enabled.
33818
aa00c583f594 added NEWS item for wwwfind
kleing
parents: 33759
diff changeset
  1283
31308
3fd52453ae81 discontinued support for Poly/ML 4.x versions;
wenzelm
parents: 31306
diff changeset
  1284
* Discontinued support for Poly/ML 4.x versions.
3fd52453ae81 discontinued support for Poly/ML 4.x versions;
wenzelm
parents: 31306
diff changeset
  1285
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1286
* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 33827
diff changeset
  1287
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
  1288
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
  1289
31308
3fd52453ae81 discontinued support for Poly/ML 4.x versions;
wenzelm
parents: 31306
diff changeset
  1290
31304
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31001
diff changeset
  1291
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1292
New in Isabelle2009 (April 2009)
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1293
--------------------------------
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27067
diff changeset
  1294
27599
ca23ef50c178 added command 'linear_undo';
wenzelm
parents: 27556
diff changeset
  1295
*** General ***
ca23ef50c178 added command 'linear_undo';
wenzelm
parents: 27556
diff changeset
  1296
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
  1297
* 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
  1298
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
  1299
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
  1300
  - 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
  1301
    "isatool."
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
  1302
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
  1303
  - 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
  1304
    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
  1305
28915
0642cbb60c98 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents: 28914
diff changeset
  1306
  - 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
  1307
    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
  1308
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
  1309
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
  1310
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
  1311
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
  1312
28915
0642cbb60c98 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents: 28914
diff changeset
  1313
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
  1314
the interface was uninstalled or changed otherwise.  Individual
0642cbb60c98 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents: 28914
diff changeset
  1315
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
  1316
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
  1317
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
  1318
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28475
diff changeset
  1319
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
  1320
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
  1321
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
  1322
28914
f993cbffc42a default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents: 28856
diff changeset
  1323
* 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
  1324
old ~/isabelle, which was slightly non-standard and apt to cause
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1325
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
  1326
f993cbffc42a default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents: 28856
diff changeset
  1327
INCOMPATIBILITY, need to move existing ~/isabelle/etc,
f993cbffc42a default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents: 28856
diff changeset
  1328
~/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
  1329
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
  1330
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
  1331
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
  1332
29161
9903e84a9c9c * Proofs of are run in parallel on multi-core systems;
wenzelm
parents: 29145
diff changeset
  1333
* Proofs of fully specified statements are run in parallel on
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1334
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
  1335
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
  1336
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
  1337
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1338
* The main reference manuals ("isar-ref", "implementation", and
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1339
"system") have been updated and extended.  Formally checked references
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1340
as hyperlinks are now available uniformly.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1341
30163
faf95eb3f375 * New prover for coherent logic (see src/Tools/coherent.ML).
wenzelm
parents: 30106
diff changeset
  1342
27599
ca23ef50c178 added command 'linear_undo';
wenzelm
parents: 27556
diff changeset
  1343
*** Pure ***
ca23ef50c178 added command 'linear_undo';
wenzelm
parents: 27556
diff changeset
  1344
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1345
* Complete re-implementation of locales.  INCOMPATIBILITY in several
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1346
respects.  The most important changes are listed below.  See the
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1347
Tutorial on Locales ("locales" manual) for details.
29253
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1348
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1349
- In locale expressions, instantiation replaces renaming.  Parameters
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1350
must be declared in a for clause.  To aid compatibility with previous
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1351
parameter inheritance, in locale declarations, parameters that are not
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1352
'touched' (instantiation position "_" or omitted) are implicitly added
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1353
with their syntax at the beginning of the for clause.
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1354
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1355
- Syntax from abbreviations and definitions in locales is available in
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1356
locale expressions and context elements.  The latter is particularly
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1357
useful in locale declarations.
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1358
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1359
- More flexible mechanisms to qualify names generated by locale
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1360
expressions.  Qualifiers (prefixes) may be specified in locale
30728
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
  1361
expressions, and can be marked as mandatory (syntax: "name!:") or
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
  1362
optional (syntax "name?:").  The default depends for plain "name:"
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
  1363
depends on the situation where a locale expression is used: in
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
  1364
commands 'locale' and 'sublocale' prefixes are optional, in
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1365
'interpretation' and 'interpret' prefixes are mandatory.  The old
30728
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
  1366
implicit qualifiers derived from the parameter names of a locale are
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
  1367
no longer generated.
30106
351fc2f8493d tuned NEWS;
wenzelm
parents: 30085
diff changeset
  1368
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1369
- Command "sublocale l < e" replaces "interpretation l < e".  The
30106
351fc2f8493d tuned NEWS;
wenzelm
parents: 30085
diff changeset
  1370
instantiation clause in "interpretation" and "interpret" (square
351fc2f8493d tuned NEWS;
wenzelm
parents: 30085
diff changeset
  1371
brackets) is no longer available.  Use locale expressions.
29253
3c6cd80a4854 New locales.
ballarin
parents: 29197
diff changeset
  1372
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1373
- When converting proof scripts, mandatory qualifiers in
30728
f0aeca99b5d9 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30706
diff changeset
  1374
'interpretation' and 'interpret' should be retained by default, even
30845
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1375
if this is an INCOMPATIBILITY compared to former behavior.  In the
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1376
worst case, use the "name?:" form for non-mandatory ones.  Qualifiers
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1377
in locale expressions range over a single locale instance only.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1378
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1379
- Dropped locale element "includes".  This is a major INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1380
In existing theorem specifications replace the includes element by the
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1381
respective context elements of the included locale, omitting those
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1382
that are already present in the theorem specification.  Multiple
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1383
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
  1384
involving the locale predicate.  In the proof body, declarations (most
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1385
notably theorems) may be regained by interpreting the respective
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1386
locales in the proof context as required (command "interpret").
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1387
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1388
If using "includes" in replacement of a target solely because the
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1389
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
  1390
consider declaring a new locale with additional type constraints on
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1391
the parameters (context element "constrains").
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1392
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1393
- Discontinued "locale (open)".  INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1394
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1395
- Locale interpretation commands no longer attempt to simplify goal.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1396
INCOMPATIBILITY: in rare situations the generated goal differs.  Use
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1397
methods intro_locales and unfold_locales to clarify.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1398
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1399
- Locale interpretation commands no longer accept interpretation
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1400
attributes.  INCOMPATIBILITY.
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1401
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1402
* 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
  1403
list any longer, but is inferred from the specification.  Particularly
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1404
in HOL, write
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1405
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1406
    class foo = ...
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1407
9a887484de53 misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents: 30741
diff changeset
  1408
instead of
9a887484de53 misc cleanup a