src/HOL/Hilbert_Choice.thy
changeset 17420 bdcffa8d8665
parent 16796 140f1e0ea846
child 17702 ea88ddeafabe
equal deleted inserted replaced
17419:16df5a5eef68 17420:bdcffa8d8665
   547 by blast
   547 by blast
   548 
   548 
   549 lemma ex_forward: "[| \<exists>x. P'(x);  !!x. P'(x) ==> P(x) |] ==> \<exists>x. P(x)"
   549 lemma ex_forward: "[| \<exists>x. P'(x);  !!x. P'(x) ==> P(x) |] ==> \<exists>x. P(x)"
   550 by blast
   550 by blast
   551 
   551 
       
   552 
       
   553 text{*Many of these bindings are used by the ATP linkup, and not just by
       
   554 legacy proof scripts.*}
   552 ML
   555 ML
   553 {*
   556 {*
   554 val inv_def = thm "inv_def";
   557 val inv_def = thm "inv_def";
   555 val Inv_def = thm "Inv_def";
   558 val Inv_def = thm "Inv_def";
   556 
   559