[isabelle-dev] Status of AFP/JinjaThreads

[Florian Haftmann]

Hi all,

> However, due to the deeper reason that the classical reasoner setup has
> been changed so that the original proof failed, one might have to look
> into this specific subgoal again (understanding how the classical
> reasoner has been changed).
> (I am guessing it is due to the Predicate/Relation intro/elim changes.)

I gave it a try.  Infortunately, there is no hint: no relation
predicates, no identifiers introduces by inductive_set etc.  The only
thing which is suspicious is a \<lambda>\<^isup>f…  I'll dive further.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120319/63f00942/attachment.sig>