> Therefore, I still would propose to recommend to use the form $e |- ( ( ph /\ > x = ... ) -> ... ) $. in deduction style.
I agree. Plus, this is more systematic hence easier to remember. > Already existing theorems need not to be rewritten They need not but they could ! > (by the way, many of them have no "d" at the end..). Since deduction form is the default for more advanced theorems, this makes sense. Benoît -- 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/a797fa74-53ad-4b63-8c3f-f8acaeb160cf%40googlegroups.com.
