Isabelle .thy 파일에서 LaTeX .tex 파일을 생성하려면 isabelle build -D xxx을 사용하고 싶습니다. 그러나 Isabelle은 모든 이론 종속성을 확인하고 모든 관련 .thy 파일이 관련되어야합니다.Isabelle에서 문서 준비
파일을 생성하기 위해 구문 오류가있는 파일 .thy을 부담없이 사용하는 것이 가능합니까? 사실 나는 종이의 일부만 작성하면됩니다.
내가 아는 한 최선을 다할 때까지. LaTeX 세대는 파일을 성공적으로 처리해야합니다. notation (latex) 명령과 antiquotations 때문에.
파일의 일부만 필요하면 생성 된 .tex 파일에서 복사하여 복사하거나 더 자동화 된 것을 원한다면 Generate TeX Snippets wiki 페이지를 살펴보십시오.
결함이 있거나 불완전한 형식 이론을 기반으로 종이를 쓰고 싶습니까?
Isabelle 문서 준비 시스템은 훌륭한 인쇄술로 실제로 작동하는 공식 이론을 게시하여 "코드"처럼 보이지 않도록하기위한 것입니다. 그래서 모든 디폴트는 잘 형성되고 검증 된 이론으로부터 LaTeX을 생산하기위한 것입니다.
그럼에도 불구하고 시스템에서 비공식 LaTeX 출력을 얻는 방법은 다양합니다. 아주 기본적인 메커니즘은 latex 인쇄 모드입니다. 이사벨 (Isabelle)의 다양한 진단 명령은 이러한 괄호 안의 인쇄 모드 사양을 허용한다. 같은 :
thm (latex) exI exE
또는
print_statement (latex) exI exE
당신은 대화 형으로이 작업을 수행 할 수 있으며, 원시 TEX 파일에 출력을 복사하여 붙여 넣습니다. isabelle.sty 파일에서 주변 환경이 적절한 지 확인해야합니다.