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:
changeset:   63253:9986559617ee
parent:      63241:f59fd6cc935e
user:        haftmann
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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.