src/HOL/plain.ML
author blanchet
Fri, 20 Jul 2012 22:19:46 +0200
changeset 48391 480746f1012c
parent 37694 19e8b730ddeb
permissions -rw-r--r--
get rid of redundant "xxx_INSTALLED" environment variabl


(* side-entry for HOL-Plain *)

use_thys ["Plain"];