equal
deleted
inserted
replaced
17 \<close> |
17 \<close> |
18 |
18 |
19 ML \<open>val ZF_ss = simpset_of \<^context>\<close> |
19 ML \<open>val ZF_ss = simpset_of \<^context>\<close> |
20 |
20 |
21 simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = \<open> |
21 simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = \<open> |
22 fn _ => Quantifier1.rearrange_bex |
22 fn _ => Quantifier1.rearrange_Bex |
23 (fn ctxt => |
23 (fn ctxt => unfold_tac ctxt @{thms Bex_def}) |
24 unfold_tac ctxt @{thms Bex_def} THEN |
|
25 Quantifier1.prove_one_point_ex_tac ctxt) |
|
26 \<close> |
24 \<close> |
27 |
25 |
28 simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = \<open> |
26 simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = \<open> |
29 fn _ => Quantifier1.rearrange_ball |
27 fn _ => Quantifier1.rearrange_Ball |
30 (fn ctxt => |
28 (fn ctxt => unfold_tac ctxt @{thms Ball_def}) |
31 unfold_tac ctxt @{thms Ball_def} THEN |
|
32 Quantifier1.prove_one_point_all_tac ctxt) |
|
33 \<close> |
29 \<close> |
34 |
30 |
35 |
31 |
36 (** Lemmas for showing that <a,b> uniquely determines a and b **) |
32 (** Lemmas for showing that <a,b> uniquely determines a and b **) |
37 |
33 |