src/Pure/Syntax/scan.ML
Mon, 09 Mar 1998 16:12:19 +0100 wenzelm Generic scanners (for potentially infinite input) -- replaces Scanner;
less more (0) tip