[isabelle-dev] Experiments in best-first-search rewriter

Makarius makarius at sketis.net
Mon Nov 3 10:51:17 CET 2014

On Sun, 2 Nov 2014, Bohua Zhan wrote:

> Two examples are given at the end: the first refers to the permutation
> example in section 6.4 of the new Isabelle Cookbook manual, rewriting:

Note that the Isabelle Cookbok is not really "new".  It is useful to get 
started in some areas of Isabelle/ML usage, but it also contains many 
things that are old, or outright misleading.

You need to take other information into account as well, and develop a 
sense of (un)reliability of certain information.

The official "implementation" manual is the main starting point for using 
Isabelle/ML. Using Isabelle/ML is not yet an Isabelle development 
activity, so it can be discussed on isabelle-users -- unless you want to 
propose concrete changes to ongoing repository versions.


                   http://stop-ttip.org  777,535 people so far

More information about the isabelle-dev mailing list