I have now patches queued to enabled all of the commented out theorems and pred_set_conv declarations, except for the generalited versions of SUP_UN_eq and INF_INT_eq. Using generalized versions of SUP_UN_eq changes the theorems generated by inductive set in a negative way:
inductive_set TFin :: "'a set set \<Rightarrow> 'a set set set" for S :: "'a set set" where succI: "x : TFin S \<Longrightarrow> succ S x : TFin S" | Pow_UnionI: "Y : Pow(TFin S) \<Longrightarrow> Union(Y) : TFin S" generates for example the theorem: TFin.Pow_UnionI: ?Y ∈ Pow (TFin ?S) ⟹ (⋃i ∈ ?Y. i) ∈ TFin ?S instead of: TFin.Pow_UnionI: ?Y ∈ Pow (TFin ?S) ⟹ ⋃?Y ∈ TFin ?S
When I adapted Relation.thy, it appeared to me suspicious that SUP_UN_eq and INF_INT_eq where not as general as they would naturally be; maybe the problem you experience now has been experienced already by Stefan when he introduced this. Stefan, does this sound somehow familiar to you?
Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev