anchor.diff:    1)
   
   ;;; ========================================================================
  +;;;   SORT DECLARATION
  +;;;   http://www.specware.org/manual/html/sorts.html
  +;;; ========================================================================
  +
  +(define-sw-parser-rule :SORT-DEF-RHS () ; as in rhs of  T x = | A x | B x
  +  (:anyof
  +   ;; these are sort abbreviations, not 
  +   (1 :TYPE-ABBREVIATION  :documentation "Type abbreviation") 
  +   (1 :RAW-SUBTYPE        :documentation "Subtype")         ; Allow unparenthesized subtype at top level: "Foo | q?"
  +   (1 :SORT               :documentation "Function sort")   ; All other sorts, including "(Foo | q?)"
  +   )
  +  1)
  +
  +;;; ========================================================================
  +;;;   TYPE ABBREVIATION
  +;;;   A type abbreviation is not a true type -- it is syntax for declaring 
  +;;;   constructors, etc.
  +;;; ========================================================================
  +
  +(define-sw-parser-rule :TYPE-ABBREVIATION () 
  +  ;; these are type abbreviations, not true types
  +  (:anyof
  +   (1 :SUM-TYPE          :documentation "Co-product sort") ; "(| Foo Nat | Bar String)"
  +   (1 :RAW-SUM-TYPE      :documentation "Co-product sort") ; "| Foo Nat | Bar String"
  +   (1 :QUOTIENT-TYPE     :documentation "Sort quotient")   ; "(Foo / q?)"
  +   (1 :RAW-QUOTIENT-TYPE :documentation "Sort quotient")   ; "Foo / q?"
  +   )
  +  1)
  +
  +;;; ------------------------------------------------------------------------
  +;;;   SUM-TYPE  (Not a true type!)
  +;;; ------------------------------------------------------------------------
  +;;;   NOTE: SUM-TYPE is only an alternative for :TYPE-ABBREVIATION,
  +;;;         and cannot be used elsewhere.
  +
  +(define-sw-parser-rule :SUM-TYPE ()
  +  (:tuple "(" (1 :RAW-SUM-TYPE) ")")
  +  1)
  +
  +(define-sw-parser-rule :RAW-SUM-TYPE ()
  +  (:tuple (1 (:repeat+ :TYPE-SUMMAND nil)))
  +  (make-sort-sum 1 ':left-lcb ':right-lcb))
  +
  +(define-sw-parser-rule :TYPE-SUMMAND ()
  +  (:tuple "|" (1 :CONSTRUCTOR) (:optional (2 :SLACK-SORT)))
  +  (make-sort-summand 1 2 ':left-lcb ':right-lcb))
  +
  +(define-sw-parser-rule :CONSTRUCTOR ()
  +  :NAME)
  +
  +;;; ------------------------------------------------------------------------
  +;;;   QUOTIENT-TYPE  (Not a true type!)
  +;;; ------------------------------------------------------------------------
  +;;;   NOTE: QUOTIENT-TYPE is only an alternative for :TYPE-ABBREVIATION,
  +;;;         and cannot be used elsewhere.
  +
  +(define-sw-parser-rule :QUOTIENT-TYPE ()
  +  (:tuple "(" (1 :RAW-QUOTIENT-TYPE) ")")
  +  1)
  +
  +(define-sw-parser-rule :RAW-QUOTIENT-TYPE ()
  +  ;; TODO: [still relevant given above?] 
  +  ;;       In doc: sort-quotient relation is expression, but that's ambiguous -- need tight-expression 
  +  (:tuple (1 :CLOSED-SORT) "/" (2 :TIGHT-EXPRESSION)) ; CLOSED-EXPRESSION?
  +  (make-sort-quotient 1 2 ':left-lcb ':right-lcb) :documentation "Quotient")
  +
  +;;; ========================================================================
   ;;;   SORT
   ;;;   http://www.specware.org/manual/html/sorts.html
   ;;; ========================================================================
  -
  -(define-sw-parser-rule :SORT-DEF-RHS () ; as in rhs of  T x = | A x | B x
  -  (:anyof
  -   (1 :SORT-SUM                :documentation "Co-product sort")
  -   (1 :SORT-QUOTIENT           :documentation "Sort quotient")
  -   (1 :SORT                    :documentation "Function sort")
  -   )
  -  1)
   
   (define-sw-parser-rule :SORT () ; anywhere
     (:anyof
  
positive.code:   (make-sort-arrow 1 2 ':left-lcb ':right-lcb))
  
  (define-sw-parser-rule :ARROW-SOURCE ()
    (:anyof :SORT-SUM :SLACK-SORT))
  
  ;;; ------------------------------------------------------------------------
  ;;;   SORT-PRODUCT
  
negative.code:   1)
  
  ;;; ------------------------------------------------------------------------
  ;;;   SORT-ARROW
  ;;; ------------------------------------------------------------------------
  
  