1.1 --- a/NEWS Thu May 27 16:29:33 2010 +0200
1.2 +++ b/NEWS Thu May 27 16:30:26 2010 +0200
1.3 @@ -1,8 +1,8 @@
1.4 Isabelle NEWS -- history user-relevant changes
1.5 ==============================================
1.6
1.7 -New in this Isabelle version
1.8 -----------------------------
1.9 +New in Isabelle2009-2 (June 2010)
1.10 +---------------------------------
1.11
1.12 *** General ***
1.13
1.14 @@ -146,9 +146,9 @@
1.15 * List membership infix mem operation is only an input abbreviation.
1.16 INCOMPATIBILITY.
1.17
1.18 -* Theory Library/Word.thy has been removed. Use library Word/Word.thy for
1.19 -future developements; former Library/Word.thy is still present in the AFP
1.20 -entry RSAPPS.
1.21 +* Theory Library/Word.thy has been removed. Use library Word/Word.thy
1.22 +for future developements; former Library/Word.thy is still present in
1.23 +the AFP entry RSAPPS.
1.24
1.25 * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no
1.26 longer shadowed. INCOMPATIBILITY.
1.27 @@ -197,7 +197,7 @@
1.28 ceiling_subtract_number_of ~> ceiling_diff_number_of
1.29 ceiling_subtract_one ~> ceiling_diff_one
1.30
1.31 -* Theory 'Finite_Set': various folding_XXX locales facilitate the
1.32 +* Theory "Finite_Set": various folding_XXX locales facilitate the
1.33 application of the various fold combinators on finite sets.
1.34
1.35 * Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"
1.36 @@ -222,6 +222,9 @@
1.37 * Theory "Rational" renamed to "Rat", for consistency with "Nat",
1.38 "Int" etc. INCOMPATIBILITY.
1.39
1.40 +* Constant Rat.normalize needs to be qualified. Minor
1.41 +INCOMPATIBILITY.
1.42 +
1.43 * New set of rules "ac_simps" provides combined assoc / commute
1.44 rewrites for all interpretations of the appropriate generic locales.
1.45
1.46 @@ -493,6 +496,50 @@
1.47
1.48 *** ML ***
1.49
1.50 +* Renamed some important ML structures, while keeping the old names
1.51 +for some time as aliases within the structure Legacy:
1.52 +
1.53 + OuterKeyword ~> Keyword
1.54 + OuterLex ~> Token
1.55 + OuterParse ~> Parse
1.56 + OuterSyntax ~> Outer_Syntax
1.57 + SpecParse ~> Parse_Spec
1.58 +
1.59 +Note that "open Legacy" simplifies porting of sources, but forgetting
1.60 +to remove it again will complicate porting again in the future.
1.61 +
1.62 +* Most operations that refer to a global context are named
1.63 +accordingly, e.g. Simplifier.global_context or
1.64 +ProofContext.init_global. There are some situations where a global
1.65 +context actually works, but under normal circumstances one needs to
1.66 +pass the proper local context through the code!
1.67 +
1.68 +* Discontinued old TheoryDataFun with its copy/init operation -- data
1.69 +needs to be pure. Functor Theory_Data_PP retains the traditional
1.70 +Pretty.pp argument to merge, which is absent in the standard
1.71 +Theory_Data version.
1.72 +
1.73 +* Antiquotations for basic formal entities:
1.74 +
1.75 + @{class NAME} -- type class
1.76 + @{class_syntax NAME} -- syntax representation of the above
1.77 +
1.78 + @{type_name NAME} -- logical type
1.79 + @{type_abbrev NAME} -- type abbreviation
1.80 + @{nonterminal NAME} -- type of concrete syntactic category
1.81 + @{type_syntax NAME} -- syntax representation of any of the above
1.82 +
1.83 + @{const_name NAME} -- logical constant (INCOMPATIBILITY)
1.84 + @{const_abbrev NAME} -- abbreviated constant
1.85 + @{const_syntax NAME} -- syntax representation of any of the above
1.86 +
1.87 +* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
1.88 +syntax constant (cf. 'syntax' command).
1.89 +
1.90 +* Antiquotation @{make_string} inlines a function to print arbitrary
1.91 +values similar to the ML toplevel. The result is compiler dependent
1.92 +and may fall back on "?" in certain situations.
1.93 +
1.94 * Sorts.certify_sort and derived "cert" operations for types and terms
1.95 no longer minimize sorts. Thus certification at the boundary of the
1.96 inference kernel becomes invariant under addition of class relations,
1.97 @@ -501,42 +548,13 @@
1.98 system. Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
1.99 explicitly in rare situations.
1.100
1.101 -* Antiquotations for basic formal entities:
1.102 -
1.103 - @{class NAME} -- type class
1.104 - @{class_syntax NAME} -- syntax representation of the above
1.105 -
1.106 - @{type_name NAME} -- logical type
1.107 - @{type_abbrev NAME} -- type abbreviation
1.108 - @{nonterminal NAME} -- type of concrete syntactic category
1.109 - @{type_syntax NAME} -- syntax representation of any of the above
1.110 -
1.111 - @{const_name NAME} -- logical constant (INCOMPATIBILITY)
1.112 - @{const_abbrev NAME} -- abbreviated constant
1.113 - @{const_syntax NAME} -- syntax representation of any of the above
1.114 -
1.115 -* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
1.116 -syntax constant (cf. 'syntax' command).
1.117 -
1.118 -* Antiquotation @{make_string} inlines a function to print arbitrary
1.119 -values similar to the ML toplevel. The result is compiler dependent
1.120 -and may fall back on "?" in certain situations.
1.121 -
1.122 * Renamed old-style Drule.standard to Drule.export_without_context, to
1.123 emphasize that this is in no way a standard operation.
1.124 INCOMPATIBILITY.
1.125
1.126 -* Curried take and drop in library.ML; negative length is interpreted
1.127 -as infinity (as in chop). INCOMPATIBILITY.
1.128 -
1.129 * Subgoal.FOCUS (and variants): resulting goal state is normalized as
1.130 usual for resolution. Rare INCOMPATIBILITY.
1.131
1.132 -* Discontinued old TheoryDataFun with its copy/init operation -- data
1.133 -needs to be pure. Functor Theory_Data_PP retains the traditional
1.134 -Pretty.pp argument to merge, which is absent in the standard
1.135 -Theory_Data version.
1.136 -
1.137 * Renamed varify/unvarify operations to varify_global/unvarify_global
1.138 to emphasize that these only work in a global situation (which is
1.139 quite rare).
1.140 @@ -544,23 +562,11 @@
1.141 * Configuration options now admit dynamic default values, depending on
1.142 the context or even global references.
1.143
1.144 -* Most operations that refer to a global context are named
1.145 -accordingly, e.g. Simplifier.global_context or
1.146 -ProofContext.init_global. There are some situations where a global
1.147 -context actually works, but under normal circumstances one needs to
1.148 -pass the proper local context through the code!
1.149 -
1.150 -* Renamed some important ML structures, while keeping the old names
1.151 -for some time as aliases within the structure Legacy:
1.152 -
1.153 - OuterKeyword ~> Keyword
1.154 - OuterLex ~> Token
1.155 - OuterParse ~> Parse
1.156 - OuterSyntax ~> Outer_Syntax
1.157 - SpecParse ~> Parse_Spec
1.158 -
1.159 -Note that "open Legacy" simplifies porting of sources, but forgetting
1.160 -to remove it again will complicate porting again in the future.
1.161 +* SHA1.digest digests strings according to SHA-1 (see RFC 3174). It
1.162 +uses an efficient external library if available (for Poly/ML).
1.163 +
1.164 +* Curried take and drop in library.ML; negative length is interpreted
1.165 +as infinity (as in chop). Subtle INCOMPATIBILITY.
1.166
1.167
1.168 *** System ***