← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/1999/ivy/ivy-v2/ivy-sources/exercises/exercise1.lsp

  • 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/workshops/1999/ivy/ivy-v2/ivy-sources/exercises/exercise1.lsp
 
1
;; Exercise file to accompany 
 
2
;;
 
3
;; Ivy: A Preprocessor and Proof Checker for First-order Logic
 
4
;;
 
5
;; William McCune (mccune@mcs.anl.gov)
 
6
;; Olga Shumsky (shumsky@ece.nwu.edu)
 
7
;;
 
8
;; Startup file for exercise 1.
 
9
;;
 
10
;; Define a function to check whether a given variable occurs
 
11
;; freely in a formula.  Prove that substitution for a variable
 
12
;; that does not occur in the formula has no effect.
 
13
 
 
14
;; All neccesary definitions are in:
 
15
(include-book "../base")
 
16