[isabelle] Isabelle2016-1-RC3: problem with records
consider the following record definition:
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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and