[isabelle-dev] the “algebra" proof method

[Tobias Nipkow]

Am 21/08/2012 19:48, schrieb Lawrence Paulson:
> Or would it make sense to integrate this functionality with the much better known arith method? It could then be a catchall for whatever else gets implemented in the general realm of arithmetic. And this reminds me that we have a great variety of different arithmetic decision procedures, which I imagine can all be invoked via arith, so maybe it indeed makes sense to add your algebraic procedures to arith.

When I came up with the name "by algebra" I had imagined it to be applicable to
many algebraic structures and to subsume many further proof methods. But given
that it has remained the only such method and that it is used primarily for
arithmetic theories, we might as well call it from "by arith", too.

Tobias