[isabelle] Isabelle2016-RC1: typedef-overloaded and records



Dear all,

when adapting our theories to Isabelle2016-RC1, I encountered a problem with the new upgrade of typedef and the overloaded constants.

Note that ('a,'b)rbt in "~~/src/HOL/Library/RBT" is such an overloaded type. As a user of RBTâs I now have to put a context around 
other types that use RBTâs with a parametric 'a as in the example type âuse_rbt_Aâ.

However, the problem is that, I now cannot put these types into records or use records with generic RBTâs as arguments, since
records are not localized. So, the creation of both types use_rbt_B and use_rbt_C fails.

Is there any known work-around to this problem? 
(Except for converting the records into datatypes and then recursively wrap a context with [[typedef_overloaded]] around every further
 type declaration that transitively depends on these types)

With best regards,
RenÃ


theory Test
imports
  "~~/src/HOL/Library/RBT"
begin

context
  notes [[typedef_overloaded]]
begin
datatype 'a use_rbt_A = Foo "('a,bool) rbt"
end

record 'a use_rbt_B = 
  bar :: "'a use_rbt_A"

record 'a use_rbt_C = 
  com :: "('a,bool)rbt"

end


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