An introductory guide, recommended for new users of gl.
This is a tutorial introduction to using GL to prove ACL2 theorems. We recommend going through the entire tutorial before beginning to use GL.
You can think of this tutorial as a quick-start guide. By the time you're done with it, you should have a good understanding of how GL works, and be able to use GL to easily prove many theorems.