changeset 17420 | bdcffa8d8665 |
parent 16796 | 140f1e0ea846 |
child 17702 | ea88ddeafabe |
--- 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";