--- a/src/HOL/ROOT Sun Jun 30 11:37:34 2013 +0200
+++ b/src/HOL/ROOT Sun Jun 30 12:30:02 2013 +0200
@@ -16,7 +16,8 @@
description {*
HOL-Main with explicit proof terms.
*}
- options [document = false, proofs = 2, skip_proofs = false]
+ options [document = false, skip_proofs = false]
+ theories Proofs (*sequential change of global flag!*)
theories Main
files
"Tools/Quickcheck/Narrowing_Engine.hs"
@@ -356,7 +357,7 @@
theories Decision_Procs
session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
- options [document = false, proofs = 2, skip_proofs = false, parallel_proofs = 0]
+ options [document = false, skip_proofs = false, parallel_proofs = 0]
theories
Hilbert_Classical
XML_Data
@@ -365,7 +366,7 @@
description {*
Examples for program extraction in Higher-Order Logic.
*}
- options [condition = ISABELLE_POLYML, proofs = 2, skip_proofs = false, parallel_proofs = 0]
+ options [condition = ISABELLE_POLYML, skip_proofs = false, parallel_proofs = 0]
theories [document = false]
"~~/src/HOL/Library/Code_Target_Numeral"
"~~/src/HOL/Library/Monad_Syntax"
@@ -390,8 +391,7 @@
The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
*}
- options [document_graph, print_mode = "no_brackets", proofs = 2, skip_proofs = false,
- parallel_proofs = 0]
+ options [document_graph, print_mode = "no_brackets", skip_proofs = false, parallel_proofs = 0]
theories [document = false]
"~~/src/HOL/Library/Code_Target_Int"
theories
@@ -652,7 +652,7 @@
MaSh_Export
TPTP_Interpret
THF_Arith
- theories [proofs = 0] (* FIXME !? *)
+ theories
ATP_Problem_Import
session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +