[isabelle] New commands in Isabelle2012



Hi all,

I am trying to define a custom Isar command in Isabelle 2012. I am
using the following example from Christian Urban's cookbook:

ML {*
      let
        val do_nothing = Scan.succeed (Local_Theory.background_theory I)
        val kind = Keyword.thy_decl
      in
        Outer_Syntax.local_theory ("foobar", kind) "description of foobar"
                                  do_nothing
      end
*}

However, I always get the error message:

 *** Undeclared outer syntax command "foobar"
 ***

Anybody know what I am doing wrong?

Thanks,

Omar.





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