[isabelle] New commands in Isabelle2012
I am trying to define a custom Isar command in Isabelle 2012. I am
using the following example from Christian Urban's cookbook:
val do_nothing = Scan.succeed (Local_Theory.background_theory I)
val kind = Keyword.thy_decl
Outer_Syntax.local_theory ("foobar", kind) "description of foobar"
However, I always get the error message:
*** Undeclared outer syntax command "foobar"
Anybody know what I am doing wrong?
This archive was generated by a fusion of
Pipermail (Mailman edition) and