src/HOL/Plain.thy

reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma

(*  Title:      HOL/Plain.thy
    ID:         $Id$

Contains fundamental HOL tools and packages.  Does not include Hilbert_Choice.
*)

header {* Plain HOL *}

theory Plain
imports Datatype FunDef Record SAT Extraction
begin

ML {* path_add "~~/src/HOL/Library" *}

end