wenzelm [Mon, 22 Oct 2001 18:01:15 +0200] rev 11884
make this module appeat late in Pure;
moved print_current_goals to display.ML;
added quick_and_dirty_prove_goalw_cterm (from Isar/skip_proof.ML);
added thm database functions (from Thy/thm_database.ML);