src/HOLCF/FOCUS/ROOT.ML
author wenzelm
Sat, 28 Aug 2010 20:24:41 +0200
changeset 38843 d95522496593
parent 32960 69916a850301
permissions -rw-r--r--
more careful locking of jEdit buffer;

use_thys ["Fstreams", "FOCUS", "Buffer_adm"];