/usr/share/acl2-6.5/books/ihs/ihs-lemmas.lisp is in acl2-books-source 6.5-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 | ; ihs-lemmas.lisp -- a top-level book INCLUDEing the IHS lemmas
; Copyright (C) 1997 Computational Logic, Inc.
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
;;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
;;;
;;; ihs-lemmas.lisp
;;;
;;; The top-level book of lemmas in the IHS (Integer Hardware
;;; Specification) library.
;;;
;;; Bishop Brock
;;; Computational Logic, Inc.
;;; 1717 West 6th Street, Suite 290
;;; Austin, Texas 78703
;;; brock@cli.com
;;;
;;; Modified for ACL2 Version_2.7 by:
;;; Matt Kaufmann, kaufmann@cs.utexas.edu
;;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(in-package "ACL2")
(include-book "math-lemmas")
(include-book "quotient-remainder-lemmas")
(include-book "logops-lemmas")
(deflabel ihs-lemmas
:doc ":doc-section ihs
A simple interface to the books of lemmas in the IHS libaray.
~/~/
Including the \"ihs-lemmas\" book includes all of the books of lemmas in
the IHS library. This book must always be included after the
\"ihs-definitions\" book, e.g.,
(INCLUDE-BOOK
\"ihs-definitions\")
(LOCAL (INCLUDE-BOOK
\"ihs-lemmas\"))
The above sequence extends the theory that existed before the inclusion of
the books with those definitions and lemmas provided be the included books.
To continue in a minimal theory that contains only the IHS libraries,
invoke the macro MINIMAL-IHS-THEORY, e.g.,
(LOCAL (MINIMAL-IHS-THEORY))~/")
(defmacro minimal-ihs-theory ()
":doc-section ihs-lemmas
Set up a minimal theory based on the IHS library.
~/~/
Executing the macro call
(MINIMAL-IHS-THEORY)
will set up a minimal theory based on the theories exported by the books in
the IHS libraries. This is the preferred way to use the IHS library.~/"
`(PROGN
(IN-THEORY NIL)
(IN-THEORY
(ENABLE
BASIC-BOOT-STRAP ; From "ihs-theories"
IHS-MATH ; From "math-lemmas"
QUOTIENT-REMAINDER-RULES ; From "quotient-remainder-lemmas"
LOGOPS-LEMMAS-THEORY ; From "logops-lemmas"
INTEGER-RANGE-P ; new for Version_2.7; added by Matt
; Kaufmann, as suggested by Matt Wilding
))))
|