Hi Alexander, For the second list, did you also restrict yourself to the main part of set.mm ? BR, _ Thierry
> Le 3 nov. 2019 à 23:38, 'Alexander van der Vekens' via Metamath > <[email protected]> a écrit : > > > >> On Thursday, October 31, 2019 at 1:55:27 PM UTC+1, Norman Megill wrote: >> >> We could add ph to every such hypothesis to make it more general-purpose, >> but 99% of the time it wouldn't be needed and would make all other proofs >> using it (as well as the theorem itself) slightly longer. Not to mention >> that it would be a huge retrofit to do this throughout set.mm. I will >> concede there may be a few cases where it would be advantageous to do things >> other than prove a simple substitution with the hypothesis, but overall I >> believe it is rare and does not justify adding ph everywhere. >> > I tried to identify all the theorems in set.mm (excluding the mathboxes) > which would be concerned - I found about 70 of them (see attachment > deduct_th_eq_hyp.txt). On the other hand, there are about 50 theorema in > deduction form having the form $e |- ( ( ph /\ x = ... ) -> ... ) $. (see > attachment deduct_th_ph_eq_hyp.txt). So there is no big difference. > Therefore, I still would propose to recommend to use the form $e |- ( ( ph /\ > x = ... ) -> ... ) $. in deduction style. Already existing theorems need not > to be rewritten (by the way, many of them have no "d" at the end..). >> > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/351cfee0-e03b-4d61-b839-694b61641bb0%40googlegroups.com. > <deduct_th_ph_eq_hyp.txt> > <deduct_th_eq_hyp.txt> -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/F0596879-A317-4BAD-8A73-C27509CDC35F%40gmx.net.
