ฉันต้องการรับโค้ด LaTeX ที่เกี่ยวข้องกับ ทฤษฎีนี้ . คำตอบก่อนหน้านี้มีเฉพาะลิงก์ไปยังเอกสารประกอบเท่านั้น ให้ฉันอธิบายสิ่งที่ฉันทำ ฉันไปที่ไดเรกทอรีของ Hales.thy และดำเนินการ isabelle mkroot ตามด้วย isabelle build -D . ซึ่งสร้างไฟล์ชื่อ...

เป็นไปได้ไหมที่จะใช้ชื่อ pred_Zero และ pred_Suc แทน 1 และ 2 ในการพิสูจน์โดยการเหนี่ยวนำต่อไปนี้ fun pred where pred_Zero: "pred 0 = 0" | pred_Suc: "pred (Suc n) = n" lemma pred_le: "pred n ≤ n" proof...