Re: [isabelle-dev] is_concealed

2014-11-27 Thread Florian Haftmann
See now http://isabelle.in.tum.de/reports/Isabelle/rev/5f060de2dfd6 Florian On 20.11.2014 17:34, Dmitriy Traytel wrote: Sorry for reviving an ancient thread, but have the constants defined by inductive ever been visible to find_consts since Florian's commit (I presume 4a3747517552 ?).

Re: [isabelle-dev] is_concealed

2014-11-26 Thread Florian Haftmann
Hi Dmitriy, thanks for figuring out. I am currently having a look at it… Florian On 20.11.2014 17:34, Dmitriy Traytel wrote: Sorry for reviving an ancient thread, but have the constants defined by inductive ever been visible to find_consts since Florian's commit (I presume

Re: [isabelle-dev] is_concealed

2014-11-26 Thread Florian Haftmann
It had been a lapsus. Regression is under way. Florian On 26.11.2014 15:39, Florian Haftmann wrote: Hi Dmitriy, thanks for figuring out. I am currently having a look at it… Florian On 20.11.2014 17:34, Dmitriy Traytel wrote: Sorry for reviving an ancient thread, but

Re: [isabelle-dev] is_concealed

2014-11-20 Thread Dmitriy Traytel
Sorry for reviving an ancient thread, but have the constants defined by inductive ever been visible to find_consts since Florian's commit (I presume 4a3747517552 ?). Today in be4a911aca71 (but also in Isabelle2014 and even in Isabelle2012) in the following inductive xyz :: bool where xyz