[isabelle-dev] Global constant names in inductive
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