Re: [isabelle-dev] Global constant names in inductive

> Your proposed change > https://isabelle.in.tum.de/repos/testboard/rev/20d5e446aa10 looks > formally OK. See now Isabelle/3c628937899d and AFP/a7160ffc25f1. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.

Re: [isabelle-dev] Global constant names in inductive

On 06/04/17 13:08, Lars Hupel wrote: >> Did you encounter an actual problem from that situation? >> >> Formally, a comment is not a problem. "Fixing" such things prematurely >> is likely to break it. > > Yes, there is an actual problem. I define a function via > "Function.add_function" and inspect

Re: [isabelle-dev] Global constant names in inductive

> Did you encounter an actual problem from that situation? > > Formally, a comment is not a problem. "Fixing" such things prematurely > is likely to break it. Yes, there is an actual problem. I define a function via "Function.add_function" and inspect the resulting info. As per usual discipline t

Re: [isabelle-dev] Global constant names in inductive

On 06/04/17 09:29, Lars Hupel wrote: > while poking around in the function package (to store more information > in "info"), I also realized that I need a little bit more information > from the inductive package. > > Reading its sources, I stumbled upon 10-year-old comments by Makarius > that remin

Re: [isabelle-dev] Global constant names in inductive

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