[isabelle-dev] NEWS -> Redundant lemmas

[Christian Urban]

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