← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/make-event/Readme.lsp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/make-event/Readme.lsp
67
67
    certify.
68
68
  portcullis-expansion.lisp
69
69
  portcullis-expansion-include.lisp
70
 
 
 
70
+ stobj-test.lisp
 
71
    Illustrates the use of stobjs during make-event expansion.
 
72
+ dotimes.lisp
 
73
    Defines a dotimes$ macro and provides an example.
 
74
+ logical-tangent.lisp
 
75
    Provides a wormhole-like capability, where you can experiment for awhile
 
76
    and then the built-in part of the state, including the logical world, will
 
77
    be reverted.
71
78
 
72
79
The rest of this file is metadata for the ACL2 system.
73
80
 
93
100
basic.lisp
94
101
defconst-fast-examples.lisp
95
102
defconst-fast.lisp
 
103
dotimes.lisp
96
104
embedded-defaxioms
97
105
embedded-defaxioms.acl2
98
106
embedded-defaxioms.lisp
106
114
gen-defun.lisp
107
115
local-requires-skip-check-include.lisp
108
116
local-requires-skip-check.lisp
 
117
logical-tangent.lisp
109
118
macros-include.lisp
110
119
macros-skip-proofs-include.acl2
111
120
macros-skip-proofs-include.lisp
122
131
read-from-file-data-mod.lsp
123
132
read-from-file-data.lsp
124
133
read-from-file.lisp
 
134
stobj-test.lisp
125
135
test-case-check.lisp
126
136
test-case.lisp
127
137
 
143
153
local-defaxiom-2.lisp
144
154
")
145
155
 (:TITLE    "Examples illustrating the use of make-event")
146
 
 (:AUTHOR/S "M. Kaufmann" "J Moore") ; non-empty list of author strings
 
156
 (:AUTHOR/S "M. Kaufmann" "J Moore" "David Rager" "Peter Dillinger")
147
157
 (:KEYWORDS ; non-empty list of keywords, case-insensitive
148
158
   "make-event" "assert!" "assert!!" "must-fail" "must-succeed" "must-eval-to"
149
 
   "must-eval-to-t" "test-case")
 
159
   "must-eval-to-t" "test-case" "dotimes$" "logical-tangent")
150
160
 (:ABSTRACT "
151
161
The .lisp files in this directory illustrate a number of potential
152
162
uses of make-event.  In particular, eval.lisp defines some macros
154
164
are many other examples as well.")
155
165
  (:PERMISSION ; author/s permission for distribution and copying:
156
166
"make-event
157
 
Copyright (C) 2006 Matt Kaufmann and J Moore
 
167
Copyright (C) 2006 University of Texas at Austin
 
168
for files not explicitly copyrighted otherwise
158
169
 
159
170
This program is free software; you can redistribute it and/or
160
171
modify it under the terms of the GNU General Public License