*** Document preparation ***
* Document headings work uniformly via the commands 'chapter',
'section', 'subsection', 'subsubsection' -- in any context, even
before the initial 'theory' command. Obsolete proof commands 'sect',
'subsect', 'subsubsect' have been discontinued. The Obsolete
Isabelle/ML has antiquotations as some kind of macro language. It can
do certain things better than the C preprocessor, although one always
needs to be careful to stay within reason.
How about this?
ap2 f (x, y) = (f x, f y)
@{ap n} f (x1, ..., xn) = (f x1, ..., f xn)
Maybe even
Dear all,
How about this?
ap2 f (x, y) = (f x, f y)
@{ap n} f (x1, ..., xn) = (f x1, ..., f xn)
@{ap n} sounds reasonable to me, however, due to the presence of apfst and
apsnd one might
think about adding an all to indicate that the function is applied to all
element. So what about
On Wed, 8 Oct 2014, Makarius wrote:
*** ML ***
* Basic combinators map, fold, fold_map, split_list are available as
parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
There was an off-list proposal by René Thiemann to define the following
antiquotation:
@{map_tuple n}
* Library/Sum_of_Squares: simplified and improved sos method. Always
use local CSDP executable, which is much faster than the NEOS server.
The sos_cert functionality is invoked as sos with additional
argument. Minor INCOMPATIBILITY.
This refers to Isabelle/71cdb885b3bb. It is a general brush-up
*** ML ***
* Basic combinators map, fold, fold_map, split_list are available as
parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
This refers to Isabelle/9f10d82e8188.
After seeing another split_list42 combinator, I could not resist to make a
fully general solution once
I have no opinion wrt PG but just don't let your update tool lose on the whole
distribution because there are some files of mine where that would create
discrepancies in the text.
Tobias
On 08/10/2014 00:25, Makarius wrote:
*** System ***
* The Isabelle tool update_cartouches changes theory
*** System ***
* The Isabelle tool update_cartouches changes theory files to use
cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
This refers to Isabelle/fffdbce036db. In the subsequent changesets, I
have modernized a few of my own hotspots accordingly, but refrained
On Thu, 2 Oct 2014, Florian Haftmann wrote:
We have a tradition not to change NEWS after release, but maybe we
should break this rule and consolidate the following accidents (3 times
only):
INCOMPATBILITY
INCOMPATIBILTY
to
INCOMPATIBILITY
This might seem ridiculous in the first instance,
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Support for BibTeX files: context menu, context-sensitive token
marker, SideKick parser.
* Document antiquotation @{cite} provides formal markup, which is
interpreted semi-formally based on .bib files that happen to be opened
in the editor
We have a tradition not to change NEWS after release, but maybe we
should break this rule and consolidate the following accidents (3 times
only):
INCOMPATBILITY
INCOMPATIBILTY
to
INCOMPATIBILITY
This might seem ridiculous in the first instance, but when using
andeditor with a context-sensitive
I can’t think of any reason to avoid correcting errors of any sort in the NEWS
file.
Larry
On 2 Oct 2014, at 16:55, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
We have a tradition not to change NEWS after release, but maybe we
should break this rule and consolidate
The situation involving ZF can go either way, as there are hardly any users.
How are negative integers written in ZF now? Can one still write #-3 or is it
$- #3?
The first one. Numerals in ZF are left as they are, *signed*.
Florian
--
PGP available:
On Sun, 21 Sep 2014, Florian Haftmann wrote:
a) Currently, the prefix for (signed!) ZF numerals is »#«. Since
operations for integers in ZF are mainly associated with »$« (e.g., »_
$+ _«, »_ $* _«), maybe it would be more consistent to prefer »$« also
here. As far as I understand from the
On Mon, 22 Sep 2014, Makarius wrote:
Looking once again at ZF xnum syntax, I think it can be expressed
without the xnum token, and without any syntax change for now -- that
may be reconsidered independently.
See now:
changeset: 58420:37cbbd8eb460
user:wenzelm
date:Mon Sep
After realising that HOL and ZF numerals are already separate lexical
categories (though the history of this being so ist not clear to me at
the moment), I finally took the adventure of turning HOL numerals into
unsigned numerals also lexically (logically, this has already been the
case for a long
On 21/09/2014 17:04, Florian Haftmann wrote:
After realising that HOL and ZF numerals are already separate lexical
categories (though the history of this being so ist not clear to me at the
moment), I finally took the adventure of turning HOL numerals into unsigned
numerals also lexically
Florian showed it to me and class_deps has become really usable. I recommend
it to anyone out there in the class jungle.
Tobias
On 10/09/2014 10:49, Florian Haftmann wrote:
* Command class_deps takes optional sort arguments constraining the
search space.
This refers to be1d10595b7b.
* Old and new SMT modules:
- The old 'smt' method has been renamed 'old_smt' and moved to
'src/HOL/Library/Old_SMT.thy'. It provided for compatibility, until
applications have been ported to use the new 'smt' method. For the
method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0)
On Wed, 21 May 2014, Lars Noschinski wrote:
The other thing I noticed during the last days was the following: When I
modify a term, I usually place the term at the position where I want to
insert something (which is often directly before a variable or
constant), start typing and only add the
* Former isabelle tty has been superseded by isabelle console,
with implicit build like isabelle jedit, and without the mostly
obsolete Isar TTY loop.
This refers to Isabelle/0e41f26a0250. Recently, I've found myself more
often doing an 'exit' of the Isar loop of isabelle tty instead of
* Proof General with its traditional helper scripts is now an optional
Isabelle component, e.g. ProofGeneral-4.2-2 from the Isabelle
component repository http://isabelle.in.tum.de/components/. See also
the system manual for general explanations about add-on components,
notably those that are not
* Updated and extended manuals: codegen, datatypes, implementation,
jedit, system.
This refers to Isabelle/96f970d1522b.
The list of updated manuals is based on a quick glance over the repository
changes, and may be incomplete. Maybe the maintainers of manuals want to
check if it makes
- MaSh and MeSh are now used by default together with the traditional
MePo (Meng-Paulson) relevance filter. To disable MaSh, set the MaSh
system option in Plugin Options / Isabelle / General to none. Other
allowed values include sml (for the default SML engine) and py
- MaSh and MeSh are now used by default together with the traditional
MePo (Meng-Paulson) relevance filter. To disable MaSh, set the MaSh
system option in Plugin Options / Isabelle / General to none. Other
allowed values include sml (for the default SML engine) and py
* Windows: support for regular TeX installation (e.g. MiKTeX) instead
of TeX Live from Cygwin.
This refers to Isabelle/bf5ddf4ec64b. In the coming release there will be
just a link to some regular MiKTeX download site like
http://www.ctan.org/tex-archive/systems/win32/miktex -- no longer any
On 12.05.2014 14:26, Makarius wrote:
* Improved management of dockable windows: clarified keyboard focus
and window placement wrt. main editor view; optional menu item to
Detach a copy where this makes sense.
I've started using the Detach functionality quite a bit during the
last week. A few
On 31.03.2014 22:04, Makarius wrote:
- Syntax completion of the editor and semantic completion of the
prover are merged. Since the latter requires a full round-trip of
document update to arrive, the default for option
jedit_completion_delay has been changed to 0.5s to improve
On 31.03.2014 22:04, Makarius wrote:
These cumulative NEWS refer to Isabelle/075397022503. This also marks
the point where my continously shrinking and growing TODO list has
reached a stable state concerning completion and the main activity
on this part is finished for now.
I have recently
On Wed, 21 May 2014, Lars Noschinski wrote:
* At least for the output window, I'd like to see a more direct to
to detach a window than the context menu.
I was thinking of that, when making that change, but did not find a
solution yet. The general idea is that there are some common
On Wed, 21 May 2014, Lars Noschinski wrote:
* The fact that a detached window stays on top of the jEdit window
is often quite nice.
* On GNOME 3.8, the detached (and floating instance) windows
do not have the usual close button, nor can they be maximized
(resizing is possible,
On Wed, 21 May 2014, Lars Noschinski wrote:
* Sometimes, I use a detached window to see the proof state at a
certain position in my theory, regardless on where my cursor is.
If I successfully changed (i.e. not in between) some lemmas before,
I want to see the updated proof state at
On Wed, 21 May 2014, Lars Noschinski wrote:
I have recently written some proof with some german plain text. This
triggered a lot of completion popups, suggesting to correct german to
english words (which is to be expected). Unfortunately, the completion
popup does not disappear when I
On Wed, 21 May 2014, Makarius wrote:
Concerning the missing German dictionary: it is easy to include additional
dictionaries as plain word lists. Users can do that via JORTHO_DICTIONARIES
in the settings environment.
Actually, I have forgotten an important detail: German uses capitalization
Am Sonntag, den 11.05.2014, 04:55 -0700 schrieb Andrei Popescu:
Johannes 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.
it’s not just about syntactic sugar. It seems to me that the complex numbers
are an elegant (if degenerative) example of a co-algebraic datatype. The
co-recursive definitions look absolutely natural to me.
Larry
On 11 May 2014, at 12:55, Andrei Popescu uuo...@yahoo.com wrote:
The fact that
Yes, but the underlying reason for that is that complex numbers are
isomorphic to pairs of real numbers, and binary product types are
degenerate (I would rather say very basic) co-algebraic datatypes.
So my point (and I would guess Andrei's as well) is that this really has
nothing to do with
Am 13.05.2014 um 14:11 schrieb Manuel Eberl ebe...@in.tum.de:
In particular, any algebraic datatype with only one constructor can be
rewritten into a corresponding codatatype, allowing you to use primcorec for
it.
In fact, even (nonrecursive) datatypes with several constructors can be
are.
Andrei
On Tue, 5/13/14, Lawrence Paulson l...@cam.ac.uk wrote:
Subject: Re: [isabelle-dev] NEWS: avoid the Complex constructor, use the more
natural
To: Andrei Popescu uuo...@yahoo.com
Cc: isabelle-dev@mailbroy.informatik.tu-muenchen.de
isabelle-dev
On Mon, 12 May 2014, Tjark Weber wrote:
On Fri, 2014-05-09 at 12:00 +0200, Tjark Weber wrote:
Moreover, it is merely a historic accident that the theory is based on
Refute. [...]
I am attaching a patch that replaces Refute with Nitpick in
HOL/ex/Sudoku.thy.
Thanks. I have pushed this as
* Improved management of dockable windows: clarified keyboard focus
and window placement wrt. main editor view; optional menu item to
Detach a copy where this makes sense.
This refers to Isabelle/c2ddbf327bbd.
After the docking framework of jEdit came up again in recent discussions
on this
Johannes 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.
Makarius wrote:
That is indeed very nice. Is that a new invention or
Makarius,
On Fri, 2014-05-09 at 12:00 +0200, Tjark Weber wrote:
Moreover, it is merely a historic accident that the theory is based on
Refute. [...]
I am attaching a patch that replaces Refute with Nitpick in
HOL/ex/Sudoku.thy.
Best,
Tjark
# HG changeset patch
# User webertj
# Date
Hallo,
I stumbled across this just now and thought about it for a bit. I don't
know much about category theory, but I would say the intuitive “reason”
why complex numbers can be represented this way is the following:
1. ℂ is a field extension of ℝ with degree 2 (since it is constructed
from the
On Wed, 2014-05-07 at 15:41 +0200, Makarius wrote:
How about ~~/src/HOL/ex/Sudoko.thy? It formally depends on ZCHAFF_HOME,
so it is rarely run in practice. Does it now make sense to remove that
condition in the ROOT file? What is tested in this theory anyway? The
'refute' / 'oops'
* 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
* 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
On Tue, 22 Apr 2014, Makarius wrote:
So if nothing happens in between, I will convert all Isabelle + AFP ROOT
files systematically at the end of this week.
After some canonical delays, this is now in Isabelle/23883e1879c5 and
AFP/23883e1879c5. I have also updated the isabelle mkroot tool to
Most useful! For fun I tried it on a text that has been read by many people and
it found another typo :-)
Thanks a lot for this
Tobias
On 14/04/2014 11:31, Makarius wrote:
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Spell-checker support for document text, comments etc.
This refers to
On Fri, 11 Apr 2014, Makarius wrote:
* Session ROOT specifications support explicit 'document_files' for
robust dependencies on LaTeX sources. Only these explicitly given
files are copied to the document output directory, before document
processing is started.
This refers to
On Tue, 25 Mar 2014, Makarius wrote:
* Command 'SML_file' reads and evaluates the given Standard ML file.
Toplevel bindings are stored within the theory context; the initial
environment is restricted to the Standard ML implementation of
Poly/ML, without the add-ons of Isabelle/ML. See also
On Tue, 15 Apr 2014, Lars Noschinski wrote:
Where C+b is bound to Complete Isabelle text, I assume (following the
repository versions, it was still Complete Word for me).
Yes. Keyboard defaults cannot be pushed on people hanging on the
repository: jEdit turns the centrally given properties
On 31.03.2014 22:04, Makarius wrote:
I played a bit around with your new completion setup.
- Support for semantic completion based on failed name space lookup.
The error produced by the prover contains information about
alternative names that are accessible in a particular position.
On Mon, 14 Apr 2014, Makarius wrote:
The present Isabelle component jortho-1.0-1 bundles the very good
English dictionaries from http://wordlist.sourceforge.net/ which are
also used in GNU Aspell, Hunspell (Open Office, Firefox) etc. I might
need to revisit that again, to make sure that the
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Spell-checker support for document text, comments etc.
This refers to Isabelle/282f3b06fa86.
Spell-checker support was one of the many missing bits over the years.
Last Friday afternoon I intended to spend a few hours to integrate one of
the
On Sun, 13 Apr 2014, Tobias Nipkow wrote:
That works fine, thank you.
Tobias
On 11/04/2014 23:52, Makarius wrote:
On Fri, 11 Apr 2014, Tobias Nipkow wrote:
What I sometimes need is to have the latex files generated but not processed.
Currently I achieve this with a dummy root.tex file that
That works fine, thank you.
Tobias
On 11/04/2014 23:52, Makarius wrote:
On Fri, 11 Apr 2014, Tobias Nipkow wrote:
What I sometimes need is to have the latex files generated but not processed.
Currently I achieve this with a dummy root.tex file that includes nothing. Is
there a less dummy
* Session ROOT specifications support explicit 'document_files' for
robust dependencies on LaTeX sources. Only these explicitly given
files are copied to the document output directory, before document
processing is started.
This refers to Isabelle/cd8b6d849b6a. That changeset also contains
On Fri, 11 Apr 2014, Tobias Nipkow wrote:
What I sometimes need is to have the latex files generated but not
processed. Currently I achieve this with a dummy root.tex file that
includes nothing. Is there a less dummy way?
There is no need for root.tex and latex to produce a dummy root.pdf.
* More support for remote files (e.g. http) using standard Java
networking operations instead of jEdit virtual file-systems.
This refers to Isabelle/aed94b61f65b. Both theories and aux. files should
now work via http, but the latter need to be retrieved manually, e.g. by
C-hover-click on the
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Support for Navigator plugin, with toolbar buttons and keyboard
shortcuts similar to major web browsers.
This refers to Isabelle/f0592485b7fb.
The jEdit Navigator plugin was very primitive some years ago, when I first
checked it. In the meantime
On 07.04.2014 15:16, Makarius wrote:
Note that keyboard shortcuts similar to major web browsers refers to
A-LEFT and A-RIGHT on Windows and Linux. On Mac OS X, that would be
Control-LEFT and Control-RIGHT, but it is neither a standard browser
key sequence, nor does it usually work at all, due
*** System ***
* The raw Isabelle process executable has been renamed from
isabelle-process to isabelle_process, which conforms to common
shell naming conventions, and allows to define a shell function within
the Isabelle environment to avoid dynamic path lookup. Rare
incompatibility for old
On Mon, 7 Apr 2014, Lars Noschinski wrote:
On 07.04.2014 15:16, Makarius wrote:
Note that keyboard shortcuts similar to major web browsers refers to
A-LEFT and A-RIGHT on Windows and Linux. On Mac OS X, that would be
Control-LEFT and Control-RIGHT, but it is neither a standard browser
key
On 07.04.2014 15:40, Makarius wrote:
I do check for jEdit keymap conflicts routinely, since this is not
ESCAPE-META-ALT-CONTROL-SHIFT with an infinite space of possibilities.
There is indeed an overlap with actions called shift-left (Sift
Indent Left) and shift-right (Shift Indent Right), but
On Mon, 7 Apr 2014, Lars Noschinski wrote:
On 07.04.2014 15:40, Makarius wrote:
I do check for jEdit keymap conflicts routinely, since this is not
ESCAPE-META-ALT-CONTROL-SHIFT with an infinite space of possibilities.
There is indeed an overlap with actions called shift-left (Sift
Indent Left)
* ML antiquotation @{print} inlines a function to print an arbitrary
ML value, which is occasionally useful for diagnostic or demonstration
purposes.
This refers to Isabelle/386e4cb7ad68, which also points to the place where
the older antiquotation @{make_string} is documented.
Despite these
So what should I use before antiquotations are available? Should I still avoid
PolyML.makestring?
Makarius makar...@sketis.net schrieb:
* ML antiquotation @{print} inlines a function to print an arbitrary
ML value, which is occasionally useful for diagnostic or demonstration
purposes.
This
On Fri, 4 Apr 2014, Lars Noschinski wrote:
So what should I use before antiquotations are available? Should I still
avoid PolyML.makestring?
All the documentation etc. is about Isabelle/ML user space, after Pure.thy
is available.
For Isabelle/Pure bootstrap different rules apply -- quite
Am 31.03.2014 23:14, schrieb Makarius:
On Fri, 28 Feb 2014, Makarius wrote:
I've made another round of refinements (presently at
Isabelle/f7ceebe2f1b5). There were some situations where the change
propagation of blobs (auxiliary files) versus theories was not right,
leading to an invalid
On Tue, 25 Mar 2014, Makarius wrote:
* Command 'SML_file' reads and evaluates the given Standard ML file.
Toplevel bindings are stored within the theory context; the initial
environment is restricted to the Standard ML implementation of
Poly/ML, without the add-ons of Isabelle/ML. See also
On 31.03.2014 16:04, Makarius wrote:
What we have here is the Isabelle Prover IDE technology used for
something that is not Isabelle, namely official Standard ML. It is
just a coincidence that it runs within the same Poly/ML runtime system
-- there is no direct connection to the Isabelle/ML
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Improved syntactic and semantic completion mechanism:
- No completion for Isar keywords that have already been recognized
by the prover, e.g. : within accepted Isar syntax looses its
meaning as abbreviation for symbol \in.
- Completion
On Fri, 28 Feb 2014, Makarius wrote:
I've made another round of refinements (presently at Isabelle/f7ceebe2f1b5).
There were some situations where the change propagation of blobs (auxiliary
files) versus theories was not right, leading to an invalid perspective of
the latter, and causing it
* Command 'SML_file' reads and evaluates the given Standard ML file.
Toplevel bindings are stored within the theory context; the initial
environment is restricted to the Standard ML implementation of
Poly/ML, without the add-ons of Isabelle/ML. See also
~/src/Tools/SML/Examples.thy for some
On Fri, 28 Feb 2014, Christian Sternagel wrote:
Dear Lars,
today I first tried using the new simplifier tracing facility (within
Isabelle/jEdit). I just started but have already some questions ;)
I am still delayed elsewhere, but before we enter the hot phase of the
summer release, we
* Basic constants of Pure use more conventional names and are always
qualified. Rare INCOMPATIBILITY, but with potentially serious
consequences, notably for tools in Isabelle/ML. The following
renaming needs to be applied:
== ~ Pure.eq
==~ Pure.imp
all
* Removed and renamed theorems in Series:
summable_le ~ suminf_le
suminf_le ~ suminf_le_const
series_pos_le ~ setsum_le_suminf
series_pos_less ~ setsum_less_suminf
suminf_ge_zero ~ suminf_nonneg
suminf_gt_zero ~ suminf_pos
Hi Chris,
In the Simplifier Trace panel itself I did not find out how to get
any output. Only after pressing the Show Trace button a new window
opens that contains the output.
yes, this is working as intended. The panel itself only shows
interactive questions to the user, and by default,
Dear Lars,
today I first tried using the new simplifier tracing facility (within
Isabelle/jEdit). I just started but have already some questions ;)
In the Simplifier Trace panel itself I did not find out how to get any
output. Only after pressing the Show Trace button a new window opens
I've made another round of refinements (presently at
Isabelle/f7ceebe2f1b5). There were some situations where the change
propagation of blobs (auxiliary files) versus theories was not right,
leading to an invalid perspective of the latter, and causing it to be
rechecked to the bottom whenever
On Mon, 24 Feb 2014, Lawrence Paulson wrote:
What I’d love to see is completion of theorem names...
Definitely. I continue to work through the sediments, to expose the
required markup information.
In Isabelle/e5128a9c4311 proof methods already work. Next will be
attributes and facts, but
On Fri, 21 Feb 2014, Makarius wrote:
* Improved completion based on context information about embedded
languages: keywords are only completed for outer syntax, symbols for
languages that support them. E.g. no symbol completion for ML source,
but within ML strings, comments, antiquotations.
Referring to e99ed112d303:
* Code generator: minimize exported identifiers by default.
This is definitely a non-trivial bussiness, and still might exhibit
deficiencies.
Note that the previous behaviour can be restored using »open« as follows:
export_code open c …
Florian
--
* Improved completion based on context information about embedded
languages: keywords are only completed for outer syntax, symbols for
languages that support them. E.g. no symbol completion for ML source,
but within ML strings, comments, antiquotations.
This refers to Isabelle/5ff4742f27ec.
Hi Makarius,
Am 17.02.2014 14:14, schrieb Makarius:
* Improved support for Isabelle/ML, with jEdit mode isabelle-ml for
auxiliary ML files.
This refers to Isabelle/56ebc4d4d008. It continues recent
improvements of auxiliary file support.
The IDE support for Isabelle/ML is already quite
On 18.02.2014 17:36, Dmitriy Traytel wrote:
However, once I had to restart Isabelle as JEdit became quite
irresponsive (using almost 4GB of memory, forced GC didn't help).
Maybe I just hat too many ML files open (I usually don't close them
once opened) or my ML files are just too big: e.g.
* Improved support for Isabelle/ML, with jEdit mode isabelle-ml for
auxiliary ML files.
This refers to Isabelle/56ebc4d4d008. It continues recent improvements of
auxiliary file support.
The IDE support for Isabelle/ML is already quite substantial, but with
every step forward, I get 5 new
On Sat, 1 Feb 2014, Peter Lammich wrote:
by (auto ... dest!: sym[of pop A for A] ...)
If this is now supported (it's not in 2013-2, where standard is already
deprecated): Nice feature! I have no objections left against removing
standard ;)
Here is one more changeset to clarify that
*** Pure ***
* Obsolete attribute standard has been discontinued (legacy since
Isabelle2012). Potential INCOMPATIBILITY, use explicit 'for' context
where instantiations with schematic variables are intended (for
declaration commands like 'lemmas' or attributes like of). The
following temporary
Am 22.01.2014 um 21:18 schrieb Makarius makar...@sketis.net:
On Tue, 21 Jan 2014, Jasmin Christian Blanchette wrote:
This brings the new (co)datatype package where we want it to be for the next
release.
Great. This is a big step forward.
Thank you for your kind words.
I would like to
On Thu, 23 Jan 2014, Jasmin Blanchette wrote:
I would like to mention the central role played by Isabelle/jEdit for
refactoring the theories, in particular reorganizing the theory imports.
The Theories and Sidekick pannels were simply invaluable.
At some point I would like to see the theory
Great news! I hope to see a brief announcement paper illustrating some of the
new things that can be done. Or did you publish that last year?
Larry
On 21 Jan 2014, at 12:54, Jasmin Christian Blanchette
jasmin.blanche...@gmail.com wrote:
*** HOL ***
* Moved new (co)datatype package and its
Hi Larry,
Am 23.01.2014 um 14:38 schrieb Lawrence Paulson l...@cam.ac.uk:
Great news! I hope to see a brief announcement paper illustrating some of the
new things that can be done. Or did you publish that last year?
I believe you are on the committee of a conference where such a paper has
On Thu, 23 Jan 2014, Lawrence Paulson wrote:
I still use it sometimes, but it could be better. I don’t think the
quality of the layout is actually that important.
You can actually try the graphview right now by searching on this
mailing list, when it was announced. That quickly lead to the
401 - 500 of 766 matches
Mail list logo
