[isabelle] Latex / Isabelle (Beginner)

Hello all,

I am new to extracting Latex files from Isabelle files. I read the
documentation but does not make sense to me. It says to use 'isabelle mkdir
NAME', but where do I even type this in? A terminal? Isabelle? Within a
file? Which?
I'm so confused.

Any help would be greatly appreciated.

Thank you so much.

Nemo Curiel

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