Add (unused) entrypoints to DefnBase for registering definitions

Also entry-points for storing induction principles to accompany them.

Up to hol.state0

doc page for type conv

also more doc changes to ..._CONV pages, reflecting use of UNCHANGED

Move lcsymtacs functions to natural homes

For example, we do not need to have >> in lcsymtacs; it might as be in
Tactical. The ultimate aim is to do away with lcsymtacs entirely.

This is work towards github issue #274

list_tactic concept

introduce list_tactic - works on a list of goals, not a single goal
THEN_LT (tac1, ltac2 : list_tactic),
A tactical that applies ltac2 to the list of subgoals resulting from tac1
TACS_TO_LT (tac2l: tactic list) : list_tactic
ALLGOALS - A list_tactic which applies a given tactic to all goals
ALL_LT - always succeeds
NTH_GOAL - applies tactic to nth goal of list
REVERSE_LT - A list_tactic that reverses a list of subgoals
SPLIT_LT - apply two list-tactics, one to first n subgoals,
the other to the rest
ROTATE_LT - rotate the list of subgoals by n positions

Change src/bool to src/1 as a prelude to experimentation!