src/HOLCF/FOCUS/ROOT.ML
author huffman
Mon, 03 May 2010 18:40:48 -0700
changeset 36656 fec55067ae9b
parent 32960 69916a850301
permissions -rw-r--r--
add lemmas eventually_nhds_metric and tendsto_mono

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