latest GRD-2005-06-02-UTC-10-16-52-703168 GRD-2005-06-22-UTC-07-23-31-271829 page that defines Mendelsons system S and gives an example of a proof by induction. The page 'cheats' in the sense that all lemmas that I have been too lazy to prove are stated as rules. By the way: stating not yet proved lemmas as rules is quite convenient during development.
Klaus Grue, 2005-06-22