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: nipkow@15130: * Theory headers: the new header syntax for Isar theories is nipkow@15130: nipkow@15130: theory wenzelm@16234: imports ... wenzelm@16234: uses ... nipkow@15130: begin nipkow@15130: wenzelm@16234: where the 'uses' part is optional. The previous syntax wenzelm@16234: wenzelm@16234: theory = + ... + : wenzelm@16234: wenzelm@16234: will disappear in the next release. Note that there is no change in wenzelm@16234: ancient non-Isar theories. nipkow@15130: berghofe@15475: * Theory loader: parent theories can now also be referred to via wenzelm@16234: relative and absolute paths. wenzelm@16234: wenzelm@16234: * Improved version of thms_containing searches for a list of criteria wenzelm@16234: instead of a list of constants. Known criteria are: intro, elim, dest, wenzelm@16234: name:string, simp:term, and any term. Criteria can be preceded by '-' wenzelm@16234: to select theorems that do not match. Intro, elim, dest select wenzelm@16234: theorems that match the current goal, name:s selects theorems whose wenzelm@16234: fully qualified name contain s, and simp:term selects all wenzelm@16234: simplification rules whose lhs match term. Any other term is wenzelm@16234: interpreted as pattern and selects all theorems matching the wenzelm@16234: pattern. Available in ProofGeneral under 'ProofGeneral -> Find wenzelm@16234: Theorems' or C-c C-f. Example: wenzelm@16234: wenzelm@16234: C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL." wenzelm@16234: wenzelm@16234: prints the last 100 theorems matching the pattern "(_::nat) + _ + _", wenzelm@16234: matching the current goal as introduction rule and not having "HOL." wenzelm@16234: in their name (i.e. not being defined in theory HOL). wenzelm@16013: wenzelm@15703: wenzelm@15703: *** Document preparation *** wenzelm@15703: wenzelm@16234: * Commands 'display_drafts' and 'print_drafts' perform simple output wenzelm@16234: of raw sources. Only those symbols that do not require additional wenzelm@16234: LaTeX packages (depending on comments in isabellesym.sty) are wenzelm@16234: displayed properly, everything else is left verbatim. isatool display wenzelm@16234: and isatool print are used as front ends (these are subject to the wenzelm@16234: DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively). wenzelm@16234: wenzelm@16234: * There is now a flag to control hiding of proofs and some other wenzelm@16234: commands (such as 'ML' or 'parse/print_translation') in document wenzelm@16234: output. Hiding is enabled by default, and can be disabled by the wenzelm@16234: option '-H false' of isatool usedir or by resetting the reference wenzelm@16234: variable IsarOutput.hide_commands in ML. Additional commands to be wenzelm@16234: hidden may be declared using IsarOutput.add_hidden_commands. wenzelm@16234: wenzelm@15979: * Several new antiquotation: wenzelm@15979: wenzelm@15979: @{term_type term} prints a term with its type annotated; wenzelm@15979: wenzelm@15979: @{typeof term} prints the type of a term; wenzelm@15979: wenzelm@16234: @{const const} is the same as @{term const}, but checks that the wenzelm@16234: argument is a known logical constant; wenzelm@15979: wenzelm@15979: @{term_style style term} and @{thm_style style thm} print a term or wenzelm@16234: theorem applying a "style" to it wenzelm@16234: wenzelm@16234: Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of wenzelm@16234: definitions, equations, inequations etc., 'concl' printing only the wenzelm@16234: conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem9' wenzelm@16234: to print the specified premise. TermStyle.add_style provides an ML wenzelm@16234: interface for introducing further styles. See also the "LaTeX Sugar" wenzelm@16234: document practical applications. wenzelm@16234: wenzelm@16234: wenzelm@16234: *** Pure *** wenzelm@16234: wenzelm@16234: * Considerably improved version of 'constdefs' command. Now performs wenzelm@16234: automatic type-inference of declared constants; additional support for wenzelm@16234: local structure declarations (cf. locales and HOL records), see also wenzelm@16234: isar-ref manual. Potential INCOMPATIBILITY: need to observe strictly wenzelm@16234: sequential dependencies of definitions within a single 'constdefs' wenzelm@16234: section; moreover, the declared name needs to be an identifier. If wenzelm@16234: all fails, consider to fall back on 'consts' and 'defs' separately. wenzelm@16234: wenzelm@16234: * Improved indexed syntax and implicit structures. First of all, wenzelm@16234: indexed syntax provides a notational device for subscripted wenzelm@16234: application, using the new syntax \<^bsub>term\<^esub> for arbitrary wenzelm@16234: expressions. Secondly, in a local context with structure wenzelm@16234: declarations, number indexes \<^sub>n or the empty index (default wenzelm@16234: number 1) refer to a certain fixed variable implicitly; option wenzelm@16234: show_structs controls printing of implicit structures. Typical wenzelm@16234: applications of these concepts involve record types and locales. wenzelm@16234: wenzelm@16234: * New command 'no_syntax' removes grammar declarations (and wenzelm@16234: translations) resulting from the given syntax specification, which is wenzelm@16234: interpreted in the same manner as for the 'syntax' command. wenzelm@16234: wenzelm@16234: * 'Advanced' translation functions (parse_translation etc.) may depend wenzelm@16234: on the signature of the theory context being presently used for wenzelm@16234: parsing/printing, see also isar-ref manual. wenzelm@16234: wenzelm@16234: * Improved internal renaming of symbolic identifiers -- attach primes wenzelm@16234: instead of base 26 numbers. wenzelm@16234: wenzelm@16234: * New flag show_question_marks controls printing of leading question wenzelm@16234: marks in schematic variable names. wenzelm@16234: wenzelm@16234: * In schematic variable names, *any* symbol following \<^isub> or wenzelm@16234: \<^isup> is now treated as part of the base name. For example, the wenzelm@16234: following works without printing of awkward ".0" indexes: wenzelm@16234: wenzelm@16234: lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1" wenzelm@16234: by simp wenzelm@16234: wenzelm@16234: * Inner syntax includes (*(*nested*) comments*). wenzelm@16234: wenzelm@16234: * Pretty pinter now supports unbreakable blocks, specified in mixfix wenzelm@16234: annotations as "(00...)". wenzelm@16234: wenzelm@16234: * Clear separation of logical types and nonterminals, where the latter wenzelm@16234: may only occur in 'syntax' specifications or type abbreviations. wenzelm@16234: Before that distinction was only partially implemented via type class wenzelm@16234: "logic" vs. "{}". Potential INCOMPATIBILITY in rare cases of improper wenzelm@16234: use of 'types'/'consts' instead of 'nonterminals'/'syntax'. Some very wenzelm@16234: exotic syntax specifications may require further adaption wenzelm@16234: (e.g. Cube/Base.thy). wenzelm@16234: wenzelm@16234: * Removed obsolete type class "logic", use the top sort {} instead. wenzelm@16234: Note that non-logical types should be declared as 'nonterminals' wenzelm@16234: rather than 'types'. INCOMPATIBILITY for new object-logic wenzelm@16234: specifications. wenzelm@16234: wenzelm@16234: * Simplifier: can now control the depth to which conditional rewriting wenzelm@16234: is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth wenzelm@16234: Limit. wenzelm@16234: wenzelm@16234: * Simplifier: simplification procedures may now take the current wenzelm@16234: simpset into account (cf. Simplifier.simproc(_i) / mk_simproc wenzelm@16234: interface), which is very useful for calling the Simplifier wenzelm@16234: recursively. Minor INCOMPATIBILITY: the 'prems' argument of simprocs wenzelm@16234: is gone -- use prems_of_ss on the simpset instead. Moreover, the wenzelm@16234: low-level mk_simproc no longer applies Logic.varify internally, to wenzelm@16234: allow for use in a context of fixed variables. wenzelm@16234: wenzelm@16234: * thin_tac now works even if the assumption being deleted contains !! wenzelm@16234: or ==>. More generally, erule now works even if the major premise of wenzelm@16234: the elimination rule contains !! or ==>. wenzelm@16234: wenzelm@16234: * Reorganized bootstrapping of the Pure theories; CPure is now derived wenzelm@16234: from Pure, which contains all common declarations already. Both wenzelm@16234: theories are defined via plain Isabelle/Isar .thy files. wenzelm@16234: INCOMPATIBILITY: elements of CPure (such as the CPure.intro / wenzelm@16234: CPure.elim / CPure.dest attributes) now appear in the Pure name space; wenzelm@16234: use isatool fixcpure to adapt your theory and ML sources. wenzelm@16234: wenzelm@16234: * New syntax 'name(i-j, i-, i, ...)' for referring to specific wenzelm@16234: selections of theorems in named facts via index ranges. wenzelm@16234: wenzelm@16234: wenzelm@16234: *** Locales *** wenzelm@16234: wenzelm@16234: * New commands for the interpretation of locale expressions in wenzelm@16234: theories ('interpretation') and proof contexts ('interpret'). These wenzelm@16234: take an instantiation of the locale parameters and compute proof wenzelm@16234: obligations from the instantiated specification. After the wenzelm@16234: obligations have been discharged, the instantiated theorems of the wenzelm@16234: locale are added to the theory or proof context. Interpretation is wenzelm@16234: smart in that already active interpretations do not occur in proof wenzelm@16234: obligations, neither are instantiated theorems stored in duplicate. wenzelm@16234: Use print_interps to inspect active interpretations of a particular wenzelm@16234: locale. For details, see the Isar Reference manual. wenzelm@16234: wenzelm@16234: INCOMPATIBILITY: former 'instantiate' has been withdrawn, use wenzelm@16234: 'interpret' instead. wenzelm@16234: wenzelm@16234: * Proper static binding of attribute syntax -- i.e. types / terms / wenzelm@16234: facts mentioned as arguments are always those of the locale definition wenzelm@16234: context, independently of the context of later invocations. Moreover, wenzelm@16234: locale operations (renaming and type / term instantiation) are applied wenzelm@16234: to attribute arguments as expected. wenzelm@16234: wenzelm@16234: INCOMPATIBILITY of the ML interface: always pass Attrib.src instead of wenzelm@16234: actual attributes; rare situations may require Attrib.attribute to wenzelm@16234: embed those attributes into Attrib.src that lack concrete syntax. wenzelm@16234: Attribute implementations need to cooperate properly with the static wenzelm@16234: binding mechanism. Basic parsers Args.XXX_typ/term/prop and wenzelm@16234: Attrib.XXX_thm etc. already do the right thing without further wenzelm@16234: intervention. Only unusual applications -- such as "where" or "of" wenzelm@16234: (cf. src/Pure/Isar/attrib.ML), which process arguments depending both wenzelm@16234: on the context and the facts involved -- may have to assign parsed wenzelm@16234: values to argument tokens explicitly. wenzelm@16234: wenzelm@16234: * New context element "constrains" adds type constraints to parameters -- wenzelm@16234: there is no logical significance. wenzelm@16234: wenzelm@16234: * Context expressions: renaming parameters permits syntax wenzelm@16234: redeclaration as well. wenzelm@16234: wenzelm@16234: * Locale definition: 'includes' now disallowed. wenzelm@16234: wenzelm@16234: * Changed parameter management in theorem generation for long goal wenzelm@16234: statements with 'includes'. INCOMPATIBILITY: produces a different wenzelm@16234: theorem statement in rare situations. wenzelm@16234: wenzelm@16234: * Attributes 'induct' and 'cases': type or set names may now be wenzelm@16234: locally fixed variables as well. wenzelm@15703: wenzelm@15703: * Antiquotations now provide the option 'locale=NAME' to specify an wenzelm@16234: alternative context used for evaluating and printing the subsequent wenzelm@16234: argument, as in @{thm [locale=LC] fold_commute}, for example. wenzelm@16234: wenzelm@16234: wenzelm@16234: *** Provers *** wenzelm@16234: wenzelm@16234: * Provers/hypsubst.ML: improved version of the subst method, for wenzelm@16234: single-step rewriting: it now works in bound variable contexts. New is wenzelm@16234: 'subst (asm)', for rewriting an assumption. INCOMPATIBILITY: may wenzelm@16234: rewrite a different subterm than the original subst method, which is wenzelm@16234: still available as 'simplesubst'. wenzelm@16234: wenzelm@16234: * Provers/quasi.ML: new transitivity reasoners for transitivity only wenzelm@16234: and quasi orders. wenzelm@16234: wenzelm@16234: * Provers/trancl.ML: new transitivity reasoner for transitive and wenzelm@16234: reflexive-transitive closure of relations. wenzelm@16234: wenzelm@16234: * Provers/blast.ML: new reference depth_limit to make blast's depth wenzelm@16234: limit (previously hard-coded with a value of 20) user-definable. wenzelm@16234: wenzelm@16234: * Provers/simplifier.ML has been moved to Pure, where Simplifier.setup wenzelm@16234: is peformed already. Object-logics merely need to finish their wenzelm@16234: initial simpset configuration as before. INCOMPATIBILITY. wenzelm@15703: berghofe@15475: schirmer@14700: *** HOL *** schirmer@14700: wenzelm@16234: * 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@16234: The symbol \ is displayed as the alternative epsilon of LaTeX wenzelm@16234: and x-symbol; use option '-m epsilon' to get it actually printed. wenzelm@16234: Moreover, the mathematically important symbolic identifier \ wenzelm@16234: becomes available as variable, constant etc. INCOMPATIBILITY, wenzelm@16234: wenzelm@16234: * "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x". wenzelm@16234: Similarly for all quantifiers: "ALL x > y" etc. The x-symbol for >= wenzelm@16234: is \. wenzelm@16234: wenzelm@16234: * "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\" wenzelm@16234: instead of ":". wenzelm@16234: wenzelm@16234: * theory SetInterval: changed the syntax for open intervals: wenzelm@16234: wenzelm@16234: Old New wenzelm@16234: {..n(} {.. {\1<\.\.} nipkow@15046: \.\.\([^(}]*\)(} -> \.\.<\1} nipkow@15046: wenzelm@16234: * theory Finite_Set: changed the syntax for 'setsum', summation over wenzelm@16234: finite sets: "setsum (%x. e) A", which used to be "\x:A. e", is wenzelm@16234: now either "SUM x:A. e" or "\x \ A. e". wenzelm@16234: wenzelm@16234: Some new syntax forms are available: wenzelm@16234: wenzelm@16234: "\x | P. e" for "setsum (%x. e) {x. P}" wenzelm@16234: "\x = a..b. e" for "setsum (%x. e) {a..b}" wenzelm@16234: "\x = a..x < k. e" for "setsum (%x. e) {..x < k. e" used to be based on a separate wenzelm@16234: function "Summation", which has been discontinued. wenzelm@16234: wenzelm@16234: * theory Finite_Set: in structured induction proofs, the insert case wenzelm@16234: is now 'case (insert x F)' instead of the old counterintuitive 'case wenzelm@16234: (insert F x)'. wenzelm@16234: wenzelm@16234: * The 'refute' command has been extended to support a much larger wenzelm@16234: fragment of HOL, including axiomatic type classes, constdefs and wenzelm@16234: typedefs, inductive datatypes and recursion. wenzelm@16234: wenzelm@16234: * Datatype induction via method 'induct' now preserves the name of the wenzelm@16234: induction variable. For example, when proving P(xs::'a list) by wenzelm@16234: induction on xs, the induction step is now P(xs) ==> P(a#xs) rather wenzelm@16234: than P(list) ==> P(a#list) as previously. Potential INCOMPATIBILITY wenzelm@16234: in unstructured proof scripts. wenzelm@16234: wenzelm@16234: * Reworked implementation of records. Improved scalability for wenzelm@16234: records with many fields, avoiding performance problems for type wenzelm@16234: inference. Records are no longer composed of nested field types, but wenzelm@16234: of nested extension types. Therefore the record type only grows linear wenzelm@16234: in the number of extensions and not in the number of fields. The wenzelm@16234: top-level (users) view on records is preserved. Potential wenzelm@16234: INCOMPATIBILITY only in strange cases, where the theory depends on the wenzelm@16234: old record representation. The type generated for a record is called wenzelm@16234: _ext_type. wenzelm@16234: wenzelm@16234: Flag record_quick_and_dirty_sensitive can be enabled to skip the wenzelm@16234: proofs triggered by a record definition or a simproc (if wenzelm@16234: quick_and_dirty is enabled). Definitions of large records can take wenzelm@16234: quite long. wenzelm@16234: wenzelm@16234: New simproc record_upd_simproc for simplification of multiple record wenzelm@16234: updates enabled by default. Moreover, trivial updates are also wenzelm@16234: removed: r(|x := x r|) = r. INCOMPATIBILITY: old proofs break wenzelm@16234: occasionally, since simplification is more powerful by default. wenzelm@16234: wenzelm@16234: * Simplifier: automatically reasons about transitivity chains wenzelm@16234: involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics wenzelm@16234: provided by Provers/trancl.ML as additional solvers. INCOMPATIBILITY: wenzelm@16234: old proofs break occasionally as simplification may now solve more wenzelm@16234: goals than previously. wenzelm@16234: wenzelm@16234: * Simplifier: converts x <= y into x = y if assumption y <= x is wenzelm@16234: present. Works for all partial orders (class "order"), in particular wenzelm@16234: numbers and sets. For linear orders (e.g. numbers) it treats ~ x < y wenzelm@16234: just like y <= x. wenzelm@16234: wenzelm@16234: * Simplifier: new simproc for "let x = a in f x". If a is a free or wenzelm@16234: bound variable or a constant then the let is unfolded. Otherwise wenzelm@16234: first a is simplified to b, and then f b is simplified to g. If wenzelm@16234: possible we abstract b from g arriving at "let x = b in h x", wenzelm@16234: otherwise we unfold the let and arrive at g. The simproc can be wenzelm@16234: enabled/disabled by the reference use_let_simproc. Potential wenzelm@16234: INCOMPATIBILITY since simplification is more powerful by default. webertj@15776: wenzelm@14655: wenzelm@14682: *** HOLCF *** wenzelm@14682: wenzelm@14682: * HOLCF: discontinued special version of 'constdefs' (which used to wenzelm@16234: support continuous functions) in favor of the general Pure one with wenzelm@16234: full type-inference. wenzelm@14682: wenzelm@14682: paulson@14885: *** ZF *** paulson@14885: wenzelm@16234: * ZF/ex: theories Group and Ring provide examples in abstract algebra, wenzelm@16234: including the First Isomorphism Theorem (on quotienting by the kernel wenzelm@16234: of a homomorphism). wenzelm@15089: wenzelm@15089: * ZF/Simplifier: install second copy of type solver that actually wenzelm@16234: makes use of TC rules declared to Isar proof contexts (or locales); wenzelm@16234: the old version is still required for ML proof scripts. wenzelm@15703: wenzelm@15703: wenzelm@15703: *** ML *** wenzelm@15703: wenzelm@15973: * Pure/library.ML no longer defines its own option datatype, but uses wenzelm@16234: that of the SML basis, which has constructors NONE and SOME instead of wenzelm@16234: None and Some, as well as exception Option.Option instead of OPTION. wenzelm@16234: The functions the, if_none, is_some, is_none have been adapted wenzelm@16234: accordingly, while Option.map replaces apsome. wenzelm@15973: wenzelm@16151: * The exception LIST has been given up in favour of the standard wenzelm@16234: exceptions Empty and Subscript, as well as Library.UnequalLengths. wenzelm@16234: Function like Library.hd and Library.tl are superceded by the standard wenzelm@16234: hd and tl functions etc. wenzelm@16234: wenzelm@16234: A number of basic functions are now no longer exported to the ML wenzelm@16234: toplevel, as they are variants of standard functions. The following wenzelm@16234: suggests how one can translate existing code: wenzelm@15973: wenzelm@15973: rev_append xs ys = List.revAppend (xs, ys) wenzelm@15973: nth_elem (i, xs) = List.nth (xs, i) wenzelm@15973: last_elem xs = List.last xs wenzelm@15973: flat xss = List.concat xss wenzelm@16234: seq fs = List.app fs wenzelm@15973: partition P xs = List.partition P xs wenzelm@15973: filter P xs = List.filter P xs wenzelm@15973: mapfilter f xs = List.mapPartial f xs wenzelm@15973: wenzelm@15703: * Pure: output via the Isabelle channels of writeln/warning/error wenzelm@16234: etc. is now passed through Output.output, with a hook for arbitrary wenzelm@16234: transformations depending on the print_mode (cf. Output.add_mode -- wenzelm@16234: the first active mode that provides a output function wins). Already wenzelm@16234: formatted output may be embedded into further text via Output.raw; the wenzelm@16234: result of Pretty.string_of/str_of and derived functions wenzelm@16234: (string_of_term/cterm/thm etc.) is already marked raw to accommodate wenzelm@16234: easy composition of diagnostic messages etc. Programmers rarely need wenzelm@16234: to care about Output.output or Output.raw at all, with some notable wenzelm@16234: exceptions: Output.output is required when bypassing the standard wenzelm@16234: channels (writeln etc.), or in token translations to produce properly wenzelm@16234: formatted results; Output.raw is required when capturing already wenzelm@16234: output material that will eventually be presented to the user a second wenzelm@16234: time. For the default print mode, both Output.output and Output.raw wenzelm@16234: have no effect. wenzelm@16234: wenzelm@16234: * Pure: print_tac now outputs the goal through the trace channel. wenzelm@16234: wenzelm@16234: * Isar debugging: new reference Toplevel.debug; default false. Set to wenzelm@16234: make printing of exceptions THM, TERM, TYPE and THEORY more verbose. wenzelm@15703: wenzelm@16151: * Pure: name spaces have been refined, with significant changes of the wenzelm@16234: internal interfaces -- INCOMPATIBILITY. Renamed cond_extern(_table) wenzelm@16234: to extern(_table). The plain name entry path is superceded by a wenzelm@16234: general 'naming' context, which also includes the 'policy' to produce wenzelm@16234: a fully qualified name and external accesses of a fully qualified wenzelm@16234: name; NameSpace.extend is superceded by context dependent wenzelm@16234: Sign.declare_name. Several theory and proof context operations modify wenzelm@16234: the naming context. Especially note Theory.restore_naming and wenzelm@16234: ProofContext.restore_naming to get back to a sane state; note that wenzelm@16234: Theory.add_path is no longer sufficient to recover from wenzelm@16234: Theory.absolute_path in particular. wenzelm@16234: wenzelm@16234: * Pure: new flags short_names (default false) and unique_names wenzelm@16234: (default true) for controlling output of qualified names. If wenzelm@16234: short_names is set, names are printed unqualified. If unique_names is wenzelm@16234: reset, the name prefix is reduced to the minimum required to achieve wenzelm@16234: the original result when interning again, even if there is an overlap wenzelm@16234: with earlier declarations. wenzelm@16151: wenzelm@16456: * Pure/TheoryDataFun: change of the argument structure; 'prep_ext' is wenzelm@16456: now 'extend', and 'merge' gets an additional Pretty.pp argument wenzelm@16456: (useful for printing error messages). INCOMPATIBILITY. wenzelm@16456: wenzelm@16456: * Pure: major reorganization of the theory context. Type Sign.sg and wenzelm@16456: Theory.theory are now identified, referring to the universal wenzelm@16456: Context.theory (see Pure/context.ML). Actual signature and theory wenzelm@16456: content is managed as theory data. The old code and interfaces were wenzelm@16456: spread over many files and structures; the new arrangement introduces wenzelm@16456: considerable INCOMPATIBILITY to gain more clarity: wenzelm@16456: wenzelm@16456: Context -- theory management operations (name, identity, inclusion, wenzelm@16456: parents, ancestors, merge, etc.), plus generic theory data; wenzelm@16456: wenzelm@16456: Sign -- logical signature and syntax operations (declaring consts, wenzelm@16456: types, etc.), plus certify/read for common entities; wenzelm@16456: wenzelm@16456: Theory -- logical theory operations (stating axioms, definitions, wenzelm@16456: oracles), plus a copy of logical signature operations (consts, wenzelm@16456: types, etc.); also a few basic management operations (Theory.copy, wenzelm@16456: Theory.merge, etc.) wenzelm@16456: wenzelm@16456: The most basic sign_of operations (Theory.sign_of, Thm.sign_of_thm wenzelm@16456: etc.) as well as the sign field in Thm.rep_thm etc. have been retained wenzelm@16456: for convenience -- they merely return the theory. wenzelm@16456: wenzelm@16373: * Pure/sign/theory: discontinued named name spaces (i.e. classK, wenzelm@16373: typeK, constK, axiomK, oracleK), but provide explicit operations for wenzelm@16373: any of these kinds. For example, Sign.intern typeK is now wenzelm@16373: Sign.intern_type, Theory.hide_space Sign.typeK is now wenzelm@16373: Theory.hide_types. Also note that former wenzelm@16373: Theory.hide_classes/types/consts are now wenzelm@16373: Theory.hide_classes_i/types_i/consts_i, while the non '_i' versions wenzelm@16373: internalize their arguments! INCOMPATIBILITY. wenzelm@16373: wenzelm@16151: * Pure: cases produced by proof methods specify options, where NONE wenzelm@16234: means to remove case bindings -- INCOMPATIBILITY in wenzelm@16234: (RAW_)METHOD_CASES. wenzelm@16151: wenzelm@16373: * Pure: the following operations retrieve axioms or theorems from a wenzelm@16373: theory node or theory hierarchy, respectively: wenzelm@16373: wenzelm@16373: Theory.axioms_of: theory -> (string * term) list wenzelm@16373: Theory.all_axioms_of: theory -> (string * term) list wenzelm@16373: PureThy.thms_of: theory -> (string * thm) list wenzelm@16373: PureThy.all_thms_of: theory -> (string * thm) list wenzelm@16373: wenzelm@15703: * Provers: Simplifier and Classical Reasoner now support proof context wenzelm@16234: dependent plug-ins (simprocs, solvers, wrappers etc.). These extra wenzelm@16234: components are stored in the theory and patched into the wenzelm@16234: simpset/claset when used in an Isar proof context. Context dependent wenzelm@16234: components are maintained by the following theory operations: wenzelm@16234: wenzelm@16234: Simplifier.add_context_simprocs wenzelm@16234: Simplifier.del_context_simprocs wenzelm@16234: Simplifier.set_context_subgoaler wenzelm@16234: Simplifier.reset_context_subgoaler wenzelm@16234: Simplifier.add_context_looper wenzelm@16234: Simplifier.del_context_looper wenzelm@16234: Simplifier.add_context_unsafe_solver wenzelm@16234: Simplifier.add_context_safe_solver wenzelm@16234: wenzelm@16234: Classical.add_context_safe_wrapper wenzelm@16234: Classical.del_context_safe_wrapper wenzelm@16234: Classical.add_context_unsafe_wrapper wenzelm@16234: Classical.del_context_unsafe_wrapper wenzelm@16234: wenzelm@16234: IMPORTANT NOTE: proof tools (methods etc.) need to use wenzelm@16234: local_simpset_of and local_claset_of to instead of the primitive wenzelm@16234: Simplifier.get_local_simpset and Classical.get_local_claset, wenzelm@16234: respectively, in order to see the context dependent fields! wenzelm@16234: wenzelm@16251: * File.sysify_path and File.quote_sysify path have been replaced by wenzelm@16251: File.platform_path and File.shell_path (with appropriate hooks). This wenzelm@16251: provides a clean interface for unusual systems where the internal and wenzelm@16251: external process view of file names are different. wenzelm@16251: wenzelm@16234: wenzelm@16234: *** System *** wenzelm@16234: wenzelm@16234: * Allow symlinks to all proper Isabelle executables (Isabelle, wenzelm@16234: isabelle, isatool etc.). wenzelm@16234: wenzelm@16234: * ISABELLE_DOC_FORMAT setting specifies preferred document format (for wenzelm@16234: isatool doc, isatool mkdir, display_drafts etc.). wenzelm@16234: wenzelm@16234: * isatool usedir: option -f allows specification of the ML file to be wenzelm@16234: used by Isabelle; default is ROOT.ML. wenzelm@16234: wenzelm@16251: * New isatool version outputs the version identifier of the Isabelle wenzelm@16251: distribution being used. wenzelm@16251: wenzelm@16251: * HOL: new isatool dimacs2hol converts files in DIMACS CNF format wenzelm@16234: (containing Boolean satisfiability problems) into Isabelle/HOL wenzelm@16234: theories. wenzelm@15703: wenzelm@15703: 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