revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)
(* 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