mailing-list for TeXmacs Users

[Victor Porton <address@hidden>]

I suggest to add the following feature to Coq:

Make a modified "Import" statement (possible syntax: "Import Safe 
MODULENAME.").

This would transform every axiom (or parameter) in the imported module into a 
theorem condition, just like as it is done with sections.

This is especially useful for researching interrelations of several different 
axiom systems.

--
Victor Porton - http://portonvictor.org