[isabelle] No such variable



Hi,



I have a small feature request: I have a large list of theorems that I'm giving to blast. To simplify blast's search space, I want to fix all of the variables in my theorem list. However, some of the theorems contain only a proper subset of the variables I'm fixing. This causes Isabelle to report a "no such variable" error, even though all of the variables I'm fixing occur in at least one of the theorems.



Below is a simplified example of the error I'm hitting:



theory NoSuchVar

imports Main

begin



lemma L1: "x = x" by auto



lemma L2: "y = y" by auto



lemmas both = L1 L2



thm both[where x=x and y=y] -- {* reports "no such variable" error *}



end



Could this behavior be changed such that the error is reported only when a variable occurs in none of the theorems?



I'm using Isabelle2011-1.



Thanks,



John





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.