Hi All, Somebody recently added in the NEWS the entry
Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary, INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter, INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset, UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been discarded. For anybody who has to update a theory (with proofs possibly generated by Sledgehammer), it might be useful to know what the lemmas are that replaced them. In my case I was stumbling upon UNION_eq_Union_image and needed to find out what its replacement should be (SUP_def). I was lucky that this was obvious from the snapshot I needed to update from. But there are also renamings since Isabelle2011, which might make that difficult for larger deltas. I think an entry like for renaming of lemmas, such as More consistent and comprehensive names: INFI_def ~> INF_def SUPR_def ~> SUP_def INF_leI ~> INF_lower INF_leI2 ~> INF_lower2 le_INFI ~> INF_greatest le_SUPI ~> SUP_upper le_SUPI2 ~> SUP_upper2 SUP_leI ~> SUP_least INFI_bool_eq ~> INF_bool_eq SUPR_bool_eq ~> SUP_bool_eq INFI_apply ~> INF_apply SUPR_apply ~> SUP_apply INTER_def ~> INTER_eq UNION_def ~> UNION_eq would be much more useful. Anybody feels responsible? Best wishes, Christian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
