Isabelle/JEdit에서 xsymbols가 사용됩니까? <a href="http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf" rel="nofollow">Isabelle/HOL tutorial</a>의 섹션 4.1.2에서

Question

우리는 증명 일반의 X-기호 모드 또는 LaTeX의 출력이 활성화 될 때마다

이 규칙에 따라 "xsymbols"의 모드가 활성화되어 찾을 수 있습니다.

이제 일반 사무 총장의 퇴색과 관련하여 xsymbols와 관련이 있습니까?

Answer 1

xsymbols Isabelle/jEdit의 모드는 여전히 기본값입니다.

Isabelle/jEdit은 유니 코드로 편집기에서 심볼을 렌더링하지만 내부 표현은 여전히 ​​xsymbol 인코딩을 사용합니다. 이것은 다른 편집기에서 저장된 이론 파일을 열어서 볼 수 있습니다. 이 주 이자벨 프로세스와 통신으로 jEdit과에 이자벨 플러그인과 유니 코드에서 변환을 수행

lemma "a \<and> b \<Longrightarrow> b \<and> a" 
    by simp 

: 예를 들어, 텍스트 :

lemma "a ∧ b ⟹ b ∧ a" 
    by simp 

는 xsymbols 인코딩으로 파일에 저장됩니다 . (당신이 궁금하면 변환 테이블은, Isabelle/etc/symbols에서 볼 수 있습니다.) 당신이 표기법을 정의하는 경우

이것의 실제적인 결과는, xsymbols는 유액, ProofGeneral와 이자벨/jEdit과 모두를 의미합니다.

아마도 unicode 모드가 내부 xsymbols 표현을 대체 할 것입니다. 그러나 아직 없습니다.