CODEWITHSUNDEEP
isabelleml
Fadoua
Fadoua

Reputation: 171

ML-programming in Isabelle: could not find some of the built-in functions and tactics

I am studying the "Isabelle Cookbook" to write ML code in Isabelle.

Unfortunately, many of the examples do not work because built-in functions were not found (name changed? the path structure.fct should be specified?). For instance, the examples that use etac, rtac and atac are not working anymore. What are the new names and how do I find them by myself?

Upvotes: 2

Views: 108

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8298

The Isabelle cookbook always had a very unofficial status and I would suspect that it is now severely outdated. There is some nice information in there, but the ‘official’ an up-to-date source is the Isabelle implementation manual.

To find out the names of things that have been renamed, it can often be useful to look in the NEWS file, e.g. in this case:

* Old tactic shorthands atac, rtac, etac, dtac, ftac have been
discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
instead (with proper context).

You can find those in ~~/src/Pure/tactic.ML. If you're looking for some ML functions, just search the ~~/src/Pure/ directory and that's usually where they are. jEdit's hyper search is particularly useful for this.

Upvotes: 3

Related Questions