Isabelle 有两种证明方式：旧的“应用”方式，证明只是一个链
apply (this method)
apply (that method)
声明，以及新的“结构化”Isar 风格。我自己，我觉得两者都很有用；“应用”风格更简洁，因此对于无趣的技术引理很方便，而“结构化”风格对于主要定理很方便。
有时我喜欢从一种风格切换到另一种风格，中等证明。从“应用”样式切换到“结构化”样式很容易：我只是插入
proof -
在我的应用链中。我的问题是：如何从“结构化”样式切换回“应用”样式？
举一个更具体的例子：假设我有五个子目标。我发出一些“应用”指令来发送前两个子目标。然后我开始进行结构化证明以省去第三个证明。我还有两个子目标：我如何为这些返回“应用”样式？
apply_end您可以通过使用而不是在结构化证明中继续“应用”样式apply，但这在实践中很少见，只有在探索性工作中才会出现。在完善的证明中，您只需选择值得 Isar 证明的子目标，并在 之后的一个方法调用中完成所有剩余的子目标qed，因为不需要以任何特定顺序处理子目标。
或者，您可以defer在开始结构化证明之前使用proof并立即以“应用”样式继续处理其他子目标，即，您将结构化证明的目标推迟到最后。
fix最后，您当然可以在结构化证明中使用/ assume/重新陈述您的目标，show并在此处继续“应用”样式。但是您必须分别为每个剩余的子目标执行此操作，因此这可能有点乏味。默认案例名称goal1,goal2等有助于打字，但此类证明通常难以维护（尤其是在apply_end更改目标编号时goal<n>）。