[isabelle-dev] Beta/Eta normalisation and net matching.

2010-08-03 Thread Thomas Sewell
Hello Isabelle developers. I was about to have another attempt at speeding up a tactic we implemented for L4.verified using net-matching. In reading Pure/net.ML I spotted the comment Requires operands to be beta-eta-normal. In rereading the existing biresolution_from_nets_tac code, however, I

Re: [isabelle-dev] Beta/Eta normalisation and net matching.

2010-08-03 Thread Tobias Nipkow
There is no requirement or guarantee that theorems in general are in any kind of normal form. Tobias Thomas Sewell schrieb: Hello Isabelle developers. I was about to have another attempt at speeding up a tactic we implemented for L4.verified using net-matching. In reading Pure/net.ML I