src/Doc/ROOT
changeset 59175 bf465f335e85
parent 58801 f420225a22d6
child 59378 065f349852e6
     1.1 --- a/src/Doc/ROOT	Mon Dec 22 15:50:16 2014 +0100
     1.2 +++ b/src/Doc/ROOT	Mon Dec 22 16:44:24 2014 +0100
     1.3 @@ -206,7 +206,7 @@
     1.4      "root.tex"
     1.5  
     1.6  session Locales (doc) in "Locales" = HOL +
     1.7 -  options [document_variants = "locales", pretty_margin = 65, skip_proofs = false]
     1.8 +  options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false]
     1.9    theories
    1.10      Examples1
    1.11      Examples2
    1.12 @@ -387,7 +387,7 @@
    1.13      "Documents/Documents"
    1.14    theories [document = ""]
    1.15      "Types/Setup"
    1.16 -  theories [pretty_margin = 64, thy_output_indent = 0]
    1.17 +  theories [thy_output_margin = 64, thy_output_indent = 0]
    1.18      "Types/Numbers"
    1.19      "Types/Pairs"
    1.20      "Types/Records"
    1.21 @@ -397,7 +397,7 @@
    1.22      "Rules/Basic"
    1.23      "Rules/Blast"
    1.24      "Rules/Force"
    1.25 -  theories [pretty_margin = 64, thy_output_indent = 5]
    1.26 +  theories [thy_output_margin = 64, thy_output_indent = 5]
    1.27      "Rules/TPrimes"
    1.28      "Rules/Forward"
    1.29      "Rules/Tacticals"