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

Fix examples/category for tight equality

Reconcile store_thms with diverging names in db and val binding

Fixes to category theory example in light of 92317114

remove TruePrefix from category theory example

minor changes (to discrete_cat) in category theory example

Update to category theory example.

Main new result is a Yoneda embedding into the category of zfset-valued
presheaves, whose properties are (mostly) simply inherited from the
simpler embedding into the category of (predicate-)set-valued
presheaves.

More work on categoryTheory example

Highlights include:
- proof that an embedding is essentially injective on objects
- one direction of the proof that an equivalence of categories is full,
faithful, and essentially surjective on objects
- proof that the binary product functor is a functor; characterization
of binary products

Major reworking of categoryTheory example

Major changes include:

- Reuse a polymorphic type of "morphisms" for morphisms in a category as
well as for functors and natural transformations. The category record
no longer has dom and cod fields.

- Only store the id_map in a category (and the comp map) because the dom
and cod of these morphisms is forced.

- O'Keefe style treatment of the category of sets: have a separate
category of sets for each HOL type (so really a subcategory of the
real category of sets). Have not yet linked this up with a
Katovsky-style zfset theory (would want to exhibit embeddings).

- Use overloading and Parse rules for nicer syntax.

- Split category theory into category, functor, and nat_trans theories.

- Make many (all?) partial functions extensional, that is, explicitly
set to ARB outside their domain (so that they are comparable).

- Use the constants 'full' and 'faithful' and (new) 'inj_obj' to
characterize the Yoneda embedding. Katovsky said it was injective on
objects in "YonedaEmbedding", which is the wrong term.

- Start a theory of limits (barely started).

Finish reproving Katovsky's category theory

Culminates in proof of the Yoneda lemma, and then that the Yoneda
functor is full and faithful and an embedding.

Haven't included his stuff on monadic equational logic.
Next thing to do would probably be limits.

category theory up to definition of set-valued hom functors

(Squashed commit of the following:
Merge branch 'master' into category
show what contra_hom_functor does on objects and morphisms
remove looping rewrites and open boolLib
define (set-valued) hom_functor and prove it is a functor
add theorems to ease access to two category axioms
start set_catTheory, prove set_cat is a category
prove IdFn is identity for ComposeFn
also add a version of ExtFn suitable for match_mp
finish up to end of functor categories
up to that composition of natural transformations is natural
Merge branch 'master' into category
define natural transformations
Continue translating Katovksy's category theory)

Continue translating Katovksy's category theory

Finished his Natural Transformation theory, which includes the
definition of functor categories.

Continue translating Katovksy's category theory

Finished his Functor theory, but skipped Universe and Monadic Equational
Theory.

Finish translating Katovsky's first theory about categories

(there are six more in his Isabelle development)
This includes definition of category, various theorems about
isomorphisms and inverses, and examples of the unit category and the
opposite category.

Rework category theory to follow Alexander Katovsky's (in Isabelle) more closely

(http://afp.sourceforge.net/entries/Category2.shtml)

start category theory example - nothing in it yet

just define a record for categories and a predicate over it