; ihs-init.acl2 -- helper for ihs-init.lisp certification
; Copyright (C) 1997  Computational Logic, Inc.

; This file is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.

; This book 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 book; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

; If you're looking at this file because something is blowing up, what you
; probably have to do is change the path below to point to the place where
; the U package definition is for your system.  When you installed the system
; it was in ...<acl2 stuff>.../books/data-structures.

(acl2::value :q)
(acl2::lp)
(ld '((ubt! 1)
      (ld "../data-structures/define-u-package.lisp")
      (certify-book "ihs-init" 1)))