Hi *,
I am currently busy with stocktaking the results of my visit to TUM last
Wednesday, and I have updated the current state of two affairs in the wiki:
* The set story: https://isabelle.in.tum.de/community/Having_%27a_set_back
Not everything mentioned there is an ultimate need, but we should s
Dear Makarius,
Thanks for the effort put into jEdit! With every revision I use it more
frequently and for ever larger developments. I already reached the point
where I am annoyed when I have to fall back to ProofGeneral (glaring at
the Screen for some moments and waiting for a result, until I
Something slightly related and not very important. In changeset
9ff441f295c2 of the Isabelle repo the congruence rule for the constant
"list_ex" is called list_any_cong. For consistency I suggest to rename
it to list_ex_cong.
cheers
chris
On 03/16/2012 06:47 PM, Christian Sternagel wrote:
D
On Fri, 16 Mar 2012, Lawrence Paulson wrote:
I have a problem with the current version (9ff441f295c2). See
attachment. This prevents the use of PG within ZF. However, it builds at
the command line. What is supposed to be here?
Are you sure that your Pure/FOL base image is up to date?
Anyway,
Also in ZF/Inductive_ZF.thy...
Larry
On 16 Mar 2012, at 10:35, Lawrence Paulson wrote:
> I have a problem with the current version (9ff441f295c2). See attachment.
> This prevents the use of PG within ZF. However, it builds at the command
> line. What is supposed to be here?
>
>
>
>
> Larry
Dear all,
in preparation for the next release I refactored one of our AFP entries
(Abstract-Rewriting). There was an underlying theory Util.thy (quite
big), which essentially turned out to be unused in the rest of the AFP
entry ;) (but we heavily rely on it in IsaFoR, which is not in the AFP).
