[isabelle] datatype fails in unnamed contexts with assumptions
Dear BNF developers,
I noticed that the datatype does not work inside unnamed contexts which make assumptions.
Here's a minimal example:
context assumes "True" begin
datatype f = F
The error message varies with the form of the assumptions. In the above example, it is
exception THM 0 raised (line 111 of "~~/src/Tools/induct.ML"):
No variables in major premise of rule
âTrue; ây. â?x = ??.Scratch.f.Abs_f_IITN_f y; y â UNIVâ â ?Pâ â ?P
Is this not supported at all (I have not found it listed in the limitations section of the
datatype tutorial) or just an implementation insufficiency?
Some background on my usecase: I want to define a datatype which I just need to reduce a
complex problem to a simpler one (a typical "without loss of generality" step), so I'd
want to hide the datatype using "private" (once this will work properly). However, the
theorem already lives in an unnamed context with assumptions, so I cannot easily move the
datatype out of the context with assumptions.
This archive was generated by a fusion of
Pipermail (Mailman edition) and