summaryrefslogtreecommitdiff
path: root/books/workshops/2014/russinoff-oleary/support/cert.acl2
diff options
context:
space:
mode:
Diffstat (limited to 'books/workshops/2014/russinoff-oleary/support/cert.acl2')
-rw-r--r--books/workshops/2014/russinoff-oleary/support/cert.acl25
1 files changed, 5 insertions, 0 deletions
diff --git a/books/workshops/2014/russinoff-oleary/support/cert.acl2 b/books/workshops/2014/russinoff-oleary/support/cert.acl2
new file mode 100644
index 0000000..f874bd8
--- /dev/null
+++ b/books/workshops/2014/russinoff-oleary/support/cert.acl2
@@ -0,0 +1,5 @@
+; Copyright (C) 2015, ForrestHunt, Inc.
+; Written by Matt Kaufmann, March, 2015
+; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
+
+(include-book "rtl/rel11/portcullis" :dir :system)