[isabelle] Request for TTP and PTT Interfaces

Hello everyone,
what also could be useful for my current project are human language interfaces, which transform proofs into readable text and vice versa. Is that already possible for Isabelle or even done?
[I do not dare to ask for natural language interfaces, I only mean texts in a controlled language.]
Happy reasoning,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.