trivial output tweaks for vl model command
Merge interface work with Sol
some basic interface tests
Allow documentation fragments in defsection/define

This is a little hack that may give a more convenient way to add a bit of
commentary to a long sections.  For instance, it lets you write things like
this:

   (define frags (x)
     :short "Example of documentation fragments"
     (if (atom x)
	 1
       (+ 1 (frags (cdr x))))
     ///
     "<p>This would be better written as a type-prescription rule:</p>"
     (defthm posp-of-frags
       (posp (frags x)))
     "<p>But this would not make a good type prescription rule:</p>"
     (defthm frags-of-cons
       (equal (frags (cons a x)) (+ 1 (frags x)))))

In the resulting documentation, you'll get these little paragraphs interspersed
with the events in the "Definitions and Theorems" section.

This hasn't been well tested but it seems to work on small examples.
Add new immediate dependency stuff
Merge remote-tracking branch 'remotes/origin/master'
Merge remote-tracking branch 'remotes/jared/doc'
VL: fix a few transforms to behave better w/r/t interfaces; deftypes: add theorems about list/alist-fix of append
VL: bugfix in warning elision, allow consteval of concatenations, change "unique casez (1'b1)" idiom from error to warning in caseelim
merge
merge back
Slight reorganization

 - Move toposort out of VL and into a new centaur/depgraph library
 - Move cons-listp and cons-list-listp out of VL and into std/typed-lists
 - Move some lemmas about intersectp-equal, intersection$, and set-difference$
   out of VL and into std/lists
 - Fix various of hints to deal with the above
 - Rework drop-missing-submodules to use scopestacks
implement transdeps function
merge
Identical defthm events are now redundant.

  A [defthm] or [defaxiom] event is now redundant when there is already
  a syntactically identical event in the logical [world], even if the
  rules suggested by the two [events] differ. See [redundant-events].
  Thanks to Jared Davis and Sol Swords for sending the following
  example, which illustrates the change. Previously, the final event
  was not redundant, and hence failed. Now, it is redundant, even
  though the :typed-term suggested by the new [type-prescription]
  rule is (booleanp (foop x)) where the existing rule's :typed-term
  is (foop x).

    (defund foop (x) (consp x))

    (defthm booleanp-of-foop
      (booleanp (foop x))
      :rule-classes :type-prescription)

    (in-theory (disable booleanp-compound-recognizer))

    (defthm booleanp-of-foop
      (booleanp (foop x))
      :rule-classes :type-prescription)
Minor toothbrush updates, mainly comments.
Removed HTML file generation from bin/make-fancy-manual.sh as per Rager.  Added a comment to note-7-0 that I thought I had already added.
Added fast-rotate.lisp to the bitops library