src/Pure/pure_syn.ML
2012-08-23 wenzelm 2012-08-23 clarified type Token.file;
2012-08-23 wenzelm 2012-08-23 simplified Thy_Load.provide: do not store full path;
2012-08-22 wenzelm 2012-08-22 clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
2012-08-22 wenzelm 2012-08-22 clarified bootstrapping of Pure;