src/HOL/Set.thy
changeset 26480 544cef16045b
parent 26339 7825c83c9eff
child 26513 6f306c8c2c54
equal deleted inserted replaced
26479:3a2efce3e992 26480:544cef16045b
   471   by blast
   471   by blast
   472 
   472 
   473 lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
   473 lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
   474   by blast
   474   by blast
   475 
   475 
   476 ML_setup {*
   476 ML {*
   477   local
   477   local
   478     val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
   478     val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
   479     fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
   479     fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
   480     val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
   480     val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
   481 
   481