Just a reminder (since I changed details in the original posting), my torture chamber for PPDP is tomorrow at 2pm, and I reserved room 166 for it. I'll be talking for 25 minutes on Making Induction Manifest in Modular ACL2. Carl Eastlund