Inconsistent naming of variables in IDE
Naming of variable is inconsistent between different view options (with/without introduction of premises). As a result, the names selected might not be the one you think. For the following goal:
module A
use import int.Int
constant x : int = 0
goal G : forall x:int. x = 1 -> x >= 0
end
with introduction of premises disabled, calling a transformation that refer to "x" will not refer to the constant with that name but to the quantified variable (named "x1" by IDE).
Note: as a side effect, this will also perform a "hard" premises introduction.