之間的轉換有兩種樣式伊莎貝爾證明:舊的「適用」的風格,證明僅僅是一個伊莎貝爾:「結構化」和「應用式」證據
apply (this method)
apply (that method)
陳述鏈,和新的「結構化」伊薩爾風格。我自己,我覺得有用; 「應用」風格更加簡潔,因此適用於無趣的技術語法,而「結構化」風格則適用於主要定理。
有時我喜歡從一種風格切換到另一種風格,中等防護。從「應用」風格切換到「結構化」風格很簡單:我只需在我的應用鏈中插入
proof -
。我的問題是:我怎樣才能從「結構化」風格切換回「適用」風格?
舉一個更具體的例子:假設我有五個子目標。我發佈了一些「適用」指令來發送前兩個子目標。然後,我發起了一個結構化的證明,取消第三個。我還有兩個子目標:我如何返回到「應用」風格?