[tlaplus] definitions and theorems import in proofs

[Mamoun FILALI-AMINE <mamounfilali@xxxxxxxxx>]

Hello,

Is there a syntax to import all the definitions of a given module by 
specifying only the module name, rather than enumerating each 
definition? For example, instead of writing 'BY DEF IsFiniteSet, 
Cardinality', is there a way to write something like 'BY DEF FiniteSets'?

thanks

Mamoun

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/b1d02b7d-b555-4625-85a4-b1dac5cf2d4b%40gmail.com.