Index of /users/moore/publications/trecia/support

Icon  Name                    Last modified      Size  Description
[DIR] Parent Directory - [TXT] Makefile 03-Apr-2003 13:40 599 [TXT] Makefile-generic 03-Apr-2003 13:40 7.1K [   ] certify.lsp 03-Apr-2003 13:37 3.1K [   ] defpun.cert 03-Apr-2003 13:42 240 [   ] defpun.date 03-Apr-2003 13:41 29 [TXT] defpun.lisp 03-Apr-2003 13:37 17K [   ] defpun.o 03-Apr-2003 13:42 21K [TXT] defpun.out 03-Apr-2003 13:42 9.1K [   ] demo.acl2 03-Apr-2003 13:37 52 [   ] demo.cert 03-Apr-2003 13:45 7.5K [   ] demo.date 03-Apr-2003 13:44 29 [TXT] demo.lisp 03-Apr-2003 13:37 19K [   ] demo.o 03-Apr-2003 13:45 12K [TXT] demo.out 03-Apr-2003 13:45 37K [   ] m5.acl2 03-Apr-2003 13:37 4.2K [   ] m5.cert 03-Apr-2003 13:42 2.3K [   ] m5.date 03-Apr-2003 13:42 29 [   ] m5.lisp 03-Apr-2003 13:37 112K [   ] m5.o 03-Apr-2003 13:42 179K [TXT] m5.out 03-Apr-2003 13:42 53K [   ] utilities.acl2 03-Apr-2003 13:37 50 [   ] utilities.cert 03-Apr-2003 13:44 4.7K [   ] utilities.date 03-Apr-2003 13:42 29 [TXT] utilities.lisp 03-Apr-2003 13:41 5.6K [   ] utilities.o 03-Apr-2003 13:44 2.6K [TXT] utilities.out 03-Apr-2003 13:44 50K [   ] vcg-examples.acl2 03-Apr-2003 13:37 59 [   ] vcg-examples.cert 03-Apr-2003 13:47 7.8K [   ] vcg-examples.date 03-Apr-2003 13:45 29 [TXT] vcg-examples.lisp 03-Apr-2003 13:37 33K [   ] vcg-examples.o 03-Apr-2003 13:47 15K [TXT] vcg-examples.out 03-Apr-2003 13:47 73K
; Tail-Recursive Completion of Inductive Assertions
;  in an Operational Semantics Setting

; J Strother Moore

; This directory contains supporting material for the paper above.
; To recertify the books here, type make to the linux prompt or
; get into ACL2 while standing on this directory and type

; (ld "certify.lsp" :ld-pre-eval-print t)