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.