Integrate environment with Isabelle

ggrov / tinker

Graph based proof strategy language

http://ggrov.github.io/tinker/

6 stars 0 forks source link

Open ggrov opened 9 years ago

ggrov commented 9 years ago

[ ] add support to instantiate terms/thms/cterms using (Isabelle's) environment
[ ] be able to insert our string->term bindings into Isabelle's environment
[ ] be able to lookup (using string) a maplet from Isabelle's env and add this to our environment as a string-> term binding

ggrov commented 9 years ago

This will be required for examples in AI4FM book