This summary seems to make it clear that this new feature achieves very little, with the following costs:
- it gives users yet something else (as if there isn't already enough!) to lookup in the documentation, or ask questions about - it's positively confusing, in that "Theorem name ... " has totally different meanings, depending on which case applies (eg, in one case, name must already exist, in the other, it ought not to already exist) This idea looks like the start of the path followed in Isabelle and Coq, of having a multitude of commands, some with a multitude of variants (eg optional arguments) with no coherent consistent grammar rules - just so that the user doesn't need to type a few punctuation symbols. Jeremy On 8/1/19 2:41 pm, Konrad Slind wrote: > Isn't it clear just from the form? > > Theorem name quote (ML) --> val name = Q.store_thm(name,quote,ML) > Theorem name (ML) --> val name = save_thm(name,ML) > > _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
