Come posso utilizzare Isabelle/HOL per generare automaticamente LaTeX dai miei file di teoria dei sorgenti?Come posso generare LaTeX da Isabelle/HOL?
Isabelle/HOL's tutorial.pdf è molto bello. Ho intenzione di scrivere un articolo su LaTeX con un sacco di codice Isabelle.
Si dovrebbe prima dare un'occhiata alla documentazione esistente e tornare con domande più specifiche in seguito (se ne rimangono alcune, ma sono sicuro che ci sarà;)).
Quello che vuoi fare si chiama preparazione documento in Isabelle. Il primo posto da cercare è Capitolo 4 Presentando le teorie di the Isabelle System Manual. (In realtà è anche una buona idea di leggere prima il capitolo precedente su sessioni di Isabelle e costruire gestione.)
Per qualche notazione ordinata anche LaTeX Sugar for Isabelle Documents potrebbero essere di interesse.
Alcune altre cose utili, come la generazione di frammenti TeX dalle vostre teorie Isabelle e la loro inclusione nel documento (che si potrebbe lavorare collaborando su con gli altri che non hanno installato Isabelle), possono essere trovati sul Community Wiki.
Grazie, ora posso usare 'isabelle mkroot -d' e' isabelle build -D' per fare il lavoro. – njuguoyi
[Isabelle/HOL] (https://isabelle.in.tum.de/) - una logica matematica formale e un linguaggio di programmazione: contiene meccanismi per generare LaTeX dai file sorgente. Questa domanda è molto in tema per Stack Overflow. – davidg