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:
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@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@14816: * Pure: tuned internal renaming of symbolic identifiers -- attach
wenzelm@14816: primes instead of base 26 numbers.
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@14897: fold_commute}, for example. Note that a proof context is escaped to
wenzelm@14897: the enclosing theory context first.
wenzelm@14897:
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@14917: be presented to the user a second time.
wenzelm@14795:
wenzelm@14707:
schirmer@14700: *** HOL ***
schirmer@14700:
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@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:
wenzelm@14731: * Simplifier: "record_upd_simproc" for simplification of multiple
wenzelm@14731: record updates enabled by default. INCOMPATIBILITY: old proofs
wenzelm@14731: break occasionally, since simplification is more powerful by
wenzelm@14731: default.
wenzelm@14731:
wenzelm@14655:
wenzelm@14682: *** HOLCF ***
wenzelm@14682:
wenzelm@14682: * HOLCF: discontinued special version of 'constdefs' (which used to
wenzelm@14731: support continuous functions) in favor of the general Pure one with
wenzelm@14731: full type-inference.
wenzelm@14682:
wenzelm@14682:
paulson@14885: *** ZF ***
paulson@14885:
paulson@14885: * ZF/ex/{Group,Ring}: examples in abstract algebra, including the First
paulson@14885: Isomorphism Theorem (on quotienting by the kernel of a homomorphism).
paulson@14885:
paulson@14885:
wenzelm@14655:
wenzelm@14606: New in Isabelle2004 (April 2004)
wenzelm@14606: --------------------------------
wenzelm@13280:
skalberg@14171: *** General ***
skalberg@14171:
ballarin@14398: * Provers/order.ML: new efficient reasoner for partial and linear orders.
ballarin@14398: Replaces linorder.ML.
ballarin@14398:
wenzelm@14606: * Pure: Greek letters (except small lambda, \), 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