* Theorems about complex numbers are now stated only using Re and Im, the
Complex
constructor is not used anymore. It is possible to use primcorec to defined
the
behaviour of a complex-valued function.
Removed theorems about the Complex constructor from the simpset, they are
available
On Mon, 5 May 2014, Makarius wrote:
Users running on batteries might also want a mode that restricts all
threads to the behaviour above.
Have you tried that with threads = 1 (there is also a special treatment for
high-priority prints in that mode)? So far I guess that most people run with
On Fri, 2 May 2014, Makarius wrote:
On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
text ‹
@{term ‹A \un B›}
›
Here the \un works as expected -- the cartouche remains intact
independently of its
content, as long as the funny parentheses are nested properly.
But this
* More general Query panel supersedes Find panel, with GUI access
to commands 'find_theorems' and 'find_consts', as well as print
operations for the context. Minor incompatibility in keyboard
shortcuts etc.: replace action isabelle-find by isabelle-query.
This refers to Isabelle/ee2b61f37ad9.
* Search field for all output panels (Output, Query, Info etc.)
to highlight text via regular expression.
This refers to Isabelle/2f73ef9eb272, the implementation is mostly just
38c6b70e5e53, which is notable for its simplicity.
The search factility was in the pipeline several years, mainly
On Thu, 1 May 2014, boeh...@in.tum.de wrote:
* New internal SAT solver dpll_p that produces models and proof traces.
This refers to Isabelle/848d507584db. The added SAT solver should be more
efficient than the internal SAT solvers dpll and enumerate. Since the
solver dpll_p produces proof
* Support for path completion within the formal text, based on
file-system content.
This refers to Isabelle/b2bfcd8cda80. It is relevant e.g. for document
antiquotation @{file} or the arguments of so-called load commands in the
theory, such as 'ML_File', 'SML_File'.
The completion
* Improved Console/Scala plugin: more uniform scala.Console output,
more robust treatment of threads and interrupts.
This refers to Isabelle/477cd67f963f.
I have standardized Isabelle/Scala towards scala.Console, with
Output.writeln, Output.warning, Output.error_message using that as well.
On Wed, 7 May 2014, Johannes Hölzl wrote:
* Theorems about complex numbers are now stated only using Re and Im, the
Complex
constructor is not used anymore. It is possible to use primcorec to defined the
behaviour of a complex-valued function.
This is also a surprising application of
