diff options
Diffstat (limited to 'books/workshops/1999/mu-calculus/book/README')
| -rw-r--r-- | books/workshops/1999/mu-calculus/book/README | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/books/workshops/1999/mu-calculus/book/README b/books/workshops/1999/mu-calculus/book/README new file mode 100644 index 0000000..5a28a39 --- /dev/null +++ b/books/workshops/1999/mu-calculus/book/README @@ -0,0 +1,26 @@ +The files in this directory contain the events that appear in the +book. For example, the functions defined here do not have guards. +This directory may be useful for someone who wants to do the +exercises, but does not want to type in the functions presented in the +chapter. In addition, this directory may be useful for someone who +wants to experiment with ACL2 while reading the the book. Eventually, +you will want to look at the "solutions" directory which contains +proofs and guards (and their verification). See "../README" for more +information. + +Because the definitions of some functions depend on solutions to +exercises, some exercise solutions are included (although not noted as +such) in the files in this directory. + +You can use "cert.pl" to certify these books. + +File - Description +--------------------------------------------- +README - This file +sets.lisp - Functions in Section Sets +fast-sets.lisp - Functions in Section Fast-sets +fixpoints.lisp - Functions in Section Fixpoint Theory +relations.lisp - Functions in Section Relation Theory +models.lisp - Functions in Section Models +syntax.lisp - Functions in Section Mu-calculus Syntax +semantics.lisp - Functions in Section Mu-calculus Semantics |