Add `(in-package "ACL2")` lines.HEADmaster

13 files changed, 23 insertions, 1 deletions

diff --git a/L-99.lisp b/L-99.lisp
index 3c8dc71..b1854fc 100644
--- a/L-99.lisp
+++ b/L-99.lisp
@@ -1,3 +1,5 @@
+(in-package "ACL2")
+
 ;; P01 (*) Find the last box of a list.
 (defun my-last (x)
   (declare (xargs :guard (and (true-listp x)
diff --git a/binary-tree.lisp b/binary-tree.lisp
index b26b8fb..aab189d 100644
--- a/binary-tree.lisp
+++ b/binary-tree.lisp
@@ -1,3 +1,5 @@
+(in-package "ACL2")
+
 (defun emptyp (x)
  (atom x))
 
diff --git a/combinations.lisp b/combinations.lisp
index 93c3b67..9495676 100644
--- a/combinations.lisp
+++ b/combinations.lisp
@@ -1,3 +1,5 @@
+(in-package "ACL2")
+
 (defun cons-all (e x)
   (declare (xargs :guard (true-listp x)))
   (if (endp x)
diff --git a/consecutive-fibonacci-numbers-are-coprime.lisp b/consecutive-fibonacci-numbers-are-coprime.lisp
index af0a534..0146dc1 100644
--- a/consecutive-fibonacci-numbers-are-coprime.lisp
+++ b/consecutive-fibonacci-numbers-are-coprime.lisp
@@ -1,4 +1,5 @@
-;; consecutive-fibonacci-numbers-are-coprime.lisp: 隣り合うフィボナッチ数は互いに素である
+;;; consecutive-fibonacci-numbers-are-coprime.lisp: 隣り合うフィボナッチ数は互いに素である
+(in-package "ACL2")
 
 ;; 数字を足したり引いたりする関数に関する証明をするときに便利な Book
 (include-book "arithmetic/top-with-meta" :dir :system)
diff --git a/divisor-list.lisp b/divisor-list.lisp
index 21cbb10..20d2793 100644
--- a/divisor-list.lisp
+++ b/divisor-list.lisp
@@ -1,4 +1,5 @@
 ;;; divisor-list.lisp: 約数に関する証明
+(in-package "ACL2")
 
 ;; e が x の約数であるかどうかを調べる述語
 (defmacro divisorp (e x)
diff --git a/fast-expt.lisp b/fast-expt.lisp
index 3318946..d3fb779 100644
--- a/fast-expt.lisp
+++ b/fast-expt.lisp
@@ -1,3 +1,5 @@
+(in-package "ACL2")
+
 (defmacro square (x)
   `(* ,x ,x))
 
diff --git a/flist.lisp b/flist.lisp
index dc6ffe7..8e38395 100644
--- a/flist.lisp
+++ b/flist.lisp
@@ -1,3 +1,5 @@
+(in-package "ACL2")
+
 (defun true-flistp (x)
   (if (endp x)
       (null x)
diff --git a/list-monad.lisp b/list-monad.lisp
index f7a6425..56a79dd 100644
--- a/list-monad.lisp
+++ b/list-monad.lisp
@@ -1,5 +1,6 @@
 ;;; list-monad.lisp
 ;;; ACL2 でリストモナドがモナド則を満たしていることを示す
+(in-package "ACL2")
 
 ;; ACL2 では第一級の関数は使えないため、値としての関数は連想リストで表現する
 ;; ACL2 には apply$ という限定的な高階関数を実現する機能があるがよく分かってい
diff --git a/palindrome-sandwich.lisp b/palindrome-sandwich.lisp
index 98f5e64..b2d2a9d 100644
--- a/palindrome-sandwich.lisp
+++ b/palindrome-sandwich.lisp
@@ -7,6 +7,7 @@
 ;;;                 (true-listp y))
 ;;;            (equal (palindromep (app y (app x (rev y))))
 ;;;                   (palindromep x))))
+(in-package "ACL2")
 
 ;; 二つのリストを連結する
 (defun app (x y)
diff --git a/peano.lisp b/peano.lisp
index 8fedc56..9ea24ba 100644
--- a/peano.lisp
+++ b/peano.lisp
@@ -1,3 +1,5 @@
+(in-package "ACL2")
+
 (defmacro zero? (x)
   `(equal ,x nil))
 
diff --git a/permutations.lisp b/permutations.lisp
index d75a4d2..ef843ba 100644
--- a/permutations.lisp
+++ b/permutations.lisp
@@ -1,3 +1,5 @@
+(in-package "ACL2")
+
 (defun mapcar-cons (e x)
   (declare (xargs :guard (true-listp x)))
   (if (endp x)
diff --git a/pigeonhole.lisp b/pigeonhole.lisp
index 91c221f..23b8637 100644
--- a/pigeonhole.lisp
+++ b/pigeonhole.lisp
@@ -1,3 +1,5 @@
+(in-package "ACL2")
+
 (defun member-if-over-1 (x)
   (cond ((endp x) nil)
         ((< 1 (car x)) x)
diff --git a/units.lisp b/units.lisp
index 4b353e1..8533509 100644
--- a/units.lisp
+++ b/units.lisp
@@ -1,3 +1,5 @@
+(in-package "ACL2")
+
 (defun m (x)
   x)