HomeIsabelle/Phabricator

clarified use of memory: prefer share tree structures over fresh strings;

Authored by makarius.

Description

clarified use of memory: prefer share tree structures over fresh strings;

Details

Committed
makariusJun 24 2020, 8:59 PM
Parents
rISABELLEc5003c5c72c8: more Java heap space (see 2d658beb815b);
Branches
Unknown
Tags
Unknown