[isabelle-dev] NEWS: expand_fun_eq -> ext_iff, expand_set_eq -> set_ext_iff

[Michael Norrish]

On 08/09/10 05:04, Brian Huffman wrote:
> OK, this makes sense. It is nice to have the pair of lemmas "foo_ext"
> and "foo_ext_iff" for each function-like type "foo".
>
> So do you propose that we rename all of the expand_*_eq lemmas that I
> listed before? (It would also be good to make sure there is a
> properly-named *_ext lemma corresponding to each one.)

Why not keep both sets of names in play?

Michael