Re: [isabelle] Custom Isar Commands

Hello Matthew,

the details how to set up a command properly are explained in great detail in "The Isabelle Cookbook" ( in chapter 5.8 (page 98 ff.)

Hope this helps.


On 10/19/2011 03:40 AM, Matthew wrote:
In the first step of building an automatic tool, I am trying to set up
an Isar-level command, following the example of the Nitpick sources.
However, I am having a problem getting Isar to "see" the command.
Here is an utterly simplified version, based on the Nitpick sources.


signature TEST =

structure Test : TEST =

fun test_function a =
   writeln( "test function called" )
   |>  K(K(Toplevel.empty),a)

fun test_params_function a =
   writeln( "test params function called" )
   |>  K(K(Toplevel.empty),a)

val _ = Outer_Syntax.improper_command "test"
             "test the Outer_Syntax.improper_command function"
             Keyword.diag test_function
val _ = Outer_Syntax.command "test_params"
             "test the Outer_Syntax.command function"
             Keyword.thy_decl test_params_function


End file

As far as I can tell, the following Isar code should load the commands
"test" and "test_params" into Isar's syntax:

theory Scratch
imports Main
uses ("")

use ""

However, if I next type test or test_params and try to process it,
ProofGeneral will protest that it cannot find any complete commands to
What am I doing wrong here?

Matthew Weidner

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