--- a/src/ZF/pair.thy Sun May 24 21:11:23 2020 +0200
+++ b/src/ZF/pair.thy Sun May 24 19:57:13 2020 +0000
@@ -19,17 +19,13 @@
ML \<open>val ZF_ss = simpset_of \<^context>\<close>
simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_bex
- (fn ctxt =>
- unfold_tac ctxt @{thms Bex_def} THEN
- Quantifier1.prove_one_point_ex_tac ctxt)
+ fn _ => Quantifier1.rearrange_Bex
+ (fn ctxt => unfold_tac ctxt @{thms Bex_def})
\<close>
simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_ball
- (fn ctxt =>
- unfold_tac ctxt @{thms Ball_def} THEN
- Quantifier1.prove_one_point_all_tac ctxt)
+ fn _ => Quantifier1.rearrange_Ball
+ (fn ctxt => unfold_tac ctxt @{thms Ball_def})
\<close>