comment

--- a/src/HOL/Hilbert_Choice.thy	Thu Sep 15 17:18:57 2005 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Thu Sep 15 17:44:53 2005 +0200
@@ -549,6 +549,9 @@
 lemma ex_forward: "[| \<exists>x. P'(x);  !!x. P'(x) ==> P(x) |] ==> \<exists>x. P(x)"
 by blast
 
+
+text{*Many of these bindings are used by the ATP linkup, and not just by
+legacy proof scripts.*}
 ML
 {*
 val inv_def = thm "inv_def";