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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
