doc-src/Codegen/Thy/Setup.thy
changeset 42669 04dfffda5671
parent 42358 b47d41d9f4b5
child 43271 8b968645d216
equal deleted inserted replaced
42668:b98f22593f97 42669:04dfffda5671
    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 declare [[unique_names = false]]
    25 declare [[names_unique = false]]
    26 
    26 
    27 end
    27 end