[isabelle-dev] typedef (open) legacy

[Christian Urban]

Hi,

"Closed" type definitions with

  typedef new_type = "some set"

are considered legacy. The warning message suggests
to use

  typedef (open) new_type = "some set"

but as far as I can see, this does not introduce
a definition for the set underlying the type. For
example the theorem

  new_type_def

is not generated with open.

I have a number of lemmas that are of the form

   f \<in> new_type ==> something

which require new_type_def. What is the received
wisdom to update those proofs?

I see that FinFun.thy goes around the problem
above by giving an explicit definition for the 
set as in

  definition new_type_set = something

  typedef (open) new_type = new_type_set 

Is this how it should be done nowadays? Looks
to me more verbose than an improvement.

Any comments?

Best wishes,
Christian