Re: [isabelle] Isabelle2016-1-RC3: problem with records
On 25/11/16 14:15, Thiemann, Rene wrote:
> record foo =
> a :: bool
> a' :: bool
> It compiles with Isabelle 2016, but not with Isabelle 2016-RC3.
> In the release candidate there is a name clash of internal variables
> in the record construction which seem to be generated by just adding
> a prime (â):
> Duplicate variables on left hand side of equation, in theorem:
> equal_foo_ext_inst.equal_foo_ext âa = ?a, a' = ?a', â = ?moreâ âa = ?a', a' = ?a'', â = ?more'â â
> ?a = ?a' â ?a' = ?a'' â ?more = ?more'
> Failed to define record "foo"
Bisection leads to
The first bad revision is:
date: Mon Jun 06 22:22:05 2016 +0200
summary: clear distinction between different situations concerning
strictness of code equations
It is unclear to me, what happens here. Florian needs to look at it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and