src/HOL/plain.ML
author bulwahn
Fri, 11 Mar 2011 10:37:40 +0100
changeset 41910 709c04e7b703
parent 37694 19e8b730ddeb
permissions -rw-r--r--
adding serial instance of finite_4 in lazysmallcheck; changing code equations for implies


(* side-entry for HOL-Plain *)

use_thys ["Plain"];