renamed get_axiom_i to axiom, removed obsolete get_axiom;
reduced pervasive names;
(* 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