[acl2-books] r994 committed - Renamed some lemmas true-listp-explode-nonnegative-integer to...

[acl2-...@googlecode.com]

Revision: 994
Author: kauf...@cs.utexas.edu
Date: Fri Mar 2 10:59:51 2012
Log: Renamed some lemmas true-listp-explode-nonnegative-integer to
true-listp-explode-nonnegative-integer-rewrite in three books named
basic-def.lisp, since a similar lemma of rule class :type-prescription
is provided by the (development version of the) ACL2 system.

http://code.google.com/p/acl2-books/source/detail?r=994

Modified:
/trunk/workshops/1999/pipeline/basic-def.lisp
/trunk/workshops/2000/manolios/pipeline/trivial/basic-def.lisp
/trunk/workshops/2000/manolios/pipeline/trivial/sawada-model/basic-def.lisp

=======================================
--- /trunk/workshops/1999/pipeline/basic-def.lisp Sun Dec 16 16:23:46 2007
+++ /trunk/workshops/1999/pipeline/basic-def.lisp Fri Mar 2 10:59:51 2012
@@ -436,8 +436,10 @@
(implies (and (integerp n) (>= n 0))
(character-listp (explode-nonnegative-integer n print-base nil)))))

+; Renamed by Matt K. after Version 4.3, since a similar :type-prescription
+; lemma is now provided by the ACL2 system. Perhaps it could be deleted
now.
(local
- (defthm true-listp-explode-nonnegative-integer
+ (defthm true-listp-explode-nonnegative-integer-rewrite
(implies (true-listp x)
(true-listp (explode-nonnegative-integer n print-base x)))))

=======================================
--- /trunk/workshops/2000/manolios/pipeline/trivial/basic-def.lisp Sun Dec
16 16:23:46 2007
+++ /trunk/workshops/2000/manolios/pipeline/trivial/basic-def.lisp Fri Mar
2 10:59:51 2012
@@ -436,8 +436,10 @@
(implies (and (integerp n) (>= n 0))
(character-listp (explode-nonnegative-integer n print-base nil)))))

+; Renamed by Matt K. after Version 4.3, since a similar :type-prescription
+; lemma is now provided by the ACL2 system. Perhaps it could be deleted
now.
(local
- (defthm true-listp-explode-nonnegative-integer
+ (defthm true-listp-explode-nonnegative-integer-rewrite
(implies (true-listp x)
(true-listp (explode-nonnegative-integer n print-base x)))))

=======================================
---
/trunk/workshops/2000/manolios/pipeline/trivial/sawada-model/basic-def.lisp
Sun Dec 16 16:23:46 2007
+++
/trunk/workshops/2000/manolios/pipeline/trivial/sawada-model/basic-def.lisp
Fri Mar 2 10:59:51 2012
@@ -436,8 +436,10 @@
(implies (and (integerp n) (>= n 0))
(character-listp (explode-nonnegative-integer n print-base nil)))))

+; Renamed by Matt K. after Version 4.3, since a similar :type-prescription
+; lemma is now provided by the ACL2 system. Perhaps it could be deleted
now.
(local
- (defthm true-listp-explode-nonnegative-integer
+ (defthm true-listp-explode-nonnegative-integer-rewrite
(implies (true-listp x)
(true-listp (explode-nonnegative-integer n print-base x)))))