title: completely replace the inner syntax in isar?
body: <p>I am interested in using Isar as a meta language for writing formal proofs about <a href="http://jsoftware.com/help/primer/start_here.htm" rel="noreferrer">J</a>, an executable math notation and programming language, and I'd like to be able to use J as the inner syntax.</p>
  
  <p>J consists of a large number of <a href="http://jsoftware.com/help/dictionary/vocabul.htm" rel="noreferrer">primitives</a>, and assigns (multiple!) meanings to every ASCII character, including single and double quotes.</p>
  
  <p>Where can I find documentation or example code for implementing a completely new inner syntax? Or is this even possible? (I've been looking around in the <code>src/</code> directory, but it's somewhat overwhelming and I'm not entirely sure what I'm looking for.)</p>