src/HOL/base.ML
author huffman
Wed, 10 Aug 2011 14:10:52 -0700
changeset 44137 ac5cb4c86448
parent 37694 19e8b730ddeb
permissions -rw-r--r--
simplify some proofs


(* side-entry for HOL-Base *)

use_thys ["HOL"];