equal
deleted
inserted
replaced
400 |
400 |
401 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + |
401 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + |
402 options [document = false, parallel_proofs = 0] |
402 options [document = false, parallel_proofs = 0] |
403 theories |
403 theories |
404 Hilbert_Classical |
404 Hilbert_Classical |
|
405 Proof_Terms |
405 XML_Data |
406 XML_Data |
406 |
407 |
407 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" + |
408 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" + |
408 description {* |
409 description {* |
409 Examples for program extraction in Higher-Order Logic. |
410 Examples for program extraction in Higher-Order Logic. |