Tue, 25 Jan 2011 12:14:31 +0000 zhang 1. Myhill.thy is proved to correct some typos. 2. Some sections are added to the first direction. 3. The small theory of list difference is now separated into Prefix_subtract.thy and the ROOT.ML
(0) -30 -10 -1 +1 +10 +30 +100 +300 tip