wenzelm@5363: Isabelle NEWS -- history user-relevant changes wenzelm@5363: ============================================== wenzelm@2553: wenzelm@13280: New in this Isabelle release wenzelm@13280: ---------------------------- 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: skalberg@14171: * Pure: Greek letters (except small lambda, \), as well as gothic skalberg@14173: (\...\\...\), caligraphic (\...\), 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: kleing@14234: * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now kleing@14234: allowed in identifiers. Similar to greek letters \<^isub> is now considered kleing@14234: a normal (but invisible) letter. For multiple letter subscripts repeat kleing@14234: \<^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 kleing@14333: PG and LaTeX, text between \<^bsup> and \<^esup> in superscript. The kleing@14333: new control characters are not identifier parts. kleing@14333: schirmer@14361: * Pure: Control-symbols of the form \<^raw...> will literally print the schirmer@14361: content of ... to the latex file instead of \isacntrl... . The ... schirmer@14361: accepts all printable characters excluding the end bracket >. schirmer@14361: schirmer@14361: * Pure: Symbols may only start with one backslash: \<...>. \\<...> is no schirmer@14361: longer accepted by the scanner. 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: skalberg@14503: * Pure: It is now illegal to specify Theory.ML explicitly as a dependency skalberg@14503: in the files section of the theory Theory. (This is more of a diagnostic skalberg@14503: than a restriction, as the theory loader screws up if Theory.ML is manually skalberg@14503: loaded.) skalberg@14503: 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: kleing@14283: * Calculation commands "moreover" and "also": kleing@14283: Do not reset facts ("this") any more. 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@14508: instantiate