[isabelle] No such variable


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


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 *}


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.



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