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