src/HOL/Mirabelle/ROOT.ML
author huffman
Mon, 12 Sep 2011 10:43:36 -0700
changeset 44905 3e8cc9046731
parent 33615 261abc2e3155
permissions -rw-r--r--
remove trivial lemma Lim_at_iff_LIM

use_thys ["Mirabelle_Test"];