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
