On 8/1/19 4:49 pm, michael.norr...@data61.csiro.au wrote:
> I think you've misunderstood.
that's true, sorry.
> Here the advantage is quite clear and valuable: in the existing system, you
> have to type the same string of symbols twice in order to avoid annoying
> maintenance issues when theorems get moved. There's no utility in allowing
> people to write things like
>
> val foo = save_thm("bar", ...)
>
> and it just leads to real pain.
>
there's certainly a discernible advantage in this particular case, I agree
> Slippery slope arguments cut no mustard.
>
Let's hope it's not the start of one. And do work out a way of getting
it into the online documentation (eg, in
HOL/help/src-sml/htmlsigs/idIndex.html)
Jeremy
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
