1
; Copyright (C) 2014, ForrestHunt, Inc.
2
; Written by Matt Kaufmann, November, 2014
3
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
5
(certify-book "make-toothbrush" ? t :ttags (:make-toothbrush))
7
; cert-flags: ? t :ttags (:make-toothbrush)