src/HOL/plain.ML
author wenzelm
Fri, 28 May 2010 16:01:25 +0200
changeset 37163 a60f88087ee1
parent 33615 261abc2e3155
child 37694 19e8b730ddeb
permissions -rw-r--r--
deleted some old fonts;

(*side-entry for HOL-Plain*)
use_thys ["Plain"];