>> Dear all, >> >> I tried the variant of the lemma from my previous mail and the result is >> in the attached patch (created with "hg qnew"). For testing I ran >> >> isabelle build -b HOL-Imperative_HOL >> >> as well as >> >> isabelle afp_build Separation_Logic_Imperative_HOL >> >> as far as I can tell the only session in the AFP depending on >> Imperative_HOL. >> >> I did not obtain any errors.
See now http://isabelle.in.tum.de/reports/Isabelle/rev/c6427c9d0898. Cheers, 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
