src/Doc/ROOT
changeset 54017 2a3c07f49615
parent 53769 036e80175bdd
child 54331 9e944630be0c
     1.1 --- a/src/Doc/ROOT	Tue Oct 01 22:50:42 2013 +0200
     1.2 +++ b/src/Doc/ROOT	Tue Oct 01 23:46:46 2013 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4      "document/style.sty"
     1.5  
     1.6  session Functions (doc) in "Functions" = HOL +
     1.7 -  options [document_variants = "functions", skip_proofs = false]
     1.8 +  options [document_variants = "functions", skip_proofs = false, quick_and_dirty]
     1.9    theories Functions
    1.10    files
    1.11      "../prepare_document"