[isabelle-dev] Global constant names in inductive

Lars Hupel hupel at in.tum.de
Thu Apr 6 10:23:33 CEST 2017

> 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.


Does anybody have any objections to pushing this?


More information about the isabelle-dev mailing list