imports <theory1> ... <theoryn>

   imports <theory1> ... <theoryN>

   uses <file1> ... <fileM>

   optionally also with a "files" section. The syntax

 where the 'uses' part is optional.  The previous syntax

   theory <name> = <theory1> + ... + <theoryn>:

   theory <name> = <theory1> + ... + <theoryN>:

   will still be supported for some time but will eventually disappear.

 will disappear in the next release.  Note that there is no change in

   The syntax of old-style theories has not changed.

 ancient non-Isar theories.

   relative and absolute paths.

 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:

   C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL."

 prints the last 100 theorems matching the pattern "(_::nat) + _ + _",

 matching the current goal as introduction rule and not having "HOL."

 in their name (i.e. not being defined in theory HOL).

 *** Document preparation ***

 * Commands 'display_drafts' and 'print_drafts' perform simple output

 of raw sources.  Only those symbols that do not require additional

 LaTeX packages (depending on comments in isabellesym.sty) are

 displayed properly, everything else is left verbatim.  isatool display

 and isatool print are used as front ends (these are subject to the

 DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively).

 * There is now a flag to control hiding of proofs and some other

 commands (such as 'ML' or 'parse/print_translation') in document

 output.  Hiding is enabled by default, and can be disabled by the

 option '-H false' of isatool usedir or by resetting the reference

 variable IsarOutput.hide_commands in ML.  Additional commands to be

 hidden may be declared using IsarOutput.add_hidden_commands.

 * Several new antiquotation:

   @{term_type term} prints a term with its type annotated;

   @{typeof term} prints the type of a term;

   @{const const} is the same as @{term const}, but checks that the

   argument is a known logical constant;

   @{term_style style term} and @{thm_style style thm} print a term or

   theorem applying a "style" to it

 Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of

 definitions, equations, inequations etc., 'concl' printing only the

 conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem9'

 to print the specified premise.  TermStyle.add_style provides an ML

 interface for introducing further styles.  See also the "LaTeX Sugar"

 document practical applications.

 *** Pure ***

 * Considerably improved version of 'constdefs' command.  Now performs

 automatic type-inference of declared constants; additional support for

 local structure declarations (cf. locales and HOL records), see also

 isar-ref manual.  Potential INCOMPATIBILITY: need to observe strictly

 sequential dependencies of definitions within a single 'constdefs'

 section; moreover, the declared name needs to be an identifier.  If

 all fails, consider to fall back on 'consts' and 'defs' separately.

 * Improved indexed syntax and implicit structures.  First of all,

 indexed syntax provides a notational device for subscripted

 application, using the new syntax \<^bsub>term\<^esub> for arbitrary

 expressions.  Secondly, in a local context with structure

 declarations, number indexes \<^sub>n or the empty index (default

 number 1) refer to a certain fixed variable implicitly; option

 show_structs controls printing of implicit structures.  Typical

 applications of these concepts involve record types and locales.

 * New command 'no_syntax' removes grammar declarations (and

 translations) resulting from the given syntax specification, which is

 interpreted in the same manner as for the 'syntax' command.

 * 'Advanced' translation functions (parse_translation etc.) may depend

 on the signature of the theory context being presently used for

 parsing/printing, see also isar-ref manual.

 * Improved internal renaming of symbolic identifiers -- attach primes

 instead of base 26 numbers.

 * New flag show_question_marks controls printing of leading question

 marks in schematic variable names.

 * In schematic variable names, *any* symbol following \<^isub> or

 \<^isup> is now treated as part of the base name.  For example, the

 following works without printing of awkward ".0" indexes:

   lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1"

     by simp

 * Inner syntax includes (*(*nested*) comments*).

 * Pretty pinter now supports unbreakable blocks, specified in mixfix

 annotations as "(00...)".

 * Clear separation of logical types and nonterminals, where the latter

 may only occur in 'syntax' specifications or type abbreviations.

 Before that distinction was only partially implemented via type class

 "logic" vs. "{}".  Potential INCOMPATIBILITY in rare cases of improper

 use of 'types'/'consts' instead of 'nonterminals'/'syntax'.  Some very

 exotic syntax specifications may require further adaption

 (e.g. Cube/Base.thy).

 * Removed obsolete type class "logic", use the top sort {} instead.

 Note that non-logical types should be declared as 'nonterminals'

 rather than 'types'.  INCOMPATIBILITY for new object-logic

 specifications.

 * Simplifier: can now control the depth to which conditional rewriting

 is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth

 Limit.

 * Simplifier: simplification procedures may now take the current

 simpset into account (cf. Simplifier.simproc(_i) / mk_simproc

 interface), which is very useful for calling the Simplifier

 recursively.  Minor INCOMPATIBILITY: the 'prems' argument of simprocs

 is gone -- use prems_of_ss on the simpset instead.  Moreover, the

 low-level mk_simproc no longer applies Logic.varify internally, to

 allow for use in a context of fixed variables.

 * thin_tac now works even if the assumption being deleted contains !!

 or ==>.  More generally, erule now works even if the major premise of

 the elimination rule contains !! or ==>.

 * Reorganized bootstrapping of the Pure theories; CPure is now derived

 from Pure, which contains all common declarations already.  Both

 theories are defined via plain Isabelle/Isar .thy files.

 INCOMPATIBILITY: elements of CPure (such as the CPure.intro /

 CPure.elim / CPure.dest attributes) now appear in the Pure name space;

 use isatool fixcpure to adapt your theory and ML sources.

 * New syntax 'name(i-j, i-, i, ...)' for referring to specific

 selections of theorems in named facts via index ranges.

 *** Locales ***

 * New commands for the interpretation of locale expressions in

 theories ('interpretation') and proof contexts ('interpret').  These

 take an instantiation of the locale parameters and compute proof

 obligations from the instantiated specification.  After the

 obligations have been discharged, the instantiated theorems of the

 locale are added to the theory or proof context.  Interpretation is

 smart in that already active interpretations do not occur in proof

 obligations, neither are instantiated theorems stored in duplicate.

 Use print_interps to inspect active interpretations of a particular

 locale.  For details, see the Isar Reference manual.

 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use

 'interpret' instead.

 * Proper static binding of attribute syntax -- i.e. types / terms /

 facts mentioned as arguments are always those of the locale definition

 context, independently of the context of later invocations.  Moreover,

 locale operations (renaming and type / term instantiation) are applied

 to attribute arguments as expected.

 INCOMPATIBILITY of the ML interface: always pass Attrib.src instead of

 actual attributes; rare situations may require Attrib.attribute to

 embed those attributes into Attrib.src that lack concrete syntax.

 Attribute implementations need to cooperate properly with the static

 binding mechanism.  Basic parsers Args.XXX_typ/term/prop and

 Attrib.XXX_thm etc. already do the right thing without further

 intervention.  Only unusual applications -- such as "where" or "of"

 (cf. src/Pure/Isar/attrib.ML), which process arguments depending both

 on the context and the facts involved -- may have to assign parsed

 values to argument tokens explicitly.

 * New context element "constrains" adds type constraints to parameters --

 there is no logical significance.

 * Context expressions: renaming parameters permits syntax

 redeclaration as well.

 * Locale definition: 'includes' now disallowed.

 * Changed parameter management in theorem generation for long goal

 statements with 'includes'.  INCOMPATIBILITY: produces a different

 theorem statement in rare situations.

 * Attributes 'induct' and 'cases': type or set names may now be

 locally fixed variables as well.

 * Antiquotations now provide the option 'locale=NAME' to specify an

 alternative context used for evaluating and printing the subsequent

 argument, as in @{thm [locale=LC] fold_commute}, for example.

 *** Provers ***

 * Provers/hypsubst.ML: improved version of the subst method, for

 single-step rewriting: it now works in bound variable contexts. New is

 'subst (asm)', for rewriting an assumption.  INCOMPATIBILITY: may

 rewrite a different subterm than the original subst method, which is

 still available as 'simplesubst'.

   and quasi orders.

 and quasi orders.

   reflexive-transitive closure of relations.

 reflexive-transitive closure of relations.

   limit (previously hard-coded with a value of 20) user-definable.

 limit (previously hard-coded with a value of 20) user-definable.

 * Provers: new version of the subst method, for single-step rewriting: it now

   works in bound variable contexts. New is subst (asm), for rewriting an

   assumption. Thanks to Lucas Dixon! INCOMPATIBILITY: may rewrite a different

   subterm than the original subst method, which is still available under the

   name simplesubst.

 * Pure: thin_tac now works even if the assumption being deleted contains !! or ==>. 

   More generally, erule now works even if the major premise of the elimination rule

   contains !! or ==>.

 * Pure: considerably improved version of 'constdefs' command.  Now

   performs automatic type-inference of declared constants; additional

   support for local structure declarations (cf. locales and HOL

   records), see also isar-ref manual.  Potential INCOMPATIBILITY: need

   to observe strictly sequential dependencies of definitions within a

   single 'constdefs' section; moreover, the declared name needs to be

   an identifier.  If all fails, consider to fall back on 'consts' and

   'defs' separately.

 * Pure: improved indexed syntax and implicit structures.  First of

   all, indexed syntax provides a notational device for subscripted

   application, using the new syntax \<^bsub>term\<^esub> for arbitrary

   expressions.  Secondly, in a local context with structure

   declarations, number indexes \<^sub>n or the empty index (default

   number 1) refer to a certain fixed variable implicitly; option

   show_structs controls printing of implicit structures.  Typical

   applications of these concepts involve record types and locales.

 * Pure: clear separation of logical types and nonterminals, where the

   latter may only occur in 'syntax' specifications or type

   abbreviations.  Before that distinction was only partially

   implemented via type class "logic" vs. "{}".  Potential

   INCOMPATIBILITY in rare cases of improper use of 'types'/'consts'

   instead of 'nonterminals'/'syntax'.  Some very exotic syntax

   specifications may require further adaption (e.g. Cube/Base.thy).

 * Pure: removed obsolete type class "logic", use the top sort {}

   instead.  Note that non-logical types should be declared as

   'nonterminals' rather than 'types'.  INCOMPATIBILITY for new

   object-logic specifications.

 * Pure: command 'no_syntax' removes grammar declarations (and

   translations) resulting from the given syntax specification, which

   is interpreted in the same manner as for the 'syntax' command.

 * Pure: print_tac now outputs the goal through the trace channel.

 * Pure: reference NameSpace.unique_names included.  If true the

   (shortest) namespace-prefix is printed to disambiguate conflicts (as

   yet). If false the first entry wins (as during parsing). Default

   value is true.

 * Pure: tuned internal renaming of symbolic identifiers -- attach

   primes instead of base 26 numbers.

 * Pure: new flag show_question_marks controls printing of leading

   question marks in schematic variable names.

 * Pure: new version of thms_containing that 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."

   prints the last 100 theorems matching the pattern "(_::nat) + _ + _",

   matching the current goal as introduction rule and not having "HOL." 

   in their name (i.e. not being defined in theory HOL).

 * Pure/Syntax: In schematic variable names, *any* symbol following

   \<^isub> or \<^isup> is now treated as part of the base name.  For

   example, the following works without printing of ugly ".0" indexes:

     lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1"

       by simp

 * Pure/Syntax: inner syntax includes (*(*nested*) comments*).

 * Pure/Syntax: pretty pinter now supports unbreakable blocks,

   specified in mixfix annotations as "(00...)".

 * Pure/Syntax: 'advanced' translation functions (parse_translation

   etc.) may depend on the signature of the theory context being

   presently used for parsing/printing, see also isar-ref manual.

 * Pure/Simplifier: you can control the depth to which conditional rewriting

   is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth Limit.

 * Pure/Simplifier: simplification procedures may now take the current

   simpset into account (cf. Simplifier.simproc(_i) / mk_simproc

   interface), which is very useful for calling the Simplifier

   recursively.  Minor INCOMPATIBILITY: the 'prems' argument of

   simprocs is gone -- use prems_of_ss on the simpset instead.

   Moreover, the low-level mk_simproc no longer applies Logic.varify

   internally, to allow for use in a context of fixed variables.

 * Isar debugging: new reference Toplevel.debug; default false.  Set to

   make printing of exceptions THM, TERM, TYPE and THEORY more verbose.

 * Locales: modifications regarding "includes"

   - "includes" disallowed in declaration of named locales (command "locale").

   - Fixed parameter management in theorem generation for goals with "includes".

     INCOMPATIBILITY: rarely, the generated theorem statement is different.

 * Locales: new context element "constrains" for adding type constraints

   to parameters.

 * Locales: context expressions permit optional syntax redeclaration when

   renaming parameters.

 * Locales: new commands for the interpretation of locale expressions

   in theories (interpretation) and proof contexts (interpret).  These take an

   instantiation of the locale parameters and compute proof obligations from

   the instantiated specification.  After the obligations have been discharged,

   the instantiated theorems of the locale are added to the theory or proof

   context.  Interpretation is smart in that already active interpretations

   do not occur in proof obligations, neither are instantiated theorems stored

   in duplicate.

   Use print_interps to inspect active interpretations of a particular locale.

   For details, see the Isar Reference manual.

 * Locales: INCOMPATIBILITY: experimental command "instantiate" has

   been withdrawn.  Use "interpret" instead.

 * Locales: proper static binding of attribute syntax -- i.e. types /

   terms / facts mentioned as arguments are always those of the locale

   definition context, independently of the context of later

   invocations.  Moreover, locale operations (renaming and type / term

   instantiation) are applied to attribute arguments as expected.

   INCOMPATIBILITY of the ML interface: always pass Attrib.src instead

   of actual attributes; rare situations may require Attrib.attribute

   to embed those attributes into Attrib.src that lack concrete syntax.

   Attribute implementations need to cooperate properly with the static

   binding mechanism.  Basic parsers Args.XXX_typ/term/prop and

   Attrib.XXX_thm etc. already do the right thing without further

   intervention.  Only unusual applications -- such as "where" or "of"

   (cf. src/Pure/Isar/attrib.ML), which process arguments depending

   both on the context and the facts involved -- may have to assign

   parsed values to argument tokens explicitly.

 * Attributes 'induct' and 'cases': type or set names may now be

   locally fixed variables as well.

 * Isar: new syntax 'name(i-j, i-, i, ...)' for referring to specific

   selections of theorems in named facts via indices.

 * Pure: reorganized bootstrapping of the Pure theories; CPure is now

   derived from Pure, which contains all common declarations already.

   Both theories are defined via plain Isabelle/Isar .thy files.

   INCOMPATIBILITY: elements of CPure (such as the CPure.intro /

   CPure.elim / CPure.dest attributes) now appear in the Pure name

   space; use isatool fixcpure to adapt your theory and ML sources.

   is peformed already.  Object-logics merely need to finish their

 is peformed already.  Object-logics merely need to finish their

   initial simpset configuration as before.

 initial simpset configuration as before.  INCOMPATIBILITY.

 *** Document preparation ***

 * Several new antiquotation:

   @{term_type term} prints a term with its type annotated;

   @{typeof term} prints the type of a term;

   @{const const} is the same as @{term const}, but checks

     that the argument is a known logical constant;

   @{term_style style term} and @{thm_style style thm} print a term or

     theorem applying a "style" to it

   Predefined styles are "lhs" and "rhs" printing the lhs/rhs of

   definitions, equations, inequations etc. and "conclusion" printing

   only the conclusion of a meta-logical statement theorem.  Styles may

   be defined via TermStyle.add_style in ML.  See the "LaTeX Sugar"

   document for more information.

 * Antiquotations now provide the option 'locale=NAME' to specify an

   alternative context used for evaluating and printing the subsequent

   argument, as in @{thm [locale=LC] fold_commute}, for example.

 * Commands 'display_drafts' and 'print_drafts' perform simple output

   of raw sources.  Only those symbols that do not require additional

   LaTeX packages (depending on comments in isabellesym.sty) are

   displayed properly, everything else is left verbatim.  We use

   isatool display and isatool print as front ends; these are subject

   to the DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively.

 * Proof scripts as well as some other commands such as ML or

   parse/print_translation can now be hidden in the document.  Hiding

   is enabled by default, and can be disabled either via the option '-H

   false' of isatool usedir or by resetting the reference variable

   IsarOutput.hide_commands. Additional commands to be hidden may be

   declared using IsarOutput.add_hidden_commands.

 * Datatype induction via method `induct' now preserves the name of the

 * Symbolic syntax of Hilbert Choice Operator is now as follows:

   induction variable. For example, when proving P(xs::'a list) by induction

   on xs, the induction step is now P(xs) ==> P(a#xs) rather than

   P(list) ==> P(a#list) as previously.

 * HOL/record: reimplementation of records. Improved scalability for

   records with many fields, avoiding performance problems for type

   inference. Records are no longer composed of nested field types, but

   of nested extension types. Therefore the record type only grows

   linear in the number of extensions and not in the number of fields.

   The top-level (users) view on records is preserved.  Potential

   INCOMPATIBILITY only in strange cases, where the theory depends on

   the old record representation. The type generated for a record is

   called <record_name>_ext_type.

 * HOL/record: Reference record_quick_and_dirty_sensitive can be

   enabled to skip the proofs triggered by a record definition or a

   simproc (if quick_and_dirty is enabled). Definitions of large

   records can take quite long.

 * HOL/record: "record_upd_simproc" for simplification of multiple

   record updates enabled by default.  Moreover, trivial updates are

   also removed: r(|x := x r|) = r.  INCOMPATIBILITY: old proofs break

   occasionally, since simplification is more powerful by default.

 * HOL: symbolic syntax of Hilbert Choice Operator is now as follows:

   The symbol \<some> is displayed as the alternative epsilon of LaTeX

 The symbol \<some> is displayed as the alternative epsilon of LaTeX

   and x-symbol; use option '-m epsilon' to get it actually printed.

 and x-symbol; use option '-m epsilon' to get it actually printed.

   Moreover, the mathematically important symbolic identifier

 Moreover, the mathematically important symbolic identifier \<epsilon>

   \<epsilon> becomes available as variable, constant etc.

 becomes available as variable, constant etc.  INCOMPATIBILITY,

 * HOL: "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".

 * "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".

   Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=

 Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=

   is \<ge>.

 is \<ge>.

 * HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}" (and similarly for

 * "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>"

   "\<in>" instead of ":").

 instead of ":".

 * HOL/SetInterval: The syntax for open intervals has changed:

 * theory SetInterval: changed the syntax for open intervals:

   Old         New

   Old       New

   {..n(}   -> {..<n}

   {..n(}    {..<n}

   {)n..}   -> {n<..}

   {)n..}    {n<..}

   {m..n(}  -> {m..<n}

   {m..n(}   {m..<n}

   {)m..n}  -> {m<..n}

   {)m..n}   {m<..n}

   {)m..n(} -> {m<..<n}

   {)m..n(}  {m<..<n}

   The old syntax is still supported but will disappear in the future.

 The old syntax is still supported but will disappear in the next

   For conversion use the following emacs search and replace patterns:

 release.  For conversion use the following Emacs search and replace

 patterns (these are not perfect but work quite well):

   They are not perfect but work quite well.

 * theory Finite_Set: changed the syntax for 'setsum', summation over

 finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is

 * HOL: The syntax for 'setsum', summation over finite sets, has changed:

 now either "SUM x:A. e" or "\<Sum>x \<in> A. e".

   The syntax for 'setsum (%x. e) A' used to be '\<Sum>x:A. e'

 Some new syntax forms are available:

   and is now either 'SUM x:A. e' or '\<Sum>x\<in>A. e'.

   "\<Sum>x | P. e"      for     "setsum (%x. e) {x. P}"

   There is new syntax for summation over finite sets:

   "\<Sum>x = a..b. e"   for     "setsum (%x. e) {a..b}"

   "\<Sum>x = a..<b. e"  for     "setsum (%x. e) {a..<b}"

   '\<Sum>x | P. e'    is the same as  'setsum (%x. e) {x. P}'

   "\<Sum>x < k. e"      for     "setsum (%x. e) {..<k}"

   '\<Sum>x=a..b. e'   is the same as  'setsum (%x. e) {a..b}'

   '\<Sum>x=a..<b. e'  is the same as  'setsum (%x. e) {a..<b}'

 The latter form "\<Sum>x < k. e" used to be based on a separate

   '\<Sum>x<k. e'      is the same as  'setsum (%x. e) {..<k}'

 function "Summation", which has been discontinued.

   Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e'

 * theory Finite_Set: in structured induction proofs, the insert case

   now translates into 'setsum' as above.

 is now 'case (insert x F)' instead of the old counterintuitive 'case

 (insert F x)'.

 * HOL: Finite set induction: In Isar proofs, the insert case is now

   "case (insert x F)" instead of the old counterintuitive "case (insert F x)".

 * The 'refute' command has been extended to support a much larger

 fragment of HOL, including axiomatic type classes, constdefs and

 * HOL/Simplifier:

 typedefs, inductive datatypes and recursion.

   - Is now set up to reason about transitivity chains involving "trancl"

 * Datatype induction via method 'induct' now preserves the name of the

   (r^+) and "rtrancl" (r^*) by setting up tactics provided by

 induction variable. For example, when proving P(xs::'a list) by

   Provers/trancl.ML as additional solvers.  INCOMPATIBILITY: old proofs break

 induction on xs, the induction step is now P(xs) ==> P(a#xs) rather

   occasionally as simplification may now solve more goals than previously.

 than P(list) ==> P(a#list) as previously.  Potential INCOMPATIBILITY

 in unstructured proof scripts.

   - Converts x <= y into x = y if assumption y <= x is present.  Works for

   all partial orders (class "order"), in particular numbers and sets. For

 * Reworked implementation of records.  Improved scalability for

   linear orders (e.g. numbers) it treats ~ x < y just like y <= x.

 records with many fields, avoiding performance problems for type

 inference. Records are no longer composed of nested field types, but

   - Simproc for "let x = a in f x"

 of nested extension types. Therefore the record type only grows linear

   If a is a free or bound variable or a constant then the let is unfolded.

 in the number of extensions and not in the number of fields.  The

   Otherwise first a is simplified to a', and then f a' is simplified to

 top-level (users) view on records is preserved.  Potential

   g. If possible we abstract a' from g arriving at "let x = a' in g' x",

 INCOMPATIBILITY only in strange cases, where the theory depends on the

   otherwise we unfold the let and arrive at g. The simproc can be 

 old record representation. The type generated for a record is called

   enabled/disabled by the reference use_let_simproc. Potential

 <record_name>_ext_type.

   INCOMPATIBILITY since simplification is more powerful by default.

 Flag record_quick_and_dirty_sensitive can be enabled to skip the

 * HOL: The 'refute' command has been extended to support a much larger

 proofs triggered by a record definition or a simproc (if

   fragment of HOL, including axiomatic type classes, constdefs and typedefs,

 quick_and_dirty is enabled).  Definitions of large records can take

   inductive datatypes and recursion.

 quite long.

 New simproc record_upd_simproc for simplification of multiple record

 updates enabled by default.  Moreover, trivial updates are also

 removed: r(|x := x r|) = r.  INCOMPATIBILITY: old proofs break

 occasionally, since simplification is more powerful by default.

 * Simplifier: automatically reasons about transitivity chains

 involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics

 provided by Provers/trancl.ML as additional solvers.  INCOMPATIBILITY:

 old proofs break occasionally as simplification may now solve more

 goals than previously.

 * Simplifier: converts x <= y into x = y if assumption y <= x is

 present.  Works for all partial orders (class "order"), in particular

 numbers and sets.  For linear orders (e.g. numbers) it treats ~ x < y

 just like y <= x.

 * Simplifier: new simproc for "let x = a in f x".  If a is a free or

 bound variable or a constant then the let is unfolded.  Otherwise

 first a is simplified to b, and then f b is simplified to g. If

 possible we abstract b from g arriving at "let x = b in h x",

 otherwise we unfold the let and arrive at g.  The simproc can be

 enabled/disabled by the reference use_let_simproc.  Potential

 INCOMPATIBILITY since simplification is more powerful by default.

   support continuous functions) in favor of the general Pure one with

 support continuous functions) in favor of the general Pure one with

   full type-inference.

 full type-inference.

 * ZF/ex/{Group,Ring}: examples in abstract algebra, including the

 * ZF/ex: theories Group and Ring provide examples in abstract algebra,

   First Isomorphism Theorem (on quotienting by the kernel of a

 including the First Isomorphism Theorem (on quotienting by the kernel

   homomorphism).

 of a homomorphism).

   makes use of TC rules declared to Isar proof contexts (or locales);

 makes use of TC rules declared to Isar proof contexts (or locales);

   the old version is still required for ML proof scripts.

 the old version is still required for ML proof scripts.

 *** System ***

 * Allow symlinks to all proper Isabelle executables (Isabelle,

   isabelle, isatool etc.).

 * isabelle-process: Poly/ML no longer needs Perl to run an interactive

   session.

 * ISABELLE_DOC_FORMAT setting specifies preferred document format (for

   isatool doc, isatool mkdir, display_drafts etc.).

 * isatool usedir: option -f allows specification of the ML file to be

   used by Isabelle; default is ROOT.ML.

 * HOL: isatool dimacs2hol converts files in DIMACS CNF format

   (containing Boolean satisfiability problems) into Isabelle/HOL

   theories.

   that of the SML basis, which has constructors NONE and SOME instead

 that of the SML basis, which has constructors NONE and SOME instead of

   of None and Some, as well as exception Option.Option instead of

 None and Some, as well as exception Option.Option instead of OPTION.

   OPTION.  The functions the, if_none, is_some, is_none have been

 The functions the, if_none, is_some, is_none have been adapted

   adapted accordingly, while Option.map replaces apsome.

 accordingly, while Option.map replaces apsome.

   exceptions Empty and Subscript, as well as Library.UnequalLengths.

 exceptions Empty and Subscript, as well as Library.UnequalLengths.

   Function like Library.hd and Library.tl are superceded by the

 Function like Library.hd and Library.tl are superceded by the standard

   standard hd and tl functions etc.

 hd and tl functions etc.

   A number of basic functions are now no longer exported to the ML

 A number of basic functions are now no longer exported to the ML

   toplevel, as they are variants of standard functions.  The following

 toplevel, as they are variants of standard functions.  The following

   suggests how one can translate existing code:

 suggests how one can translate existing code:

     seq fs = app fs

     seq fs = List.app fs

   etc. is now passed through Output.output, with a hook for arbitrary

 etc. is now passed through Output.output, with a hook for arbitrary

   transformations depending on the print_mode (cf. Output.add_mode --

 transformations depending on the print_mode (cf. Output.add_mode --

   the first active mode that provides a output function wins).

 the first active mode that provides a output function wins).  Already

   Already formatted output may be embedded into further text via

 formatted output may be embedded into further text via Output.raw; the

   Output.raw; the result of Pretty.string_of/str_of and derived

 result of Pretty.string_of/str_of and derived functions

   functions (string_of_term/cterm/thm etc.) is already marked raw to

 (string_of_term/cterm/thm etc.) is already marked raw to accommodate

   accommodate easy composition of diagnostic messages etc.

 easy composition of diagnostic messages etc.  Programmers rarely need

   Programmers rarely need to care about Output.output or Output.raw at

 to care about Output.output or Output.raw at all, with some notable

   all, with some notable exceptions: Output.output is required when

 exceptions: Output.output is required when bypassing the standard

   bypassing the standard channels (writeln etc.), or in token

 channels (writeln etc.), or in token translations to produce properly

   translations to produce properly formatted results; Output.raw is

 formatted results; Output.raw is required when capturing already

   required when capturing already output material that will eventually

 output material that will eventually be presented to the user a second

   be presented to the user a second time.  For the default print mode,

 time.  For the default print mode, both Output.output and Output.raw

   both Output.output and Output.raw have no effect.

 have no effect.

 * Pure: print_tac now outputs the goal through the trace channel.

 * Isar debugging: new reference Toplevel.debug; default false.  Set to

 make printing of exceptions THM, TERM, TYPE and THEORY more verbose.

   internal interfaces -- INCOMPATIBILITY.  Renamed cond_extern(_table)

 internal interfaces -- INCOMPATIBILITY.  Renamed cond_extern(_table)

   to extern(_table).  The plain name entry path is superceded by a

 to extern(_table).  The plain name entry path is superceded by a

   general 'naming' context, which also includes the 'policy' to

 general 'naming' context, which also includes the 'policy' to produce

   produce a fully qualified name and external accesses of a fully

 a fully qualified name and external accesses of a fully qualified

   qualified name; NameSpace.extend is superceded by context dependent

 name; NameSpace.extend is superceded by context dependent

   Sign.declare_name.  Several theory and proof context operations

 Sign.declare_name.  Several theory and proof context operations modify

   modify the naming context.  Especially note Theory.restore_naming

 the naming context.  Especially note Theory.restore_naming and

   and ProofContext.restore_naming to get back to a sane state; note

 ProofContext.restore_naming to get back to a sane state; note that

   that Theory.add_path is no longer sufficient to recover from

 Theory.add_path is no longer sufficient to recover from

   Theory.absolute_path in particular.

 Theory.absolute_path in particular.

 * Pure: new flags short_names (default false) and unique_names

 (default true) for controlling output of qualified names.  If

 short_names is set, names are printed unqualified.  If unique_names is

 reset, the name prefix is reduced to the minimum required to achieve

 the original result when interning again, even if there is an overlap

 with earlier declarations.

   means to remove case bindings -- INCOMPATIBILITY in

 means to remove case bindings -- INCOMPATIBILITY in

   (RAW_)METHOD_CASES.

 (RAW_)METHOD_CASES.

   dependent plug-ins (simprocs, solvers, wrappers etc.).  These extra

 dependent plug-ins (simprocs, solvers, wrappers etc.).  These extra

   components are stored in the theory and patched into the

 components are stored in the theory and patched into the

   simpset/claset when used in an Isar proof context.  Context

 simpset/claset when used in an Isar proof context.  Context dependent

   dependent components are maintained by the following theory

 components are maintained by the following theory operations:

   operations:

   Simplifier.add_context_simprocs

     Simplifier.add_context_simprocs

   Simplifier.del_context_simprocs

     Simplifier.del_context_simprocs

   Simplifier.set_context_subgoaler

     Simplifier.set_context_subgoaler

   Simplifier.reset_context_subgoaler

     Simplifier.reset_context_subgoaler

   Simplifier.add_context_looper

     Simplifier.add_context_looper

   Simplifier.del_context_looper

     Simplifier.del_context_looper

   Simplifier.add_context_unsafe_solver

     Simplifier.add_context_unsafe_solver

   Simplifier.add_context_safe_solver

     Simplifier.add_context_safe_solver

   Classical.add_context_safe_wrapper

     Classical.add_context_safe_wrapper

   Classical.del_context_safe_wrapper

     Classical.del_context_safe_wrapper

   Classical.add_context_unsafe_wrapper

     Classical.add_context_unsafe_wrapper

   Classical.del_context_unsafe_wrapper

     Classical.del_context_unsafe_wrapper

 IMPORTANT NOTE: proof tools (methods etc.) need to use

   IMPORTANT NOTE: proof tools (methods etc.) need to use

 local_simpset_of and local_claset_of to instead of the primitive

   local_simpset_of and local_claset_of to instead of the primitive

 Simplifier.get_local_simpset and Classical.get_local_claset,

   Simplifier.get_local_simpset and Classical.get_local_claset,

 respectively, in order to see the context dependent fields!

   respectively, in order to see the context dependent fields!

 *** System ***

 * Allow symlinks to all proper Isabelle executables (Isabelle,

 isabelle, isatool etc.).

 * ISABELLE_DOC_FORMAT setting specifies preferred document format (for

 isatool doc, isatool mkdir, display_drafts etc.).

 * isatool usedir: option -f allows specification of the ML file to be

 used by Isabelle; default is ROOT.ML.

 * HOL: isatool dimacs2hol converts files in DIMACS CNF format

 (containing Boolean satisfiability problems) into Isabelle/HOL

 theories.