मैं इसाबेल/एचओएल से लाटेक्स कैसे उत्पन्न करूं?

Question

मैं अपने स्रोत सिद्धांत फ़ाइलों से स्वचालित रूप से लाटेक्स उत्पन्न करने के लिए इसाबेल/एचओएल का उपयोग कैसे कर सकता हूं?

इसाबेल/एचओएल का tutorial.pdf बहुत सुंदर है। मैं लाटेक्स में एक पेपर लिखने जा रहा हूं जिसमें बहुत सारे इसाबेल कोड हैं।

Answer 1

आपको पहले मौजूदा दस्तावेज को देखना चाहिए और बाद में अधिक विशिष्ट प्रश्नों के साथ वापस आना चाहिए (यदि कोई रहता है, लेकिन मुझे यकीन है कि वहां होगा;))।

आप क्या करना चाहते हैं इसे दस्तावेज़ तैयारी इसाबेल में कहा जाता है। देखने के लिए पहली जगह अध्याय 4 the Isabelle System Manual प्रस्तुत करने वाली सिद्धांतों को प्रस्तुत करना है। (वास्तव में यह भी एक अच्छा विचार पहले इसाबेल सत्र पर पिछले अध्याय पढ़ सकते हैं और प्रबंधन निर्माण करना है।)

कुछ साफ अंकन के लिए भी LaTeX Sugar for Isabelle Documents ब्याज की हो सकती है।

कुछ अन्य उपयोगी चीजें, अपने इसाबेल सिद्धांतों से टेक्स के टुकड़े पैदा करने और उन्हें अपने दस्तावेज़ में शामिल है (जो आप सहयोगी रूप से दूसरों कि इसाबेल स्थापित नहीं है, के साथ पर काम कर सकते हैं) की तरह, Community Wiki पर पाया जा सकता।