src/HOL/Hilbert_Choice.thy
changeset 17420 bdcffa8d8665
parent 16796 140f1e0ea846
child 17702 ea88ddeafabe
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Sep 15 17:18:57 2005 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Sep 15 17:44:53 2005 +0200
     1.3 @@ -549,6 +549,9 @@
     1.4  lemma ex_forward: "[| \<exists>x. P'(x);  !!x. P'(x) ==> P(x) |] ==> \<exists>x. P(x)"
     1.5  by blast
     1.6  
     1.7 +
     1.8 +text{*Many of these bindings are used by the ATP linkup, and not just by
     1.9 +legacy proof scripts.*}
    1.10  ML
    1.11  {*
    1.12  val inv_def = thm "inv_def";