Ошибка в определении функции Isabelle взяты из конспектов

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, поэтому оно должно быть правильным.
(Конечно, текст старый, так что, возможно, синтаксис изменился, но даже после замены всех : на \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)"