doc-src/Codegen/Thy/Setup.thy
changeset 42358 b47d41d9f4b5
parent 42293 6cca0343ea48
child 42669 04dfffda5671
equal deleted inserted replaced
42357:3305f573294e 42358:b47d41d9f4b5
    20 end
    20 end
    21 *}
    21 *}
    22 
    22 
    23 setup {* Code_Target.set_default_code_width 74 *}
    23 setup {* Code_Target.set_default_code_width 74 *}
    24 
    24 
    25 ML_command {* unique_names := false *}
    25 declare [[unique_names = false]]
    26 
    26 
    27 end
    27 end