; A simple example of a book directory ; Copyright (C) 2006 University of Texas at Austin ((:FILES ; non-empty list of filenames, generated from Unix command "ls -1R" " .: Makefile Readme.lsp sub.lisp top.lisp ") (:TITLE "A simple example of a book directory") (:AUTHOR/S "E. Cartman") ; non-empty list of author strings (:KEYWORDS ; non-empty list of keywords, case-insensitive "book contributions" "contributed books") (:ABSTRACT " This directory illustrates the structure of contribution to ACL2's set of certifiable books. This directory is particularly simple, in that it is without subdirectories.") (:PERMISSION ; author/s permission for distribution and copying: "Simple example 1 Copyright (C) 2006 Joe User and Aunt Acid This program is free software; you can redistribute it and/or modify it under the terms of Version 2 of the GNU General Public License as published by the Free Software Foundation. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA."))