# HG changeset patch # User wenzelm # Date 1404478325 -7200 # Node ID 5cf245c62c4cabdd0b839cff927b92be341c7778 # Parent 3e04e25a751e0db87db1fd7e5bc7d99a378a0ab0 misc tuning for release; diff -r 3e04e25a751e -r 5cf245c62c4c ANNOUNCE --- a/ANNOUNCE Fri Jul 04 11:39:34 2014 +0200 +++ b/ANNOUNCE Fri Jul 04 14:52:05 2014 +0200 @@ -9,7 +9,8 @@ * Improved Isabelle/jEdit Prover IDE: navigation, completion, spell-checking, Query panel, Simplifier Trace panel. -* Support for auxiliary files within the Prover IDE. +* Support for auxiliary files within the Prover IDE, notably + Isabelle/ML. * Support for official Standard ML within the Prover IDE, independently of Isabelle theory and proof development. @@ -19,19 +20,19 @@ * HOL tool enhancements: Nitpick, Sledgehammer. -* HOL: numerous library enhancements: Main, HOL-Multivariate_Analysis, - HOL-Probability. - * HOL: internal SAT solver "cdclite" with models and proof traces. * HOL: updated SMT module, with support for SMT-LIB 2 and recent versions of Z3, as well as CVC3, CVC4. +* HOL: numerous library enhancements: Main, HOL-Multivariate_Analysis, + HOL-Probability. + +* System integration: improved support of LateX on Windows platform. + * Updated and extended manuals: codegen, datatypes, implementation, isar-ref, jedit, system. -* System integration: improved support of LateX on Windows platform. - You may get Isabelle2013-2 from the following mirror sites: diff -r 3e04e25a751e -r 5cf245c62c4c NEWS --- a/NEWS Fri Jul 04 11:39:34 2014 +0200 +++ b/NEWS Fri Jul 04 14:52:05 2014 +0200 @@ -15,6 +15,16 @@ separate environments. See also ~~/src/Tools/SML/Examples.thy for some examples. +* Standard tactics and proof methods such as "clarsimp", "auto" and +"safe" now preserve equality hypotheses "x = expr" where x is a free +variable. Locale assumptions and chained facts containing "x" +continue to be useful. The new method "hypsubst_thin" and the +configuration option "hypsubst_thin" (within the attribute name space) +restore the previous behavior. INCOMPATIBILITY, especially where +induction is done after these methods or when the names of free and +bound variables clash. As first approximation, old proofs may be +repaired by "using [[hypsubst_thin = true]]" in the critical spot. + * More static checking of proof methods, which allows the system to form a closure over the concrete syntax. Method arguments should be processed in the original proof context as far as possible, before @@ -51,18 +61,6 @@ * Updated and extended manuals: codegen, datatypes, implementation, isar-ref, jedit, system. -* Standard tactics and proof methods such as "clarsimp", "auto" and -"safe" now preserve equality hypotheses "x = expr" where x is a free -variable. Locale assumptions and chained facts containing "x" -continue to be useful. The new method "hypsubst_thin" and the -configuration option "hypsubst_thin" (within the attribute name space) -restore the previous behavior. - -INCOMPATIBILITY, especially where induction is done after these -methods or when the names of free and bound variables clash. As first -approximation, old proofs may be repaired by "using [[hypsubst_thin = -true]]" in the critical spot. - *** Prover IDE -- Isabelle/Scala/jEdit *** @@ -122,9 +120,18 @@ within the context. - *** Pure *** +* Low-level type-class commands 'classes', 'classrel', 'arities' have +been discontinued to avoid the danger of non-trivial axiomatization +that is not immediately visible. INCOMPATIBILITY, use regular +'instance' command with proof. The required OFCLASS(...) theorem +might be postulated via 'axiomatization' beforehand, or the proof +finished trivially if the underlying class definition is made vacuous +(without any assumptions). See also Isabelle/ML operations +Axclass.class_axiomatization, Axclass.classrel_axiomatization, +Axclass.arity_axiomatization. + * Basic constants of Pure use more conventional names and are always qualified. Rare INCOMPATIBILITY, but with potentially serious consequences, notably for tools in Isabelle/ML. The following @@ -153,16 +160,6 @@ Later the application is moved to the current Isabelle version, and the auxiliary aliases are deleted. -* Low-level type-class commands 'classes', 'classrel', 'arities' have -been discontinued to avoid the danger of non-trivial axiomatization -that is not immediately visible. INCOMPATIBILITY, use regular -'instance' command with proof. The required OFCLASS(...) theorem -might be postulated via 'axiomatization' beforehand, or the proof -finished trivially if the underlying class definition is made vacuous -(without any assumptions). See also Isabelle/ML operations -Axclass.class_axiomatization, Axclass.classrel_axiomatization, -Axclass.arity_axiomatization. - * Attributes "where" and "of" allow an optional context of local variables ('for' declaration): these variables become schematic in the instantiated theorem. @@ -186,22 +183,45 @@ (only makes sense in practice, if outer syntax is delimited differently, e.g. via cartouches). +* Command 'print_term_bindings' supersedes 'print_binds' for clarity, +but the latter is retained some time as Proof General legacy. + * Code generator preprocessor: explicit control of simp tracing on a per-constant basis. See attribute "code_preproc". -* Command 'print_term_bindings' supersedes 'print_binds' for clarity, -but the latter is retained some time as Proof General legacy. - *** HOL *** -* Qualified String.implode and String.explode. INCOMPATIBILITY. +* Code generator: enforce case of identifiers only for strict target +language requirements. INCOMPATIBILITY. + +* Code generator: explicit proof contexts in many ML interfaces. +INCOMPATIBILITY. + +* Code generator: minimize exported identifiers by default. Minor +INCOMPATIBILITY. + +* Code generation for SML and OCaml: dropped arcane "no_signatures" +option. Minor INCOMPATIBILITY. + +* "declare [[code abort: ...]]" replaces "code_abort ...". +INCOMPATIBILITY. + +* "declare [[code drop: ...]]" drops all code equations associated +with the given constants. + +* Code generations are provided for make, fields, extend and truncate +operations on records. * Command and antiquotation "value" are now hardcoded against nbe and ML. Minor INCOMPATIBILITY. -* Separate command "approximate" for approximative computation in -src/HOL/Decision_Procs/Approximation. Minor INCOMPATIBILITY. +* Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY. + +* The symbol "\" may be used within char or string literals +to represent (Char Nibble0 NibbleA), i.e. ASCII newline. + +* Qualified String.implode and String.explode. INCOMPATIBILITY. * Adjustion of INF and SUP operations: - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM. @@ -217,13 +237,6 @@ INCOMPATIBILITY. -* Revisions to HOL/Number_Theory - - consolidated the proofs of the binomial theorem - - the function fib is again of type nat=>nat and not overloaded - - no more references to Old_Number_Theory in the HOL libraries (except the AFP) - -INCOMPATIBILITY. - * Swapped orientation of facts image_comp and vimage_comp: image_compose ~> image_comp [symmetric] @@ -239,25 +252,6 @@ [[simp_legacy_precond]]. This configuration option will disappear again in the future. INCOMPATIBILITY. -* HOL-Word: - - Abandoned fact collection "word_arith_alts", which is a duplicate - of "word_arith_wis". - - Dropped first (duplicated) element in fact collections - "sint_word_ariths", "word_arith_alts", "uint_word_ariths", - "uint_word_arith_bintrs". - -* Code generator: enforce case of identifiers only for strict target -language requirements. INCOMPATIBILITY. - -* Code generator: explicit proof contexts in many ML interfaces. -INCOMPATIBILITY. - -* Code generator: minimize exported identifiers by default. Minor -INCOMPATIBILITY. - -* Code generation for SML and OCaml: dropped arcane "no_signatures" -option. Minor INCOMPATIBILITY. - * Simproc "finite_Collect" is no longer enabled by default, due to spurious crashes and other surprises. Potential INCOMPATIBILITY. @@ -374,12 +368,8 @@ INCOMPATIBILITY. -* New theory src/HOL/Cardinals/Ordinal_Arithmetic.thy. - -* New theory src/HOL/Library/Tree.thy. - -* Theory reorganization: - Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy +* Theory reorganization: split of Big_Operators.thy into +Groups_Big.thy and Lattices_Big.thy. * Consolidated some facts about big group operators: @@ -486,22 +476,11 @@ * Try0: Added 'algebra' and 'meson' to the set of proof methods. -* Command renaming: enriched_type ~> functor. INCOMPATIBILITY. - -* The symbol "\" may be used within char or string literals -to represent (Char Nibble0 NibbleA), i.e. ASCII newline. - * Activation of Z3 now works via "z3_non_commercial" system option (without requiring restart), instead of former settings variable "Z3_NON_COMMERCIAL". The option can be edited in Isabelle/jEdit menu Plugin Options / Isabelle / General. -* "declare [[code abort: ...]]" replaces "code_abort ...". -INCOMPATIBILITY. - -* "declare [[code drop: ...]]" drops all code equations associated -with the given constants. - * Abolished slightly odd global lattice interpretation for min/max. Fact consolidations: @@ -557,15 +536,9 @@ INCOMPATBILITY. -* HOL-Word: bit representations prefer type bool over type bit. -INCOMPATIBILITY. - * Theorem disambiguation Inf_le_Sup (on finite sets) ~> Inf_fin_le_Sup_fin. INCOMPATIBILITY. -* Code generations are provided for make, fields, extend and truncate -operations on records. - * Qualified constant names Wellfounded.acc, Wellfounded.accp. INCOMPATIBILITY. @@ -633,9 +606,6 @@ * SUP and INF generalized to conditionally_complete_lattice. -* Theory Lubs moved HOL image to HOL-Library. It is replaced by -Conditionally_Complete_Lattices. INCOMPATIBILITY. - * Introduce bdd_above and bdd_below in theory Conditionally_Complete_Lattices, use them instead of explicitly stating boundedness of sets. @@ -764,6 +734,34 @@ - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to "hide_types". +* Theory Lubs moved HOL image to HOL-Library. It is replaced by +Conditionally_Complete_Lattices. INCOMPATIBILITY. + +* HOL-Library: new theory src/HOL/Library/Tree.thy. + +* HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it +is subsumed by session Kleene_Algebra in AFP. + +* HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy. + +* HOL-Word: bit representations prefer type bool over type bit. +INCOMPATIBILITY. + +* HOL-Word: + - Abandoned fact collection "word_arith_alts", which is a duplicate + of "word_arith_wis". + - Dropped first (duplicated) element in fact collections + "sint_word_ariths", "word_arith_alts", "uint_word_ariths", + "uint_word_arith_bintrs". + +* HOL-Number_Theory: + - consolidated the proofs of the binomial theorem + - the function fib is again of type nat => nat and not overloaded + - no more references to Old_Number_Theory in the HOL libraries + (except the AFP) + +INCOMPATIBILITY. + * HOL-Multivariate_Analysis: - Type class ordered_real_vector for ordered vector spaces. - New theory Complex_Basic_Analysis defining complex derivatives, @@ -908,8 +906,9 @@ - Formalized properties about exponentially, Erlang, and normal distributed random variables. -* Removed theory src/HOL/Library/Kleene_Algebra.thy; it is subsumed by -session Kleene_Algebra in AFP. +* HOL-Decision_Procs: Separate command 'approximate' for approximative +computation in src/HOL/Decision_Procs/Approximation. Minor +INCOMPATIBILITY. *** Scala *** @@ -926,6 +925,25 @@ *** ML *** +* Subtle change of semantics of Thm.eq_thm: theory stamps are not +compared (according to Thm.thm_ord), but assumed to be covered by the +current background theory. Thus equivalent data produced in different +branches of the theory graph usually coincides (e.g. relevant for +theory merge). Note that the softer Thm.eq_thm_prop is often more +appropriate than Thm.eq_thm. + +* Proper context for basic Simplifier operations: rewrite_rule, +rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to +pass runtime Proof.context (and ensure that the simplified entity +actually belongs to it). + +* Proper context discipline for read_instantiate and instantiate_tac: +variables that are meant to become schematic need to be given as +fixed, and are generalized by the explicit context of local variables. +This corresponds to Isar attributes "where" and "of" with 'for' +declaration. INCOMPATIBILITY, also due to potential change of indices +of schematic variables. + * Moved ML_Compiler.exn_trace and other operations on exceptions to structure Runtime. Minor INCOMPATIBILITY. @@ -941,30 +959,11 @@ ML is still available as default_print_depth, but rarely used. Minor INCOMPATIBILITY. -* Proper context discipline for read_instantiate and instantiate_tac: -variables that are meant to become schematic need to be given as -fixed, and are generalized by the explicit context of local variables. -This corresponds to Isar attributes "where" and "of" with 'for' -declaration. INCOMPATIBILITY, also due to potential change of indices -of schematic variables. - * Toplevel function "use" refers to raw ML bootstrap environment, without Isar context nor antiquotations. Potential INCOMPATIBILITY. Note that 'ML_file' is the canonical command to load ML files into the formal context. -* Proper context for basic Simplifier operations: rewrite_rule, -rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to -pass runtime Proof.context (and ensure that the simplified entity -actually belongs to it). - -* Subtle change of semantics of Thm.eq_thm: theory stamps are not -compared (according to Thm.thm_ord), but assumed to be covered by the -current background theory. Thus equivalent data produced in different -branches of the theory graph usually coincides (e.g. relevant for -theory merge). Note that the softer Thm.eq_thm_prop is often more -appropriate than Thm.eq_thm. - * Simplified programming interface to define ML antiquotations, see structure ML_Antiquotation. Minor INCOMPATIBILITY. @@ -985,17 +984,17 @@ *** System *** * Proof General with its traditional helper scripts is now an optional -Isabelle component, e.g. ProofGeneral-4.2-2 from the Isabelle -component repository http://isabelle.in.tum.de/components/. See also -the "system" manual for general explanations about add-on components, -notably those that are not bundled with the normal release. +Isabelle component, e.g. see ProofGeneral-4.2-2 from the Isabelle +component repository http://isabelle.in.tum.de/components/. Note that +the "system" manual provides general explanations about add-on +components, especially those that are not bundled with the release. * The raw Isabelle process executable has been renamed from "isabelle-process" to "isabelle_process", which conforms to common shell naming conventions, and allows to define a shell function within the Isabelle environment to avoid dynamic path lookup. Rare -incompatibility for old tools that do not use the $ISABELLE_PROCESS -settings variable yet. +incompatibility for old tools that do not use the ISABELLE_PROCESS +settings variable. * Former "isabelle tty" has been superseded by "isabelle console", with implicit build like "isabelle jedit", and without the mostly @@ -1018,14 +1017,14 @@ repeated invocation in PIDE front-end: re-use single file $ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views. -* Windows: support for regular TeX installation (e.g. MiKTeX) instead -of TeX Live from Cygwin. - * Session ROOT specifications require explicit 'document_files' for robust dependencies on LaTeX sources. Only these explicitly given files are copied to the document output directory, before document processing is started. +* Windows: support for regular TeX installation (e.g. MiKTeX) instead +of TeX Live from Cygwin. + New in Isabelle2013-2 (December 2013)