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

[Makarius]

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.


 	Makarius

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