src/HOL/plain.ML
author haftmann
Mon, 08 Feb 2010 14:22:22 +0100
changeset 35043 07dbdf60d5ad
parent 33615 261abc2e3155
child 37694 19e8b730ddeb
permissions -rw-r--r--
dropped accidental duplication of "lin" prefix from cs. 108662d50512

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