錯誤從講座採取了伊莎貝爾函數定義指出

Question

爲什麼一個函數（類）的定義如下

definition nondecreasing_on :: "real set => (real => real) => bool" 
where "nondecreasing_on S f <-> (ALL x:S. ALL y:S. x<=y --> f x <= f y)" 

回報Inner syntax error⌂ Failed to parse prop？

該定義取自this文本，鏈接自Isabelle社區wiki的講義筆記部分，因此它應該是正確的。
（當然，文本是舊的，所以也許語法已經改變了，但即使在用\in替換的所有文件以使其具有適當的類似LaTeX的格式之後，導入Complex_Main而不是Main，正如講座筆記所暗示的，刪除可能存在問題的符號，如_等等，錯誤仍然存​​在。）

Answer 1

您可以在Isabelle/jEdit中看到<->的<加下劃線爲紅色。舊的ASCII語法被越來越多地刪除。在現代伊莎貝爾，其定義如下所示：

definition nondecreasing_on :: "real set ⇒ (real ⇒ real) ⇒ bool" 
    where "nondecreasing_on S f ⟷ (∀x∈S. ∀y∈S. x ≤ y ⟶ f x ≤ f y)"