[isabelle] Isabelle2016-RC1: typedef-overloaded and records
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,
datatype 'a use_rbt_A = Foo "('a,bool) rbt"
record 'a use_rbt_B =
bar :: "'a use_rbt_A"
record 'a use_rbt_C =
com :: "('a,bool)rbt"
This archive was generated by a fusion of
Pipermail (Mailman edition) and