HOL-ex.Sketch_and_Explore