remove lcsymtacs (github issue #666)

The lcsymtacs structure is regarded superseded as it plainly is
a shorthand for opening the following modules:
Abbrev HolKernel boolLib Tactic Tactical BasicProvers simpLib
Rewrite bossLib Thm_cont

Clean up context-free/grammar a little

Deal with rebindings of ptree_{size,fringe}_def in grammarScript

Ability to EVAL these constants is lost because of b98f5ead5

Not sure that anybody ever used this, but still. With regression
test.

Define valid_lptree constant (from CakeML).

This constant asserts that the parse tree respects the provided
grammar (as per valid_ptree), but also that every non-terminal node in
the tree has the correct locations recorded (derived from the
locations of the sub-trees, using the merge_list_locs constant.

Remove trailing whitespace in grammarScript.sml

Define real_fringe constant and prove some properties (from CakeML)

The simpler ptree_fringe returns just the tokens; real_fringe returns
the actual fringe, which couples the tokens with their locations.

Try a slightly different approach to handling locations in parse trees

Location from parse_tree

Location in parser done (up to a cheat)

Fix CFG theories in light of pat_assum rename

playground for formal language theory developments.