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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev