I tried the following with mmj2: 1. open the original theorem (with local definition) 2. copy proof into a text editor 3. delete the hypothesis containing the local definition 4. replace the local class variable (e.g. Z) by the globally defined symbol (e.g. ZZring) 5. create a new theorem 6. copy the modified proof 7. adjust the proof according to the erormessages provided after unification (these should not be a lot) 8. copy the new theorem (ncluding the proof) into set.mm I think this is much better than retyping the complete prove. But is there even a better solution?
Alexander -- 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/78b20b70-faed-4886-b802-564c286b83dd%40googlegroups.com.
