> I'm at a loss for an explanation. Does anybody have any idea what is
> going on there?

I now have an updated patch that instead of changing
"add_inductive_global" to use "open_target"/"close_target" leaves it
unchanged. With this, HOL-Proofs-Lambda and everything else goes through.

  <https://isabelle.in.tum.de/repos/testboard/rev/20d5e446aa10>

Does anybody have any objections to pushing this?

Cheers
Lars
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to