[isabelle-dev] the “algebra" proof method

Makarius makarius at sketis.net
Wed Aug 22 21:18:33 CEST 2012

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.


More information about the isabelle-dev mailing list