当我有很多假设时，有时我会得到很多使证明混乱的临时名称。
我在谈论这样的事情：
lemma foo: ...
proof
assume P: ... and Q: ... and R: ...
then have ...
then have ... using P ...
then have ... using P R ...
then show ...
proof
assume A: ... and B: ... and C: ...
then have ...
then have ... using B C ...
...
你能想象它是如何演变的吗？许多语句的名称，在事物的宏大计划中，不值得命名，但仍然被命名，因为我们需要稍后引用它们。
另一方面，如果我们使用所有当前假设，多余的名称不会使证明混乱：
lemma foo: ...
proof
assume ... and ... and ...
then have ...
then have ... using assumptions ...
then have ... using assumptions ...
then show ...
proof
assume ... and ... and ...
then have ...
then have ... using assumptions ...
...
当然，using assumptions伊莎贝尔不是一个有效的说法。我知道 about assms，它引用了该assumes子句，但我不知道是否存在这样的事情 for assume。
有没有办法引用由创建的所有当前假设assume？