Is there any Isar command for IsaScheme at the moment?
At the moment, there is no Isar support within IsaScheme. All commands must be performed using direct calls to the ML API inside a 'setup' block.
e.g .
setup {* Definitions.explore_definitions ["zero","%x. True","%x. False","suc"] *}
I will work hard to give support to the most natural Isar language.
Log in to post a comment.
At the moment, there is no Isar support within IsaScheme. All commands must
be performed using direct calls to the ML API inside a 'setup' block.
e.g .
setup {* Definitions.explore_definitions ["zero","%x. True","%x.
False","suc"] *}
I will work hard to give support to the most natural Isar language.