Finally, (after I have found out how to use afp_build) I could reproduce
and fix the docuemnt preparation errors in the CAVA-entries, and now,
according to afp-status, everything works fine.
-- Peter
___
isabelle-dev mailing list
isabelle-...@in.tum.de
Thanks for that. It’s good to have them all back to green.
Cheers,
Gerwin
On 30 Jun 2014, at 11:20 am, Peter Lammich lamm...@in.tum.de wrote:
Finally, (after I have found out how to use afp_build) I could reproduce
and fix the docuemnt preparation errors in the CAVA-entries, and now,
* 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
On Sun, 29 Jun 2014, Cezary Kaliszyk wrote:
Hi Makarius,
On Thu, Jun 26, 2014 at 11:08 PM, Makarius makar...@sketis.net wrote:
At the moment (06599233e54e) there are no remaining uses of Proof General to
the best of my knowledge. If anybody has counter-examples they should be
put on the
On Wed, 11 Jun 2014, Gerwin Klein wrote:
On 11.06.2014, at 2:56 pm, Thomas Sewell thomas.sew...@nicta.com.au wrote:
Gerwin will push the isabelle hypsubst change to the testboard now (assuming he
can remember how).
He could and did.
Has that change been landed? Which changeset IDs are
The changeset has landed in the sense that I sent Gerwin a bundle containing:
changeset: 6bf63b1f41f0
tag: tip
user:Thomas Sewell thomas.sew...@nicta.com.au
date:Wed Jun 11 14:24:23 2014 +1000
summary: Hypsubst preserves equality hypotheses
He probably pushed it to
Dear developers,
would somebody be willing to pull in the attached patches into
HOL/Library? The patches where generated with the help of mercurial's mq
extension (i.e., the series file gives the order of application) and
each patch can be imported into a repository by
hg import --user
Hi Makarius,
On Thu, Jun 26, 2014 at 11:08 PM, Makarius makar...@sketis.net wrote:
At the moment (06599233e54e) there are no remaining uses of Proof General to
the best of my knowledge. If anybody has counter-examples they should be
put on the table for discussion.
I am using Isabelle via
Is there any serious objection against these patches? If not and nobody
else volunteers, I plan to get hands on by Thursday.
Florian
On 30.06.2014 15:59, Christian Sternagel wrote:
Dear developers,
would somebody be willing to pull in the attached patches into
HOL/Library? The
10 matches
Mail list logo
