0
이사벨 (Isabelle)은 특정 다른 기호의 부정 버전 인 기호를 사용할 수있게합니다. 예 : ≠ 및 ∉입니다. LaTeX의 \not 매크로와 같은 임의의 기호의 부정 버전을 가져 오는 메커니즘이 있습니까?이사벨에서 임의의 기호의 음수 버전을 사용할 수 있습니까?
A
답변
1
귀하의 질문에는 두 가지 부분이 있습니다 : 임의의 부정 부호를 사용할 수 있는지 여부와 그러한 기호를 편리한 매크로로 입력 할 수 있는지 여부.
Isabelle FAQ은 JEdit이 다양한 방법으로 입력 된 수학 기호를 유니 코드로 변환하고 유니 코드 기호를 사용/표시한다고 설명합니다. 따라서 원하는 심볼이 유니 코드에 존재하면 심볼을 직접 사용할 수 있습니다 (예 : ctrl-c ctrl-v). 예를 들어, 다음은 "존재하지 않음"을 정의 할 수있게 해줍니다 :
abbreviation notexists :: "(('a ⇒ bool) ⇒ bool)" ("∄") where "∄ Φ ≡ (¬ (∃x. Φ(x)))"
그러나 모든 유니 코드 기호를 사용할 수있는 것은 아닙니다. 예를 들어 italic nabla은 jedit에 올바르게 표시되지 않습니다.
질문의 두 번째 부분 : 지금까지 내가 아는 한, 그러한 매크로는 존재하지 않습니다. 그러나 Isabelle은 기호를 굵게 표시하는 비슷한 매크로 메커니즘을 가지고 있습니다. 예를 들어, \<bold> \<exists>은 굵게 표시된 "존재"기호로 표시됩니다. 이것은 매크로 기능이 있음을 보여 주며, 나중에 제안한 것처럼 심볼을 부정하기위한 매크로를 가질 수 있습니다.