src/HOL/plain.ML
author Andreas Lochbihler
Tue, 12 Jun 2012 15:32:14 +0200
changeset 48101 1b9796b7ab03
parent 37694 19e8b730ddeb
permissions -rw-r--r--
merged


(* side-entry for HOL-Plain *)

use_thys ["Plain"];