Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-26 22:30:42 -0700 (Sun, 26 Jun 2005)
Revision: 7432
Log message:
Simplified the theory a bit to better match the FOL tutorial:
- Use "open Basic_tactics" instead of a bunch of seemingly random "open"
statements for refiner/tactic_type/dtactic/etc modules.
- unfold_not is a definition, not a prim_rw.