src/Pure/PIDE/resources.ML
Wed, 26 Mar 2014 09:07:31 +0100 wenzelm superseded by (provide_)parse_files;
Tue, 18 Mar 2014 17:39:03 +0100 wenzelm clarifed module name;
less more (0) tip