Included Books
other
(in-package "ACL2")
include-book
(include-book "deftutorial")
other
(deftutorial my-tutorial "My tutorial")
other
(def-my-tutorial-top (parent1 parent2) (p "one") (p "two"))
other
(def-my-tutorial-page first "The first thing." (p "A") (p "B") (p "C"))
other
(def-my-tutorial-page second "The second thing." (p "para1") (p "para2") (p "para3"))
other
(def-my-tutorial-page third "The third thing." (p "text"))
other
(def-my-tutorial-topics)