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
some new doc files to do with list_tactics
changed list_tactic to list-tactic in doc files, where not the ML type
replacing code for THEN and THENL using ALLGOALS and TACS_TO_LT

also defines NULL_OK_LT to implement change to THENL
(see https://github.com/HOL-Theorem-Prover/HOL/issues/214 )
Merge pull request #210 from jeremydaw/trial

Implementation of the list_tactic concept.