Re: [isabelle] Custom Isar Commands



Hi,

Makarius writes:
 > 
 >    * The Isabelle/jEdit Prover IDE, which is particulaly nice for ML
 >      development (as of Isabelle2011-1), requires some trickery though
 >      to make it accept newly created Isar commands dynamically at runtime.

Out of interest, how does this trickery work concretely?

Thanks,
Christian





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