added offset/end_offset;

tuned formatting;

clean up dead code

made SML/NJ happy;

FundefLib.try_proof : attempt a proof and see if it works

added lemmas

inner_syntax markup is back;

disabled inner_syntax markup for now;

added read_token -- with optional YXML encoding of position; tuned parse operations: print position instead of echoing input (now encoded!); do not export obsolete read operation;

parse_token: use Syntax.read_token, pass full position information;