Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unbound schematic variable


view this post on Zulip Email Gateway (Aug 22 2022 at 15:14):

From: Sven Schneider <sven.schneider.pub@gmx.de>
Hi all,

I have some old 2014 theory files that I might want to update to the
current version.
Apparently something has changed and I am unable to find anything in the
NEWS about it.
Is there a minimal workaround that requires minimal effort?
There are very many instances of this sort in the proofs...

Best regards

example
==========================
theory Test
imports
Main
begin

lemma TEST: "foo"
apply(subgoal_tac "?X")

==========================

output
=============
"Unbound schematic variable: ?X"
=============

view this post on Zulip Email Gateway (Aug 22 2022 at 15:14):

From: Makarius <makarius@sketis.net>
The proper way to do it is via "eigen-context" like this:

apply (subgoal_tac "X" for X)

Unbound schematic variables violate the Isabelle/Isar context
discipline. The more tools are properly localized, the less they can
sneak into proof texts.

Here is also a relavant NEWS entry from Isabelle2015:


Last updated: Mar 28 2024 at 20:16 UTC