src/HOL/plain.ML
author haftmann
Fri, 26 Nov 2010 22:33:21 +0100
changeset 40726 16dcfedc4eb7
parent 37694 19e8b730ddeb
permissions -rw-r--r--
keep type variable arguments of datatype constructors in bookkeeping


(* side-entry for HOL-Plain *)

use_thys ["Plain"];