Re: [Hol-info] New grammar of defining theorems?

Mon, 07 Jan 2019 22:07:41 -0800 


On 8/1/19 4:49 pm, [email protected] 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info



























					Reply via email to