← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/coi/osets/computed-hints.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/coi/osets/computed-hints.lisp
1
 
#|-*-Lisp-*-=================================================================|#
2
 
#|                                                                           |#
3
 
#|===========================================================================|#
4
 
#|
5
 
 
6
 
   Fully Ordered Finite Sets, Version 0.9
7
 
   Copyright (C) 2003, 2004 by Jared Davis <jared@cs.utexas.edu>
8
 
 
9
 
   This program is free software; you can redistribute it and/or
10
 
   modify it under the terms of the GNU General Public License as
11
 
   published by the Free Software Foundation; either version 2 of
12
 
   the License, or (at your option) any later version.
13
 
 
14
 
   This program is distributed in the hope that it will be useful
15
 
   but WITHOUT ANY WARRANTY; without even the implied warranty of
16
 
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
17
 
   GNU General Public License for more details.
18
 
 
19
 
   You should have received a copy of the GNU General Public Lic-
20
 
   ense along with this program; if not, write to the Free Soft-
21
 
   ware Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
22
 
   02111-1307, USA.
23
 
 
24
 
 
25
 
 
26
 
 computed-hints.lisp
27
 
 
28
 
    We provide support for the development of "pick a point" style
29
 
    proofs through computed hints.
30
 
 
31
 
|#
32
 
 
33
 
(in-package "COMPUTED-HINTS")
34
 
 
35
 
; [Jared] 2014-02-10: changed this book to just be a wrapper for the one in the
36
 
; std/osets library, which was identical modulo whitespace and comments.
37
 
 
38
 
; cert_param: (reloc_stub)
39
 
(include-book "std/osets/computed-hints" :dir :system)