Isabelleファイルからisabelle build -D xxxLaTeX ファイルを生成するために使用したいと考えています。しかし、Isabelle はすべての理論の依存関係をチェックし、すべての関連ファイルが含まれている必要があります。.tex.thy.thy
.thy構文エラーのあるファイルを何気なく使用してファイルを生成することは.texできますか? 実際、論文を書くにはその一部しか必要ありません。
2 に答える
4
それは、不完全または不完全な形式理論に基づいて論文を書きたいということですか?
Isabelle 文書作成システムは、実際に機能する正式な理論を公開することを目的としており、これが「コード」のように見えないように優れたタイポグラフィーを備えています。したがって、すべてのデフォルトは、整形式でチェック済みの理論から LaTeX を生成するためのものです。
それにもかかわらず、システムから非公式の LaTeX 出力を取得する方法は数多くあります。非常に基本的なメカニズムはlatex印刷モードです。Isabelle のさまざまな診断コマンドでは、このような印刷モードを丸括弧で指定できます。たとえば、次のようになります。
thm (latex) exI exE
また
print_statement (latex) exI exE
これをインタラクティブに実行し、出力を raw tex ファイルにコピー アンド ペーストできます。ファイルからの環境で適切な環境を取得するようにする必要がありisabelle.styます。
于 2014-03-14T20:46:47.217 に答える
3
私の知る限り、いいえ。LaTeX 生成では、たとえばnotation (latex)コマンドや引用符が原因で、ファイルが正常に処理される必要があります。
ファイルの一部だけが必要な場合は、生成されたファイルから単純にコピー アンド ペーストする.texか、さらに自動化されたものが必要な場合は、Generate TeX Snippets wiki ページを参照してください。
于 2013-10-18T17:00:07.483 に答える