Wie kann ich Isabelle/HOL verwenden, um LaTeX automatisch aus meinen Quellentheorie-Dateien zu generieren?Wie erzeuge ich LaTeX von Isabelle/HOL?
Isabelle/HOL tutorial.pdf ist sehr schön. Ich werde eine Arbeit in LaTeX mit viel Isabelle-Code schreiben.
Sie sollten sich zuerst die vorhandene Dokumentation ansehen und danach mit spezifischeren Fragen zurückkommen (wenn es welche gibt; aber ich bin mir sicher, dass;)).
Was Sie tun möchten, heißt Dokument Vorbereitung in Isabelle. Der erste Ort, um nachzuschauen, ist Kapitel 4 Presenting Theorien von the Isabelle System Manual. (Eigentlich ist es auch eine gute Idee, zunächst das vorherige Kapitel auf Isabelle Sitzungen zu lesen und Management aufzubauen.)
Für einige ordentlich Notation LaTeX Sugar for Isabelle Documents könnte auch von Interesse sein.
Einige andere nützliche Dinge, wie Schnipsel TeX Erzeugung von Ihren Isabelle Theorien und sie in Ihrem Dokument (die Sie gemeinsam mit anderen auf funktionieren könnte, die haben Isabelle nicht installiert ist), können sich auf der Community Wiki finden.
Danke, jetzt kann ich 'isabelle mkroot -d' und' isabelle build -D' verwenden, um die Aufgabe zu erledigen. – njuguoyi
[Isabelle/HOL] (https://isabelle.in.tum.de/) - eine formale mathematische Logik und Programmiersprache - enthält Mechanismen zum Generieren von LaTeX aus Quelldateien. Diese Frage ist für Stack Overflow sehr aktuell. – davidg