200 |
200 |
201 * New package for quotient types. Commands 'quotient_type' and |
201 * New package for quotient types. Commands 'quotient_type' and |
202 'quotient_definition' may be used for defining types and constants by |
202 'quotient_definition' may be used for defining types and constants by |
203 quotient constructions. An example is the type of integers created by |
203 quotient constructions. An example is the type of integers created by |
204 quotienting pairs of natural numbers: |
204 quotienting pairs of natural numbers: |
205 |
205 |
206 fun |
206 fun |
207 intrel :: "(nat * nat) => (nat * nat) => bool" |
207 intrel :: "(nat * nat) => (nat * nat) => bool" |
208 where |
208 where |
209 "intrel (x, y) (u, v) = (x + v = u + y)" |
209 "intrel (x, y) (u, v) = (x + v = u + y)" |
210 |
210 |
211 quotient_type int = "nat × nat" / intrel |
211 quotient_type int = "nat * nat" / intrel |
212 by (auto simp add: equivp_def expand_fun_eq) |
212 by (auto simp add: equivp_def expand_fun_eq) |
213 |
213 |
214 quotient_definition |
214 quotient_definition |
215 "0::int" is "(0::nat, 0::nat)" |
215 "0::int" is "(0::nat, 0::nat)" |
216 |
216 |
217 The method "lifting" can be used to lift of theorems from the |
217 The method "lifting" can be used to lift of theorems from the |
218 underlying "raw" type to the quotient type. The example |
218 underlying "raw" type to the quotient type. The example |
290 AFP/thys/Coinductive. |
290 AFP/thys/Coinductive. |
291 |
291 |
292 * Theory PReal, including the type "preal" and related operations, has |
292 * Theory PReal, including the type "preal" and related operations, has |
293 been removed. INCOMPATIBILITY. |
293 been removed. INCOMPATIBILITY. |
294 |
294 |
|
295 * Real: new development using Cauchy Sequences. |
|
296 |
295 * Split off theory "Big_Operators" containing setsum, setprod, |
297 * Split off theory "Big_Operators" containing setsum, setprod, |
296 Inf_fin, Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY. |
298 Inf_fin, Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY. |
297 |
299 |
298 * Theory "Rational" renamed to "Rat", for consistency with "Nat", |
300 * Theory "Rational" renamed to "Rat", for consistency with "Nat", |
299 "Int" etc. INCOMPATIBILITY. |
301 "Int" etc. INCOMPATIBILITY. |
509 "SAT4J_Light". INCOMPATIBILITY. |
511 "SAT4J_Light". INCOMPATIBILITY. |
510 - Removed "skolemize", "uncurry", "sym_break", "flatten_prop", |
512 - Removed "skolemize", "uncurry", "sym_break", "flatten_prop", |
511 "sharing_depth", and "show_skolems" options. INCOMPATIBILITY. |
513 "sharing_depth", and "show_skolems" options. INCOMPATIBILITY. |
512 - Removed "nitpick_intro" attribute. INCOMPATIBILITY. |
514 - Removed "nitpick_intro" attribute. INCOMPATIBILITY. |
513 |
515 |
|
516 * Method "induct" now takes instantiations of the form t, where t is not |
|
517 a variable, as a shorthand for "x == t", where x is a fresh variable. |
|
518 If this is not intended, t has to be enclosed in parentheses. |
|
519 By default, the equalities generated by definitional instantiations |
|
520 are pre-simplified, which may cause parameters of inductive cases |
|
521 to disappear, or may even delete some of the inductive cases. |
|
522 Use "induct (no_simp)" instead of "induct" to restore the old |
|
523 behaviour. The (no_simp) option is also understood by the "cases" |
|
524 and "nominal_induct" methods, which now perform pre-simplification, too. |
|
525 INCOMPATIBILITY. |
|
526 |
514 |
527 |
515 *** HOLCF *** |
528 *** HOLCF *** |
516 |
529 |
517 * Variable names in lemmas generated by the domain package have |
530 * Variable names in lemmas generated by the domain package have |
518 changed; the naming scheme is now consistent with the HOL datatype |
531 changed; the naming scheme is now consistent with the HOL datatype |
680 |
693 |
681 * The preliminary Isabelle/jEdit application demonstrates the emerging |
694 * The preliminary Isabelle/jEdit application demonstrates the emerging |
682 Isabelle/Scala layer for advanced prover interaction and integration. |
695 Isabelle/Scala layer for advanced prover interaction and integration. |
683 See src/Tools/jEdit or "isabelle jedit" provided by the properly built |
696 See src/Tools/jEdit or "isabelle jedit" provided by the properly built |
684 component. |
697 component. |
|
698 |
|
699 * "IsabelleText" is a Unicode font derived from Bitstream Vera Mono |
|
700 and Bluesky TeX fonts. It provides the usual Isabelle symbols, |
|
701 similar to the default assignment of the document preparation system |
|
702 (cf. isabellesym.sty). The Isabelle/Scala class Isabelle_System |
|
703 provides some operations for direct access to the font without asking |
|
704 the user for manual installation. |
685 |
705 |
686 |
706 |
687 |
707 |
688 New in Isabelle2009-1 (December 2009) |
708 New in Isabelle2009-1 (December 2009) |
689 ------------------------------------- |
709 ------------------------------------- |
3407 reals into other types. The overloaded constant Reals :: 'a set is now |
3427 reals into other types. The overloaded constant Reals :: 'a set is now |
3408 defined as range of_real; potential INCOMPATIBILITY. |
3428 defined as range of_real; potential INCOMPATIBILITY. |
3409 |
3429 |
3410 * Real: proper support for ML code generation, including 'quickcheck'. |
3430 * Real: proper support for ML code generation, including 'quickcheck'. |
3411 Reals are implemented as arbitrary precision rationals. |
3431 Reals are implemented as arbitrary precision rationals. |
3412 |
|
3413 * Real: new development using Cauchy Sequences. |
|
3414 |
3432 |
3415 * Hyperreal: Several constants that previously worked only for the |
3433 * Hyperreal: Several constants that previously worked only for the |
3416 reals have been generalized, so they now work over arbitrary vector |
3434 reals have been generalized, so they now work over arbitrary vector |
3417 spaces. Type annotations may need to be added in some cases; potential |
3435 spaces. Type annotations may need to be added in some cases; potential |
3418 INCOMPATIBILITY. |
3436 INCOMPATIBILITY. |