오류가

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?

이 정의는 Isabelle 커뮤니티 위키의 강의 노트 섹션에서 링크 된 this 텍스트에서 가져온 것이므로 정확해야합니다.
(텍스트가 오래되었으므로 구문이 변경되었지만 :을 \in으로 바꾼 후에도 적절한 LaTeX 형식을 사용하기 위해 Main 대신에 Complex_Main을 가져 오는 것이 좋습니다. _과 같이 잠재적으로 문제가되는 기호를 제거하면 오류가 계속 발생합니다.

Answer 1

<->의 <에는 빨간색 밑줄이 그어진 것을 Isabelle/jEdit에서 확인할 수 있습니다. 오래된 ASCII 구문이 점점 더 많이 제거되고 있습니다. 현대 Isabelle의 정의는 다음과 같습니다.

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