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 ---------------------------------------------------------------------------- _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev