# HG changeset patch # User Lars Hupel # Date 1460901764 -7200 # Node ID d0dfdd413a7f6a9f281574029cea29353406d8c5 # Parent 65f27985344908cba6dd9df997d075345895d341 remove "slow" session tags diff -r 65f279853449 -r d0dfdd413a7f src/HOL/ROOT --- a/src/HOL/ROOT Sun Apr 17 12:59:55 2016 +0200 +++ b/src/HOL/ROOT Sun Apr 17 16:02:44 2016 +0200 @@ -14,7 +14,7 @@ "root.bib" "root.tex" -session "HOL-Proofs" (slow) = Pure + +session "HOL-Proofs" = Pure + description {* HOL-Main with explicit proof terms. *} @@ -399,14 +399,14 @@ options [document = false] theories Decision_Procs -session "HOL-Proofs-ex" (slow) in "Proofs/ex" = "HOL-Proofs" + +session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + options [document = false, parallel_proofs = 0] theories Hilbert_Classical Proof_Terms XML_Data -session "HOL-Proofs-Extraction" (slow) in "Proofs/Extraction" = "HOL-Proofs" + +session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" + description {* Examples for program extraction in Higher-Order Logic. *} @@ -425,7 +425,7 @@ Euclid document_files "root.bib" "root.tex" -session "HOL-Proofs-Lambda" (slow) in "Proofs/Lambda" = "HOL-Proofs" + +session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" + description {* Lambda Calculus in de Bruijn's Notation.