diff -r 38e0219ec022 -r 551c9a4dd693 NEWS --- a/NEWS Thu Sep 15 16:15:22 2005 +0200 +++ b/NEWS Thu Sep 15 17:16:53 2005 +0200 @@ -24,16 +24,15 @@ * Theory loader: parent theories can now also be referred to via relative and absolute paths. -* Improved version of thms_containing searches for a list of criteria -instead of a list of constants. Known criteria are: intro, elim, dest, -name:string, simp:term, and any term. Criteria can be preceded by '-' -to select theorems that do not match. Intro, elim, dest select -theorems that match the current goal, name:s selects theorems whose -fully qualified name contain s, and simp:term selects all -simplification rules whose lhs match term. Any other term is -interpreted as pattern and selects all theorems matching the -pattern. Available in ProofGeneral under 'ProofGeneral -> Find -Theorems' or C-c C-f. Example: +* Command 'find_theorems' searches for a list of criteria instead of a +list of constants. Known criteria are: intro, elim, dest, name:string, +simp:term, and any term. Criteria can be preceded by '-' to select +theorems that do not match. Intro, elim, dest select theorems that +match the current goal, name:s selects theorems whose fully qualified +name contain s, and simp:term selects all simplification rules whose +lhs match term. Any other term is interpreted as pattern and selects +all theorems matching the pattern. Available in ProofGeneral under +'ProofGeneral -> Find Theorems' or C-c C-f. Example: C-c C-f (100) "(_::nat) + _ + _" intro -name: "HOL." @@ -41,10 +40,13 @@ matching the current goal as introduction rule and not having "HOL." in their name (i.e. not being defined in theory HOL). +* Command 'thms_containing' has been discontinued in favour of +'find_theorems'; INCOMPATIBILITY. + * Communication with Proof General is now 8bit clean, which means that Unicode text in UTF-8 encoding may be used within theory texts (both -formal and informal parts). See option -U of the Isabelle Proof -General interface. +formal and informal parts). Cf. option -U of the Isabelle Proof +General interface; HOL/ex/Hebrew.thy provides a simple example. *** Document preparation *** @@ -524,7 +526,7 @@ x |> f f #> g (x, y) |-> f f #-> g -* Pure/library.ML: canonical list combinators fold, fold_rev, and +* Pure/library.ML: natural list combinators fold, fold_rev, and fold_map support linear functional transformations and nesting. For example: @@ -540,59 +542,61 @@ (fold o fold) f [xs1, ..., xsN] = fold f xs1 #> ... #> fold f xsN -* Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types, -fold_types traverse types/terms from left to right, observing -canonical argument order. Supercedes previous foldl_XXX versions, -add_frees, add_vars etc. have been adapted as well: INCOMPATIBILITY. - -* Pure: 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. - -* Pure: Output.time_accumulator NAME creates an operator ('a -> 'b) -> -'a -> 'b to measure runtime and count invocations; the cumulative -results are displayed at the end of a batch session. - -* Isar toplevel: improved diagnostics, mostly for Poly/ML only. -Reference Toplevel.debug (default false) controls detailed printing -and tracing of low-level exceptions; Toplevel.profiling (default 0) -controls execution profiling -- set to 1 for time and 2 for space -(both increase the runtime). - -* Isar session: The initial use of ROOT.ML is now always timed, -i.e. the log will show the actual process times, in contrast to the -elapsed wall-clock time that the outer shell wrapper produces. - -* Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a -reasonably efficient light-weight implementation of sets as lists. - -* Pure: structure AList (cf. Pure/General/alist.ML) superseedes the -former associaton list functions in library. INCOMPATIBILITY. -Naive rewrites: - - assoc == uncurry (AList.lookup (op =)) - assocs == these oo AList.lookup (op =) - overwrite == uncurry (AList.update (op =)) o swap - -* Pure: new functions in the family of normalisators for the option type: - - the: 'a option -> 'a - these: 'a option -> 'a where 'a = 'b list +* Pure/library.ML: the following selectors on type 'a option are +available: + + the: 'a option -> 'a (*partial*) + these: 'a option -> 'a where 'a = 'b list the_default: 'a -> 'a option -> 'a the_list: 'a option -> 'a list +* Pure/General: structure AList (cf. Pure/General/alist.ML) provides +basic operations for association lists, following natural argument +order. The old functions may be expressed as follows: + + assoc = uncurry (AList.lookup (op =)) + assocs = these oo AList.lookup (op =) + overwrite = uncurry (AList.update (op =)) o swap + +* Pure/General: structure AList (cf. Pure/General/alist.ML) provides +basic operations for association lists, following natural argument +order; moreover the explicit equality predicate passed here avoids +potentially expensive polymorphic runtime equality checks. + +* Pure/General: structure OrdList (cf. Pure/General/ord_list.ML) +provides a reasonably efficient light-weight implementation of sets as +lists. + +* Pure/General: generic tables (cf. Pure/General/table.ML) provide a +few new operations; existing lookup and update are now curried to +follow natural argument order (for use with fold etc.); +INCOMPATIBILITY, use (uncurry Symtab.lookup) etc. as last resort. + +* Pure/General: 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. + +* Pure/General: Output.time_accumulator NAME creates an operator ('a +-> 'b) -> 'a -> 'b to measure runtime and count invocations; the +cumulative results are displayed at the end of a batch session. + +* Pure/General: File.sysify_path and File.quote_sysify path have been +replaced by File.platform_path and File.shell_path (with appropriate +hooks). This provides a clean interface for unusual systems where the +internal and external process view of file names are different. + * Pure: more efficient orders for basic syntactic entities: added fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord and typ_ord to use fast_string_ord and fast_indexname_ord (term_ord is @@ -601,6 +605,11 @@ particular order for Symtab.keys, Symtab.dest, etc. (consider using Library.sort_strings on result). +* Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types, +fold_types traverse types/terms from left to right, observing natural +argument order. Supercedes previous foldl_XXX versions, add_frees, +add_vars etc. have been adapted as well: INCOMPATIBILITY. + * Pure: name spaces have been refined, with significant changes of the internal interfaces -- INCOMPATIBILITY. Renamed cond_extern(_table) to extern(_table). The plain name entry path is superceded by a @@ -680,14 +689,24 @@ * Pure: print_tac now outputs the goal through the trace channel. -* Pure/Simplifier: improved handling of bound variables (nameless +* Isar toplevel: improved diagnostics, mostly for Poly/ML only. +Reference Toplevel.debug (default false) controls detailed printing +and tracing of low-level exceptions; Toplevel.profiling (default 0) +controls execution profiling -- set to 1 for time and 2 for space +(both increase the runtime). + +* Isar session: The initial use of ROOT.ML is now always timed, +i.e. the log will show the actual process times, in contrast to the +elapsed wall-clock time that the outer shell wrapper produces. + +* Simplifier: improved handling of bound variables (nameless representation, avoid allocating new strings). Simprocs that invoke the Simplifier recursively should use Simplifier.inherit_bounds to avoid local name clashes. -* Pure/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 +* 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: @@ -710,11 +729,6 @@ Simplifier.get_local_simpset and Classical.get_local_claset, respectively, in order to see the context dependent fields! -* File.sysify_path and File.quote_sysify path have been replaced by -File.platform_path and File.shell_path (with appropriate hooks). This -provides a clean interface for unusual systems where the internal and -external process view of file names are different. - * ML functions legacy_bindings and use_legacy_bindings produce ML fact bindings for all theorems stored within a given theory; this may help in porting non-Isar theories to Isar ones, while keeping ML proof