[isabelle-dev] the “algebra" proof method

[Makarius]

On Wed, 22 Aug 2012, 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.

See now http://isabelle.in.tum.de/repos/isabelle/rev/8c6fde547cba


 	Makarius