Thanks for your answer Michael.
On 15/10/17 06:27, michael.norr...@data61.csiro.au wrote:
> This is a feature that hasn’t really been pursued. There is some code
> supporting their use (akin to the way Abbr`v` is supported in calls to the
> simplifier), but it is incomplete and thus unused,
This is a feature that hasn’t really been pursued. There is some code
supporting their use (akin to the way Abbr`v` is supported in calls to the
simplifier), but it is incomplete and thus unused, and pretty well
undocumented.
But yes, the idea is to be able to label assumptions to make it
I accidentally posted this as a reply to an unrelated message. Apologies.
On 14/10/17 10:53, Mario Castelán Castro wrote:
> Hello.
>
> What is the purpose of labels? The ones from the theory “marker”: “$:-”.
>
> I see that there are some functions in src/marker/markerLib.sml that
> suggest
Hello.
What is the purpose of labels? The ones from the theory “marker”: “$:-”.
I see that there are some functions in src/marker/markerLib.sml that
suggest these are used to designate labels on assumptions. Is this
documented somewhere?
Thanks.
--
Do not eat animals; respect them as you
