src/HOL/plain.ML
author haftmann
Wed, 07 Sep 2011 23:07:16 +0200
changeset 44817 b63e445c8f6d
parent 37694 19e8b730ddeb
permissions -rw-r--r--
lemmas about +, *, min, max on nat


(* side-entry for HOL-Plain *)

use_thys ["Plain"];