750 *}

   750 *}

   751 

   751 

   752 section {* New Commands and Keyword Files\label{sec:newcommand} *}

   752 section {* New Commands and Keyword Files\label{sec:newcommand} *}

   753 

   753 

   754 text {*

   754 text {*

   756 

   756 

   757   Often new commands, for example for providing new definitional principles,

   757   Often new commands, for example for providing new definitional principles,

   758   need to be implemented. While this is not difficult on the ML-level,

   758   need to be implemented. While this is not difficult on the ML-level,

   759   new commands, in order to be useful, need to be recognised by

   759   new commands, in order to be useful, need to be recognised by

   760   ProofGeneral. This results in some subtle configuration issues, which we

   760   ProofGeneral. This results in some subtle configuration issues, which we

  1006   @{ML Toplevel.local_theory} do?)

  1006   @{ML Toplevel.local_theory} do?)

  1007 

  1007 

  1008   (FIXME read a name and show how to store theorems)

  1008   (FIXME read a name and show how to store theorems)

  1009 *}

  1009 *}

  1010 

  1010 

  1012 

  1012 

  1013 text {*

  1013 text {*

  1014   (FIXME: maybe move to after the tactic section)

  1014   (FIXME: maybe move to after the tactic section)

  1015 

  1015 

  1016   Methods are a central to Isabelle. They are the ones you use for example

  1016   Methods are a central to Isabelle. They are the ones you use for example