[isabelle-dev] the “algebra" proof method

Lawrence Paulson lp15 at cam.ac.uk
Thu Aug 23 12:38:25 CEST 2012


That would be great - thanks!
Larry

On 22 Aug 2012, at 20:18, Makarius wrote:

> On Tue, 21 Aug 2012, Lawrence Paulson wrote:
> 
>> Many thanks for your very detailed response! I wonder what to do next in terms of documenting this method, and perhaps, developing it further. Is there a latex source for the information you sent?  It could be added to the documentation somewhere: but where?
> 
> The default place is the IsarRef manual.  If nobody picks up the thread within a couple of weeks, say, I will just weed the text from the mailing list and put it into some place in the manual.
> 
> 
> 	Makarius




More information about the isabelle-dev mailing list