Since mmj2 can parse expressions, there might be a way to look for expressions which contain instances of a given expression ?
For example, how do I search all assertions which contain as a subexpression an instance of "ph -> ( E. x ( ph /\ ps ) ->" ? Thanks, 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/c5b50524-88cd-4996-ba7b-95988ab1dd00n%40googlegroups.com.
