; Copyright (C) 2000 Panagiotis Manolios ; This program is free software; you can redistribute it and/or modify ; it under the terms of the GNU General Public License as published by ; the Free Software Foundation; either version 2 of the License, or ; (at your option) any later version. ; This program is distributed in the hope that it will be useful, ; but WITHOUT ANY WARRANTY; without even the implied warranty of ; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ; GNU General Public License for more details. ; You should have received a copy of the GNU General Public License ; along with this program; if not, write to the Free Software ; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. ; Written by Panagiotis Manolios who can be reached as follows. ; Email: pete@cs.utexas.edu ; Postal Mail: ; Department of Computer Science ; The University of Texas at Austin ; Austin, TX 78701 USA #| What constitutes an instruction. |# (in-package "ACL2") (defun Inst (opcode rc ra rb) (list 'Inst opcode rc ra rb)) (defmacro Inst-opcode () 1) (defmacro Inst-rc () 2) (defmacro Inst-ra () 3) (defmacro Inst-rb () 4)