This is quite an interesting example.
The reason for discarding the equality is that these simple tactics work by
repetition. if the equality is retained, then the procedure will loop. One
could imagine a more refined procedure that maintained a list of variables that
had undergone
Am 15.06.2010 um 11:03 schrieb Lawrence Paulson:
Altering the behaviour of the safe method on locale constants might be
feasible, because it would affect only a few proofs. Can anybody tell me
whether there is an easy way to identify whether a free variable is actually
a locale constant?
On Tue, Jun 15, 2010 at 2:03 AM, Lawrence Paulson l...@cam.ac.uk wrote:
Altering the behaviour of the safe method on locale constants might be
feasible, because it would affect only a few proofs. Can anybody tell me
whether there is an easy way to identify whether a free variable is actually
If there is an easy way to identify free variables that are constrained
externally, then such a change would be beneficial. Failing that, the
particular case of locales is particularly necessary to handle correctly.
Larry
On 15 Jun 2010, at 14:17, Brian Huffman wrote:
Note that testing
