--- a/src/HOL/ROOT Mon Jul 01 15:08:29 2013 +0200
+++ b/src/HOL/ROOT Tue Jul 02 14:48:01 2013 +0200
@@ -16,7 +16,7 @@
description {*
HOL-Main with explicit proof terms.
*}
- options [document = false, skip_proofs = false]
+ options [document = false]
theories Proofs (*sequential change of global flag!*)
theories Main
files
@@ -357,7 +357,7 @@
theories Decision_Procs
session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
- options [document = false, skip_proofs = false, parallel_proofs = 0]
+ options [document = false, parallel_proofs = 0]
theories
Hilbert_Classical
XML_Data
@@ -366,7 +366,7 @@
description {*
Examples for program extraction in Higher-Order Logic.
*}
- options [condition = ISABELLE_POLYML, skip_proofs = false, parallel_proofs = 0]
+ options [condition = ISABELLE_POLYML, parallel_proofs = 0]
theories [document = false]
"~~/src/HOL/Library/Code_Target_Numeral"
"~~/src/HOL/Library/Monad_Syntax"
@@ -391,7 +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", skip_proofs = false, parallel_proofs = 0]
+ options [document_graph, print_mode = "no_brackets", parallel_proofs = 0]
theories [document = false]
"~~/src/HOL/Library/Code_Target_Int"
theories