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

Michael Norrish Michael.Norrish at nicta.com.au
Wed Sep 8 01:42:50 CEST 2010

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?


More information about the isabelle-dev mailing list