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