Isabelle NEWS -- history user-relevant changes ============================================== New in this Isabelle release ---------------------------- *** General *** * Pure: considerably improved version of 'constdefs' command. Now performs automatic type-inference of declared constants; additional support for local structure declarations (cf. locales and HOL records), see also isar-ref manual. Potential INCOMPATIBILITY: need to observe strictly sequential dependencies of definitions within a single 'constdefs' section; moreover, the declared name needs to be an identifier. If all fails, consider to fall back on 'consts' and 'defs' separately. * Pure: improved indexed syntax and implicit structures. First of all, indexed syntax provides a notational device for subscripted application, using the new syntax \<^bsub>term\<^esub> for arbitrary expressions. Secondly, in a local context with structure declarations, number indexes \<^sub>n or the empty index (default number 1) refer to a certain fixed variable implicitly; option show_structs controls printing of implicit structures. Typical applications of these concepts involve record types and locales. * Pure: clear separation of logical types and nonterminals, where the latter may only occur in 'syntax' specifications or type abbreviations. Before that distinction was only partially implemented via type class "logic" vs. "{}". Potential INCOMPATIBILITY in rare cases of improper use of 'types'/'consts' instead of 'nonterminals'/'syntax'. Some very exotic syntax specifications may require further adaption (e.g. Cube/Base.thy). * Pure: removed obsolete type class "logic", use the top sort {} instead. Note that non-logical types should be declared as 'nonterminals' rather than 'types'. INCOMPATIBILITY for new object-logic specifications. * Pure: print_tac now outputs the goal through the trace channel. * Pure: reference Namespace.unique_names included. If true the (shortest) namespace-prefix is printed to disambiguate conflicts (as yet). If false the first entry wins (as during parsing). Default value is true. * Pure: tuned internal renaming of symbolic identifiers -- attach primes instead of base 26 numbers. * Pure/Syntax: inner syntax includes (*(*nested*) comments*). * Pure/Syntax: pretty pinter now supports unbreakable blocks, specified in mixfix annotations as "(00...)". * Pure/Syntax: 'advanced' translation functions (parse_translation etc.) may depend on the signature of the theory context being presently used for parsing/printing, see also isar-ref manual. * Pure/Simplifier: simplification procedures may now take the current simpset into account (cf. Simplifier.simproc(_i) / mk_simproc interface), which is very useful for calling the Simplifier recursively. Minor INCOMPATIBILITY: the 'prems' argument of simprocs is gone -- use prems_of_ss on the simpset instead. Moreover, the low-level mk_simproc no longer applies Logic.varify internally, to allow for use in a context of fixed variables. * Provers: Simplifier and Classical Reasoner now support proof context dependent plug-ins (simprocs, solvers, wrappers etc.). These extra components are stored in the theory and patched into the simpset/claset when used in an Isar proof context. Context dependent components are maintained by the following theory operations: Simplifier.add_context_simprocs Simplifier.del_context_simprocs Simplifier.set_context_subgoaler Simplifier.reset_context_subgoaler Simplifier.add_context_looper Simplifier.del_context_looper Simplifier.add_context_unsafe_solver Simplifier.add_context_safe_solver Classical.add_context_safe_wrapper Classical.del_context_safe_wrapper Classical.add_context_unsafe_wrapper Classical.del_context_unsafe_wrapper IMPORTANT NOTE: proof tools (methods etc.) need to use local_simpset_of and local_claset_of to instead of the primitive Simplifier.get_local_simpset and Classical.get_local_claset, respectively, in order to see the context dependent fields! * Document preparation: antiquotations now provide the option 'locale=NAME' to specify an alternative context used for evaluating and printing the subsequent argument, as in @{thm [locale=LC] fold_commute}, for example. * Document preparation: commands 'display_drafts' and 'print_drafts' perform simple output of raw sources. Only those symbols that do not require additional LaTeX packages (depending on comments in isabellesym.sty) are displayed properly, everything else is left verbatim. We use isatool display and isatool print as front ends; these are subject to the DVI_VIEWER and PRINT_COMMAND settings, respectively. * ML: output via the Isabelle channels of writeln/warning/error etc. is now passed through Output.output, with a hook for arbitrary transformations depending on the print_mode (cf. Output.add_mode -- the first active mode that provides a output function wins). Already formatted output may be embedded into further text via Output.raw; the result of Pretty.string_of/str_of and derived functions (string_of_term/cterm/thm etc.) is already marked raw to accommodate easy composition of diagnostic messages etc. Programmers rarely need to care about Output.output or Output.raw at all, with some notable exceptions: Output.output is required when bypassing the standard channels (writeln etc.), or in token translations to produce properly formatted results; Output.raw is required when capturing already output material that will eventually be presented to the user a second time. For the default print mode, both Output.output and Output.raw have no effect. *** HOL *** * HOL/record: reimplementation of records. Improved scalability for records with many fields, avoiding performance problems for type inference. Records are no longer composed of nested field types, but of nested extension types. Therefore the record type only grows linear in the number of extensions and not in the number of fields. The top-level (users) view on records is preserved. Potential INCOMPATIBILITY only in strange cases, where the theory depends on the old record representation. The type generated for a record is called _ext_type. * HOL/record: Reference record_quick_and_dirty_sensitive can be enabled to skip the proofs triggered by a record definition or a simproc (if quick_and_dirty is enabled). Definitions of large records can take quite long. * HOL/record: "record_upd_simproc" for simplification of multiple record updates enabled by default. Moreover, trivial updates are also removed: r(|x := x r|) = r. INCOMPATIBILITY: old proofs break occasionally, since simplification is more powerful by default. * HOL: symbolic syntax of Hilbert Choice Operator is now as follows: syntax (epsilon) "_Eps" :: "[pttrn, bool] => 'a" ("(3\_./ _)" [0, 10] 10) The symbol \ is displayed as the alternative epsilon of LaTeX and x-symbol; use option '-m epsilon' to get it actually printed. Moreover, the mathematically important symbolic identifier \ becomes available as variable, constant etc. * HOL/SetInterval: The syntax for open intervals has changed: Old New {..n(} -> {.. {n<..} {m..n(} -> {m.. {m<..n} {)m..n(} -> {m<.. {\1<\.\.} \.\.\([^(}]*\)(} -> \.\.<\1} They are not perfect but work quite well. * HOL: There is new syntax for summation over finite sets: '\x | P. e' is the same as 'setsum (%x. e) {x. P}' '\xi), as well as Gothic (\...\\...\), calligraphic (\...\), and Euler (\...\), are now considered normal letters, and can therefore be used anywhere where an ASCII letter (a...zA...Z) has until now. COMPATIBILITY: This obviously changes the parsing of some terms, especially where a symbol has been used as a binder, say '\x. ...', which is now a type error since \x will be parsed as an identifier. Fix it by inserting a space around former symbols. Call 'isatool fixgreek' to try to fix parsing errors in existing theory and ML files. * Pure: Macintosh and Windows line-breaks are now allowed in theory files. * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now allowed in identifiers. Similar to Greek letters \<^isub> is now considered a normal (but invisible) letter. For multiple letter subscripts repeat \<^isub> like this: x\<^isub>1\<^isub>2. * Pure: There are now sub-/superscripts that can span more than one character. Text between \<^bsub> and \<^esub> is set in subscript in ProofGeneral and LaTeX, text between \<^bsup> and \<^esup> in superscript. The new control characters are not identifier parts. * Pure: Control-symbols of the form \<^raw:...> will literally print the content of "..." to the latex file instead of \isacntrl... . The "..." may consist of any printable characters excluding the end bracket >. * Pure: Using new Isar command "finalconsts" (or the ML functions Theory.add_finals or Theory.add_finals_i) it is now possible to declare constants "final", which prevents their being given a definition later. It is useful for constants whose behaviour is fixed axiomatically rather than definitionally, such as the meta-logic connectives. * Pure: 'instance' now handles general arities with general sorts (i.e. intersections of classes), * Presentation: generated HTML now uses a CSS style sheet to make layout (somewhat) independent of content. It is copied from lib/html/isabelle.css. It can be changed to alter the colors/layout of generated pages. *** Isar *** * Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac, cut_tac, subgoal_tac and thin_tac: - Now understand static (Isar) contexts. As a consequence, users of Isar locales are no longer forced to write Isar proof scripts. For details see Isar Reference Manual, paragraph 4.3.2: Further tactic emulations. - INCOMPATIBILITY: names of variables to be instantiated may no longer be enclosed in quotes. Instead, precede variable name with `?'. This is consistent with the instantiation attribute "where". * Attributes "where" and "of": - Now take type variables of instantiated theorem into account when reading the instantiation string. This fixes a bug that caused instantiated theorems to have too special types in some circumstances. - "where" permits explicit instantiations of type variables. * Calculation commands "moreover" and "also" no longer interfere with current facts ("this"), admitting arbitrary combinations with "then" and derived forms. * Locales: - Goal statements involving the context element "includes" no longer generate theorems with internal delta predicates (those ending on "_axioms") in the premise. Resolve particular premise with .intro to obtain old form. - Fixed bug in type inference ("unify_frozen") that prevented mix of target specification and "includes" elements in goal statement. - Rule sets .intro and .axioms no longer declared as [intro?] and [elim?] (respectively) by default. - Experimental command for instantiation of locales in proof contexts: instantiate