(* Title: HOL/SizeChange/ROOT.ML ID: $Id$ *) no_document use_thy "Infinite_Set"; no_document use_thy "Ramsey"; use_thy "Examples";