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)