moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
(* 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