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 didn't spot any attempt to beta/eta 
normalise the terms passed.

It occurs to me that I don't even know whether theorems in Isabelle can be 
assumed to be beta/eta normal. Does anyone have any quick pointers on that? Is 
there a potential bug here? Don't go searching for it - I'm happy to build some 
test cases and search for the answer myself if noone knows.


The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
Isabelle-dev mailing list

Reply via email to