diff --git a/collects/unstable/redex.rkt b/collects/unstable/redex.rkt
new file mode 100644
index 0000000000..fc83399698
--- /dev/null
+++ b/collects/unstable/redex.rkt
@@ -0,0 +1,356 @@
+#lang racket
+(require racket/contract
+         redex/reduction-semantics
+         redex/pict
+         slideshow/pict
+         racket/list)
+
+;; TO DO:
+;; - chained binary operators
+;;   eg (+ 1 2 3) => "1 + 2 + 3"
+;; - helper for thin spaces around operators/functions ?
+;; - rewriters for more conventions (eg subst, env, judgments, ...)
+
+(provide
+ (contract-out
+  ;; Using and controlling rewriters
+  [with-rewriters
+   (-> (-> any) any)]
+  [current-atomic-rewriters
+   (parameter/c (plistof symbol? atomic-rewriter/c))]
+  [current-compound-rewriters
+   (parameter/c (plistof symbol? compound-rewriter/c))]
+  [current-unquote-rewriters
+   (parameter/c (plistof (-> lw? any/c) (-> lw? lw?)))]
+  [add-atomic-rewriters!
+   (->* [] [] #:rest (plistof symbol? atomic-rewriter/c)
+        void?)]
+  [add-compound-rewriters!
+   (->* [] [] #:rest (plistof symbol? compound-rewriter/c)
+        void?)]
+  [add-unquote-rewriters!
+   (->* [] [] #:rest (plistof (-> lw? any/c) (-> lw? lw?))
+        void?)]
+  ;; Rewriter constructors
+  [only-first-rw
+   (-> compound-rewriter/c)]
+  [binary-rw
+   (->* [content/c]
+        [#:parenthesize-arg (or/c #t #f (listof symbol?) (-> lw? any/c))
+         #:parenthesize-left (or/c #t #f (listof symbol?) (-> lw? any/c))
+         #:parenthesize-right (or/c #t #f (listof symbol?) (-> lw? any/c))]
+        compound-rewriter/c)]
+  [prefix-rw
+   (-> content/c
+       compound-rewriter/c)]
+  [postfix-rw
+   (-> content/c
+       compound-rewriter/c)]
+  [function-rw
+   (-> content/c
+       compound-rewriter/c)]
+  [splice-rw
+   (-> compound-rewriter/c)]
+  [constant-rw
+   (-> content/c
+       compound-rewriter/c)]
+  [bracket-rw
+   (->* [(or/c 'round 'square 'curly 'angle (list/c (or/c string? pict?) (or/c string? pict?)))]
+        [#:comma? any/c]
+        compound-rewriter/c)]
+  [set-cons-rw
+   (-> compound-rewriter/c)]
+  ;; Contracts
+  [compound-rewriter/c
+   contract?]
+  [plistof
+   (-> contract? contract? contract?)]
+  #|
+  [content/c
+   contract?]
+  |#))
+
+(define (plistof key/c val/c)
+  (letrec ([ctc
+            (recursive-contract
+             (or/c '()
+                   (cons/c key/c (cons/c val/c ctc))))])
+    ctc))
+
+(define content/c
+  (or/c string? pict? lw? (-> (or/c string? pict? lw?))))
+
+(define atomic-rewriter/c
+  (or/c string? pict? (-> (or/c string? pict?))))
+
+(define compound-rewriter/c
+  (-> (listof lw?)
+      (listof (or/c string? pict? lw?))))
+
+;; ============================================================
+
+(define current-atomic-rewriters (make-parameter null))
+(define current-compound-rewriters (make-parameter null))
+(define current-unquote-rewriters (make-parameter null))
+
+(define (add-atomic-rewriters! . args)
+  (push-rewriters! 'add-atomic-rewriters! current-atomic-rewriters args))
+(define (add-compound-rewriters! . args)
+  (push-rewriters! 'add-compound-rewrites! current-compound-rewriters args))
+(define (add-unquote-rewriters! . args)
+  (push-rewriters! 'add-unquote-rewrites! current-unquote-rewriters args))
+
+(define (with-rewriters thunk)
+  (with-atomic-rewriter*
+   (lambda ()
+     (with-compound-rewriter*
+      (lambda ()
+        (with-unquote-rewriter*
+         (lambda ()
+           (thunk))
+         (reverse (current-unquote-rewriters))))
+      (reverse (current-compound-rewriters))))
+   (reverse (current-atomic-rewriters))))
+
+;; ============================================================
+
+(define (push-rewriters! who param args)
+  (unless (even? (length args))
+    (error who "expected even number of arguments, got: ~e" args))
+  (param (append args (param))))
+
+;; Note: l is reversed, so rewriter comes first, symbol/pred comes second.
+(define (with-atomic-rewriter* thunk l)
+  (if (null? l)
+      (thunk)
+      (with-atomic-rewriter
+       (cadr l)
+       (let ([rw (car l)])
+         (if (string? rw)
+             (lambda () (text rw (default-style) (default-font-size)))
+             rw))
+       (with-atomic-rewriter* thunk (cddr l)))))
+(define (with-compound-rewriter* thunk l)
+  (if (null? l)
+      (thunk)
+      (with-compound-rewriter
+       (cadr l) (car l)
+       (with-compound-rewriter* thunk (cddr l)))))
+(define (with-unquote-rewriter* thunk l)
+  (with-unquote-rewriter
+   (lambda (lw)
+     (let loop ([l l])
+       (cond [(null? l)
+              lw]
+             [else
+              (let ([pred (cadr l)]
+                    [tx (car l)])
+                (cond [(pred lw) (tx lw)]
+                      [else (loop (cddr l))]))])))
+   (thunk)))
+
+;; ============================================================
+
+(define (only-first-rw)
+  (compound-rw 'only-first-rw
+    (lambda (lws)
+      (let ([arg-lw (list-ref lws 2)])
+        (list arg-lw)))))
+
+(define (binary-rw op
+                   #:parenthesize-arg [parenthesize-arg #f]
+                   #:parenthesize-left [parenthesize-left parenthesize-arg]
+                   #:parenthesize-right [parenthesize-right parenthesize-arg])
+  (compound-rw 'binary-rw
+    (lambda (lws)
+      (let ([left (list-ref lws 2)]
+            [right (list-ref lws 3)])
+        ;; (list left (just-after op left) (between "" left right) right)
+        ;; (list left (just-after op left) "" right)
+        (append (maybe-parenthesize left parenthesize-left)
+                (list (between (->string/pict op) left right))
+                (maybe-parenthesize right parenthesize-right))))
+    2 2))
+
+(define (prefix-rw pre
+                   #:parenthesize-arg [parenthesize-arg #f])
+  (compound-rw 'prefix-rw
+    (lambda (lws)
+      (let ([arg-lw (list-ref lws 2)])
+        (append (list (just-before (->string/pict pre) arg-lw))
+                (maybe-parenthesize arg-lw parenthesize-arg))))
+    1 1))
+
+(define (postfix-rw post
+                    #:parenthesize-arg [parenthesize-arg #f])
+  (compound-rw 'postfix-rw
+    (lambda (lws)
+      (let ([arg-lw (list-ref lws 2)])
+        (append (maybe-parenthesize arg-lw parenthesize-arg)
+                (list (just-after (->string/pict post) arg-lw)))))
+    1 1))
+
+(define (function-rw name)
+  (compound-rw 'function-rw
+    (lambda (lws)
+      (list* (re-lw (->string/pict name) (list-ref lws 1))
+             (between "(" (list-ref lws 1) (list-ref lws 2))
+             (comma-ize (cddr lws) #t)))))
+
+(define (bracket-rw brackets #:tall? [tall? #f] #:comma? [comma? #t])
+  (let-values ([(left-bracket right-bracket)
+                (cond [(symbol? brackets)
+                       (case brackets
+                         ((round) (values "(" ")"))
+                         ((square) (values "[" "]"))
+                         ((curly) (values "{" "}"))
+                         ((angle) (values "〈" "〉"))
+                         ;; FIXME: more
+                         (else (error 'bracket-rw "unknown bracket kind: ~e" brackets)))]
+                      [(list? brackets)
+                       (values (first brackets) (second brackets))])])
+    (compound-rw 'bracket-rw
+      (lambda (lws)
+        (let ([lwA (first lws)]
+              [lwZ (last lws)]
+              [elems (drop-right (drop lws 2) 1)])
+          (append (list (re-lw (if tall? (taller left-bracket) left-bracket) lwA)
+                        "")
+                  (if comma? (comma-ize elems #f) elems)
+                  (list (re-lw (if tall? (taller right-bracket) right-bracket) lwZ))))))))
+
+(define (splice-rw)
+  (compound-rw 'splice-rw
+    (lambda (lws)
+      (drop-right (drop lws 2) 1))))
+
+(define (constant-rw s)
+  (compound-rw 'constant-rw
+    (lambda (lws)
+      (list (re-lw s (first lws))))))
+
+(define (set-cons-rw)
+  (compound-rw 'set-cons-rw
+    (lambda (lws)
+      (list (just-before "{" (list-ref lws 2))
+            (list-ref lws 2)
+            (just-after "}∪" (list-ref lws 2))
+            (between "" (list-ref lws 2) (list-ref lws 3))
+            (list-ref lws 3)))))                                  
+
+;; ============================================================
+
+;; Content = (U string symbol pict (listof (U 'spring lw)))
+
+;; between : Content lw lw -> lw
+;; Makes an lw with given content and location between given lws.
+(define (between s a b)
+  (build-lw s
+            (lw-line a)
+            0
+            (+ (lw-column a) (lw-column-span a))
+            (max 0 (- (lw-column b)
+                      (+ (lw-column a) (lw-column-span a))))))
+
+;; re-lw : Content lw -> lw
+;; Makes an lw with locations of old lw and new content.
+(define (re-lw new-e lw)
+  (build-lw new-e
+            (lw-line lw) (lw-line-span lw)
+            (lw-column lw) (lw-column-span lw)))
+
+;; refit : (listof lw) (listof lw) -> (listof lw)
+;; Add empty lws ("") around new based on locations of old lws (??)
+;; Soaks up logical space ????
+(define (refit orig new)
+  (append (list (between "" (just-before "" (car orig)) (car new)))
+          new
+          (list (between "" (just-after "" (last new)) (just-after "" (last orig))))))
+
+(define (compound-rw who proc [min-args 0] [max-args +inf.0]
+                     #:refit? [refit? #t])
+  ((if refit? refit-rw values)
+   (lambda (lws)
+     (unless (>= (length lws) 3)
+       (error who "expected list of at least 3 lws, got: ~e" lws))
+     (let ([lwA (first lws)]
+           [lwB (second lws)]
+           [lwZ (last lws)])
+       (unless (member (lw-e lwA) '("(" "[" "{"))
+         (error who "expected first lw to contain open-paren, got: ~e" lwA))
+       (unless (symbol? (lw-e lwB))
+         (error who "expected second lw to contain symbol, got: ~e" lwB))
+       (unless (member (lw-e lwZ) '(")" "]" "}"))
+         (error who "expected last lw to contain close-paren, got: ~e" lwZ))
+       (let ([args (- (length lws) 3)])
+         (unless (<= min-args args max-args)
+           (if (= min-args max-args)
+               (error who "expected ~s argument(s), got ~s: ~e"
+                      min-args args lws)
+               (error who "expected between ~s and ~s arguments, got ~s: ~e"
+                      min-args max-args args lws))))
+       (proc lws)))))
+
+(define ((refit-rw proc) lws)
+  (refit lws (proc lws)))
+
+(define (taller s)
+  (define p
+    (cond [(string? s) (text s (default-style) (default-font-size))]
+          [(pict? s) s]))
+  (define h (pict-height p))
+  (drop-below-ascent (scale (launder p) 1 1.3) (* 0.1 h)))
+
+(define (comma-ize lws contains-close-paren?)
+  (let loop ([lws lws])
+    (cond [(and contains-close-paren?
+                (or (null? (cdr lws))
+                    (null? (cddr lws))))
+           lws]
+          [(and (not contains-close-paren?)
+                (or (null? lws)
+                    (null? (cdr lws))))
+           lws]
+          [(positive? (lw-line-span (car lws)))
+           ;; a line break?
+           (cons (car lws) (loop (cdr lws)))]
+          [else (list*
+                 (car lws)
+                 (between ", " (car lws) (cadr lws))
+                 (loop (cdr lws)))])))
+
+;; ->string/pict : (U string pict (-> (U string pict)) -> (U string pict)
+(define (->string/pict c)
+  (cond [(pict? c) c]
+        [(string? c) c] ;; ((current-text) c (default-style) (default-font-size))
+        [else (c)]))
+
+;; maybe-parenthesize : lw _ -> (nonempty-listof lw)
+(define (maybe-parenthesize arg paren-spec)
+  (if (parenthesize? arg paren-spec)
+      (parenthesize-lws (list arg))
+      (list arg)))
+
+;; parenthesize? : lw (U #t #f (listof symbol) (-> lw boolean)) -> boolean
+(define (parenthesize? arg parenthesize-arg)
+  (cond [(boolean? parenthesize-arg) parenthesize-arg]
+        [(list? parenthesize-arg)
+         (let ([contents (lw-e arg)])
+           (and (not (lw-unq? arg))
+                (not (lw-metafunction? arg))
+                (list? contents)
+                (>= (length contents) 3)
+                (member (lw-e (first contents)) '("(" "[" "{"))
+                (member (lw-e (last contents)) '(")" "]" "}"))
+                (member (lw-e (second contents)) parenthesize-arg)
+                #t))]
+        [(procedure? parenthesize-arg)
+         (parenthesize-arg arg)]))
+
+;; parenthesize-lws : (nonempty-listof lw) -> (nonempty-listof lw)
+(define (parenthesize-lws lws)
+  (let ([lwA (first lws)]
+        [lwZ (last lws)])
+    (append (list (just-before "(" lwA))
+            lws
+            (list (just-after ")" lwZ)))))
diff --git a/collects/unstable/scribblings/redex.scrbl b/collects/unstable/scribblings/redex.scrbl
new file mode 100644
index 0000000000..a314fe552c
--- /dev/null
+++ b/collects/unstable/scribblings/redex.scrbl
@@ -0,0 +1,343 @@
+#lang scribble/manual
+@(require racket/stxparam scribble/base scribble/eval "utils.rkt"
+          (for-syntax racket/base syntax/srcloc)
+          (for-label racket/base racket/contract slideshow/pict redex unstable/redex))
+
+@(define the-eval (make-base-eval))
+@(the-eval '(require redex/reduction-semantics redex/pict unstable/redex slideshow/pict))
+
+@title[#:tag "redex"]{Redex}
+@unstable-header[]
+
+@defmodule[unstable/redex]
+
+This library provides functions to help typesetting for
+@racketmodname[redex] models. The following example program provides
+an overview of the features:
+
+@with-eval-preserve-source-locations[
+@interaction[#:eval the-eval
+(define-language ZF
+  [e empty
+     (Set e)
+     (Union e_1 e_2)
+     (Powerset e)
+     ZZ
+     variable-not-otherwise-mentioned]
+  [formula (same? e_1 e_2)
+           (in? e_1 e_2)
+           true
+           false
+           (implies formula_1 formula_2)])
+]]
+
+By default, Redex models are typeset as S-expressions with some basic
+styling that distinguishes literals from nonterminal names, handles
+subscripting, etc.
+
+@with-eval-preserve-source-locations[
+@interaction[#:eval the-eval
+(language->pict ZF)
+(term->pict ZF (in? x (Set 1 2 3 ...)))
+]]
+
+This library provides helper functions for creating and using
+rewriters that transform the S-expression model terms into other
+notations.
+
+@with-eval-preserve-source-locations[
+@interaction[#:eval the-eval
+(add-atomic-rewriters!
+ 'empty "∅"
+ 'formula "φ"
+ 'ZZ "\u2124"
+ 'variable-not-otherwise-mentioned
+     (lambda () (text "x, y, z, ..." (literal-style) (default-font-size)))
+ 'true (lambda () (text "true" '(caps . modern) (default-font-size)))
+ 'false (lambda () (text "false" '(caps . modern) (default-font-size))))
+(add-compound-rewriters!
+ 'same? (binary-rw " = ")
+ 'in? (binary-rw " ∈ ")
+ 'Set (bracket-rw 'curly)
+ 'Powerset (function-rw "𝒫 ")
+ 'Union (binary-rw "∪")
+ 'implies (binary-rw " ⇒ " #:parenthesize-left '(implies)))
+(with-rewriters
+  (lambda ()
+    (language->pict ZF)))
+(with-rewriters
+  (lambda ()
+    (render-term ZF (in? x (Set 1 2 3 ...)))))
+]]
+
+@; ----------------------------------------
+
+@defproc[(with-rewriters [proc (-> any)])
+         any]{
+
+Calls @racket[proc] with the rewriters of
+@racket[current-atomic-rewriters], @racket[current-compound-rewriters],
+and @racket[current-unquote-rewriters].
+}
+
+@defparam[current-atomic-rewriters rewriters
+          (let ([atomic-rewriter/c
+                 (or/c string? pict?
+                       (-> (or/c string? pict?)))])
+            (plistof symbol? atomic-rewriter/c))]{
+
+Parameter of atomic rewriters (as in @racket[with-atomic-rewriter])
+used by @racket[with-rewriters].
+}
+
+@defparam[current-compound-rewriters rewriters
+          (plistof symbol? compound-rewriter/c)]{
+
+Parameter of compound rewriters (as in
+@racket[with-compound-rewriter]) used by @racket[with-rewriters].
+}
+
+@defparam[current-unquote-rewriters rewriters
+          (plistof (-> lw? any/c) (-> lw? lw?))]{
+
+Parameter of unquote rewriters (as in @racket[with-unquote-rewriter])
+used by @racket[with-rewriters].
+}
+
+@deftogether[[
+@defproc[(add-atomic-rewriters! [rewriters
+                                 (let ([atomic-rewriter/c
+                                        (or/c string? pict?
+                                               (-> (or/c string? pict?)))])
+                                   (plistof symbol? atomic-rewriter/c))])
+         void?]
+@defproc[(add-compound-rewriters! [rewriters
+                                   (plistof symbol? compound-rewriter/c)])
+         void?]
+@defproc[(add-unquote-rewriters! [rewriters
+                                  (plistof (-> lw? any/c) (-> lw? lw?))])
+         void?]]]{
+
+Add rewriters to the @racket[current-atomic-rewriters],
+@racket[current-compound-rewriters], or
+@racket[current-unquote-rewriters], respectively.
+}
+
+@defproc[(plistof [key/c contract?] [value/c contract?])
+         contract?]{
+
+Contract for even-length lists of alternating @racket[key/c] and
+@racket[value/c] values.
+
+Equivalent to
+@racketblock[
+(letrec ([ctc
+          (recursive-contract
+           (or/c '()
+                 (cons/c key/c (cons/c value/c ctc))))])
+  ctc)
+]
+}
+
+@defthing[compound-rewriter/c contract?]{
+
+Contract for compound rewriters, which take a list of @racket[lw]
+structs and returns a list of @racket[lw]s, @racket[pict]s, or
+strings.
+
+Equivalent to 
+@racketblock[
+(-> (listof lw?)
+    (listof (or/c lw? pict? string?)))
+]
+}
+
+@defproc[(binary-rw [operator (or/c string? pict? (-> (or/c string? pict?)))]
+                    [#:parenthesize-arg parenthesize-arg
+                                        (or/c #t #f (listof symbol?) (-> lw? any/c))
+                                        #f]
+                    [#:parenthesize-left parenthesize-left
+                                         (or/c #t #f (listof symbol?) (-> lw? any/c))
+                                         parenthesize-arg]
+                    [#:parenthesize-right parenthesize-right
+                                          (or/c #t #f (listof symbol?) (-> lw? any/c))
+                                          parenthesize-arg])
+         compound-rewriter/c]{
+
+Typesets @racket[(_sym _term1 _term2)] using @racket[operator] as a
+binary operator between @racket[_term1] and @racket[_term2].
+
+@with-eval-preserve-source-locations[
+@examples[#:eval the-eval
+(add-compound-rewriters!
+ 'plus (binary-rw " + "))
+(with-rewriters
+  (lambda ()
+    (term->pict ZF (plus 1 2))))
+]]
+
+Redex terms may become ambiguous when typeset. To avoid ambiguity, use
+@racket[#:parenthesize-arg] to direct when arguments should be
+parenthesized. If @racket[parenthesize-arg] is @racket[#t], then
+arguments are always parenthesized; if it is @racket[#f], never; if it
+is a list of symbols, then an argument is parenthesized only if the
+argument is a term starting with a symbol in the list; if it is a
+procedure, then the argument is parenthesized if the procedure applied
+to the argument's @racket[lw] struct returns a true value.
+
+@with-eval-preserve-source-locations[
+@interaction[#:eval the-eval
+(add-compound-rewriters!
+ 'times (binary-rw " × "))
+(with-rewriters
+  (lambda ()
+    (term->pict ZF (times (plus 1 2) 3))))
+(add-compound-rewriters!
+ 'times (binary-rw " × " #:parenthesize-arg '(plus)))
+(with-rewriters
+  (lambda ()
+    (term->pict ZF (times (plus 1 2) 3))))
+]]
+
+The parenthesization rules for left and right arguments can be
+supplied separately through @racket[#:parenthesize-left] and
+@racket[#:parenthesize-right], for example to create left-associated
+or right-associated operators:
+
+@with-eval-preserve-source-locations[
+@interaction[#:eval the-eval
+(add-compound-rewriters!
+ 'arrow (binary-rw " → " #:parenthesize-left '(arrow)))
+(with-rewriters
+  (lambda ()
+    (term->pict ZF (arrow (arrow A B) (arrow C D)))))
+]]
+}
+
+@defproc[(prefix-rw [prefix (or/c string? pict? (-> (or/c string? pict?)))]
+                    [#:parenthesize-arg parenthesize-arg
+                                        (or/c #f #t (listof symbol?) (-> lw? any/c))
+                                        #f])
+         compound-rewriter/c]{
+
+Typesets @racket[(_sym _term)] by placing @racket[prefix] before
+@racket[_term].
+
+@with-eval-preserve-source-locations[
+@examples[#:eval the-eval
+(add-compound-rewriters!
+ 'not (prefix-rw "¬ "))
+(with-rewriters
+  (lambda ()
+    (term->pict ZF (not (in? x empty)))))
+]]
+}
+
+@defproc[(postfix-rw [postfix (or/c string? pict? (-> (or/c string? pict?)))]
+                     [#:parenthesize-arg parenthesize-arg
+                                         (or/c #f #t (listof symbol?) (-> lw? any/c))
+                                         #f])
+         compound-rewriter/c]{
+
+Typesets @racket[(_sym _term)] by placing @racket[postfix] after
+@racket[_term].
+
+@with-eval-preserve-source-locations[
+@examples[#:eval the-eval
+(add-compound-rewriters!
+ 'nonempty (postfix-rw " is nonempty"))
+(with-rewriters
+  (lambda ()
+    (term->pict ZF (nonempty (Set x)))))
+]]
+}
+
+@defproc[(function-rw [function (or/c string? pict? (-> (or/c string? pict?)))])
+         compound-rewriter/c]{
+
+Typesets @racket[(_sym _term ...)] by placing @racket[function] before
+the parenthesized, comma-separated list of @racket[_term]s.
+
+@with-eval-preserve-source-locations[
+@examples[#:eval the-eval
+(add-compound-rewriters!
+ 'f (function-rw "f")
+ 'max (function-rw (text "max" '(bold . modern) (default-font-size))))
+(with-rewriters
+  (lambda ()
+    (term->pict ZF (max 1 2 (f 3)))))
+]]
+}
+
+@defproc[(only-first-rw)
+         compound-rewriter/c]{
+
+Typesets @racket[(_sym _term1 _term2 ...)] as @racket[_term1]. Useful
+for hiding parameters that are necessary for defining the semantics
+but can be glossed over in its explanation, such as state parameters
+used for generating unique names.
+
+@with-eval-preserve-source-locations[
+@examples[#:eval the-eval
+(add-compound-rewriters!
+ 'First (only-first-rw))
+(with-rewriters
+  (lambda ()
+    (term->pict ZF [First (in? x y) counter])))
+]]
+}
+
+@defproc[(splice-rw)
+         compound-rewriter/c]{
+
+Typesets @racket[(_sym _term ...)] by rendering the @racket[_term]s
+side-by-side.
+}
+
+@defproc[(constant-rw [constant (or/c string? pict? (-> (or/c string? pict?)))])
+         compound-rewriter/c]{
+
+Typesets @racket[(_sym _term ...)] as @racket[constant].
+}
+
+@defproc[(bracket-rw [brackets (or/c 'round 'square 'curly 'angle
+                                     (list (or/c string? pict?)
+                                           (or/c string? pict?)))]
+                     [#:comma? comma? any/c #t])
+         compound-rewriter/c]{
+
+Typesets @racket[(_sym _term ...)] by surrounding the comma-separated
+(or space-separated, if @racket[comma?] is false) sequence of
+@racket[_term]s with brackets. If @racket[brackets] is a list, the
+first element is the left bracket and the second is the right bracket;
+@racket['round] is equivalent to @racket['("(" ")")]; @racket['square]
+is equivalent to @racket['("[" "]")]; @racket['curly] is equivalent to
+@racket['("{" "}")]; and @racket['angle] is equivalent to
+@racket['("〈" "〉")].
+
+@with-eval-preserve-source-locations[
+@examples[#:eval the-eval
+(add-compound-rewriters!
+ 'Tuple (bracket-rw 'angle))
+(with-rewriters
+  (lambda ()
+    (term->pict ZF (Tuple 1 2 3))))
+]]
+}
+
+@defproc[(set-cons-rw)
+         compound-rewriter/c]{
+
+Rewriter that typesets @racket[(_sym _elem-term _set-term)] as the
+union of the singleton set containing @racket[_elem-term] with the set
+@racket[_set-term].
+
+@with-eval-preserve-source-locations[
+@examples[#:eval the-eval
+(add-compound-rewriters!
+ 'set-cons (set-cons-rw))
+(with-rewriters
+  (lambda ()
+    (term->pict ZF (set-cons x S))))
+]]
+}
diff --git a/collects/unstable/scribblings/unstable.scrbl b/collects/unstable/scribblings/unstable.scrbl
index 2c44a38210..6be8dcf4ea 100644
--- a/collects/unstable/scribblings/unstable.scrbl
+++ b/collects/unstable/scribblings/unstable.scrbl
@@ -99,6 +99,7 @@ Keep documentation and tests up to date.
 @include-section["parameter-group.scrbl"]
 @include-section["pretty.scrbl"]
 @include-section["recontract.scrbl"]
+@include-section["redex.scrbl"]
 @include-section["sandbox.scrbl"]
 @include-section["sequence.scrbl"]
 @include-section["string.scrbl"]