diff --git a/collects/redex/pict.rkt b/collects/redex/pict.rkt
index e7055f2ea1..cf20a48648 100644
--- a/collects/redex/pict.rkt
+++ b/collects/redex/pict.rkt
@@ -83,6 +83,8 @@
  [arrow-space (parameter/c natural-number/c)]
  [label-space (parameter/c natural-number/c)]
  [metafunction-cases (parameter/c (or/c #f (and/c pair? (listof (and/c integer? (or/c zero? positive?))))))]
+ [judgment-form-cases (parameter/c (or/c #f (and/c (listof (or/c exact-nonnegative-integer? string?))
+                                                   pair?)))]
  [metafunction-pict-style 
   (parameter/c (symbols 'left-right
                         'left-right/vertical-side-conditions
diff --git a/collects/redex/private/judgment-form.rkt b/collects/redex/private/judgment-form.rkt
index d149226205..4198bb0320 100644
--- a/collects/redex/private/judgment-form.rkt
+++ b/collects/redex/private/judgment-form.rkt
@@ -337,12 +337,12 @@
 
 (define-for-syntax (do-extended-judgment-form lang syn-err-name body orig stx)
   (define nts (definition-nts lang stx syn-err-name))
-  (define-values (judgment-form-name dup-form-names mode position-contracts clauses)
+  (define-values (judgment-form-name dup-form-names mode position-contracts clauses rule-names)
     (parse-judgment-form-body body syn-err-name stx (identifier? orig)))
   (define definitions
     #`(begin
         (define-syntax #,judgment-form-name 
-          (judgment-form '#,judgment-form-name '#,(cdr (syntax->datum mode)) #'judgment-form-runtime-proc #'mk-judgment-form-proc #'#,lang #'judgment-form-lws))
+          (judgment-form '#,judgment-form-name '#,(cdr (syntax->datum mode)) #'judgment-form-runtime-proc #'mk-judgment-form-proc #'#,lang #'judgment-form-lws '#,rule-names))
         (define mk-judgment-form-proc
           (compile-judgment-form-proc #,judgment-form-name #,mode #,lang #,clauses #,position-contracts #,orig #,stx #,syn-err-name))
         (define judgment-form-runtime-proc (mk-judgment-form-proc #,lang))
@@ -375,13 +375,29 @@
     (regexp-match? #rx"^-+$" (symbol->string (syntax-e id))))
   (define-syntax-class horizontal-line
     (pattern x:id #:when (horizontal-line? #'x)))
+  (define-syntax-class name
+    (pattern x #:when (string? (syntax-e #'x))))
   (define (parse-rules rules)
-    (for/list ([rule rules])
-      (syntax-parse rule
-        [(prem ... _:horizontal-line conc)
-         #'(conc prem ...)]
-        [_ rule])))
-  (define-values (name/mode mode-stx name/contract contract rules)
+    (define-values (backward-rules backward-names)
+      (for/fold ([parsed-rules '()]
+                 [names '()])
+        ([rule rules])
+        (syntax-parse rule
+          [(prem ... _:horizontal-line n:name conc)
+           (values (cons #'(conc prem ...) parsed-rules)
+                   (cons #'n names))]
+          [(prem ... _:horizontal-line conc)
+           (values (cons #'(conc prem ...) parsed-rules)
+                   (cons #f names))]
+          [(conc prem ... n:name)
+           (values (cons #'(conc prem ...) parsed-rules)
+                   (cons #'n names))]
+          [else
+           (values (cons rule parsed-rules)
+                   (cons #f names))])))
+    (values (reverse backward-rules)
+            (reverse backward-names)))
+  (define-values (name/mode mode-stx name/contract contract rules rule-names)
     (syntax-parse body #:context full-stx
       [((~or (~seq #:mode ~! mode:mode-spec)
              (~seq #:contract ~! contract:contract-spec))
@@ -405,9 +421,10 @@
                         (raise-syntax-error 
                          syn-err-name "expected at most one contract specification"
                          #f #f (syntax->list #'dups))])])
-         (values name/mode mode name/ctc ctc
-                 (parse-rules (syntax->list #'(rule ...)))))]))
+         (define-values (parsed-rules rule-names) (parse-rules (syntax->list #'(rule ...)))) 
+         (values name/mode mode name/ctc ctc parsed-rules rule-names))]))
   (check-clauses full-stx syn-err-name rules #t)
+  (check-dup-rule-names full-stx syn-err-name rule-names)
   (check-arity-consistency mode-stx contract full-stx)
   (define-values (form-name dup-names)
     (syntax-case rules ()
@@ -415,8 +432,21 @@
        (not extension?)
        (raise-syntax-error #f "expected at least one rule" full-stx)]
       [_ (defined-name (list name/mode name/contract) rules full-stx)]))
-  (values form-name dup-names mode-stx contract rules))
+  (values form-name dup-names mode-stx contract rules rule-names))
 
+;; names : (listof (or/c #f syntax[string]))
+(define-for-syntax (check-dup-rule-names full-stx syn-err-name names)
+  (define tab (make-hash))
+  (for ([name (in-list names)])
+    (when (syntax? name)
+      (define k (syntax-e name))
+      (hash-set! tab k (cons name (hash-ref tab k '())))))
+  (for ([(k names) (in-hash tab)])
+    (unless (= 1 (length names))
+      (raise-syntax-error syn-err-name
+                          "duplicate rule names"
+                          (car names) #f (cdr names)))))
+                          
 (define-for-syntax (check-arity-consistency mode-stx contracts full-def)
   (when (and contracts (not (= (length (cdr (syntax->datum mode-stx)))
                                (length contracts))))
diff --git a/collects/redex/private/pict.rkt b/collects/redex/private/pict.rkt
index 16840c4b6e..88ab08ffe8 100644
--- a/collects/redex/private/pict.rkt
+++ b/collects/redex/private/pict.rkt
@@ -62,6 +62,7 @@
          label-space
          metafunction-pict-style
          metafunction-cases
+         judgment-form-cases
          compact-vertical-min-width
          extend-language-show-union
          set-arrow-pict!
@@ -360,23 +361,27 @@
                        max-w))
 
 (define (rp->pict-label rp)
-  (define (bracket label)
-    (hbl-append
-     ((current-text) " [" (label-style) (label-font-size))
-     label
-     ((current-text) "]" (label-style) (label-font-size))))
   (cond [(rule-pict-computed-label rp) => bracket]
         [(rule-pict-label rp)
-         (let ([m (regexp-match #rx"^([^_]*)(?:_([^_]*)|)$" 
-                                (format "~a" (rule-pict-label rp)))])
-           (bracket
-            (hbl-append
-             ((current-text) (cadr m) (label-style) (label-font-size))
-             (if (caddr m)
-                 ((current-text) (caddr m) `(subscript . ,(label-style)) (label-font-size))
-                 (blank)))))]
+         (string->bracketed-label 
+          (format "~a" (rule-pict-label rp)))]
         [else (blank)]))
 
+(define (string->bracketed-label str)
+  (define m (regexp-match #rx"^([^_]*)(?:_([^_]*)|)$" str))
+  (bracket
+   (hbl-append
+    ((current-text) (cadr m) (label-style) (label-font-size))
+    (if (caddr m)
+        ((current-text) (caddr m) `(subscript . ,(label-style)) (label-font-size))
+        (blank)))))
+
+(define (bracket label)
+  (hbl-append
+   ((current-text) " [" (label-style) (label-font-size))
+   label
+   ((current-text) "]" (label-style) (label-font-size))))
+
 (define (add-between i l)
   (cond
     [(null? l) l]
@@ -774,7 +779,7 @@
 
 (define metafunction-pict-style (make-parameter 'left-right))
 (define metafunction-cases (make-parameter #f))
-(define (select-cases eqns)
+(define (select-mf-cases eqns)
   (let ([cases (metafunction-cases)])
     (if cases
         (let loop ([eqns eqns]
@@ -792,6 +797,31 @@
                 (loop (cdr eqns) cases (+ i 1))])]))
         eqns)))
 
+(define judgment-form-cases (make-parameter #f))
+(define (select-jf-cases eqns conclusions eqn-names)
+  (define cases
+    (or (judgment-form-cases)
+        (metafunction-cases)))
+  (cond
+    [cases
+     (define-values (rev-eqns rev-concs rev-eqn-names)
+       (for/fold ([eqns '()]
+                  [concs '()]
+                  [eqn-names '()])
+                 ([eqn (in-list eqns)]
+                  [conc (in-list conclusions)]
+                  [eqn-name (in-list eqn-names)]
+                  [i (in-naturals)])
+         (if (or (member i cases)
+                 (member eqn-name cases))
+             (values (cons eqn eqns)
+                     (cons conc concs)
+                     (cons eqn-name eqn-names))
+             (values eqns concs eqn-names))))
+      (values (reverse rev-eqns) (reverse rev-concs) (reverse rev-eqn-names))]
+    [else 
+     (values eqns conclusions eqn-names)]))
+
 ;; remove-dups : (listof number)[sorted] -> (listof number)[sorted]
 ;; removes duplicate numbers from 'l'
 (define (remove-dups l)
@@ -826,8 +856,8 @@
                                                    (list-ref eqn 0))))
                              (metafunc-proc-pict-info (metafunction-proc mf))))
                       mfs))]
-         [eqns (select-cases all-eqns)]
-         [lhss (select-cases all-lhss)]
+         [eqns (select-mf-cases all-eqns #f)]
+         [lhss (select-mf-cases all-lhss #f)]
          [rhss (map (lambda (eqn) (wrapper->pict (list-ref eqn 2))) eqns)]
          [_ (unless (or (not current-linebreaks)
                         (= (length current-linebreaks) (length eqns)))
@@ -1034,6 +1064,7 @@
     (error form "expected relation as argument, got a metafunction"))
   (inference-rules-pict (metafunc-proc-name (metafunction-proc mf))
                         (metafunc-proc-pict-info (metafunction-proc mf))
+                        (map (λ (x) #f) (metafunc-proc-pict-info (metafunction-proc mf)))
                         (metafunc-proc-lang (metafunction-proc mf))))
 
 (define (render-pict make-pict filename)
@@ -1044,17 +1075,17 @@
      (parameterize ([dc-for-text-size (make-object bitmap-dc% (make-object bitmap% 1 1))])
        (make-pict))]))
 
-(define (inference-rules-pict name all-eqns lang)
-  (let* ([all-nts (language-nts lang)]
-         [wrapper->pict (lambda (lw) (lw->pict all-nts lw))]
-         [all-conclusions 
-          (map (lambda (eqn) 
-                 (wrapper->pict
-                  (metafunction-call name (list-ref eqn 0))))
-               all-eqns)]
-         [eqns (select-cases all-eqns)]
-         [conclusions (select-cases all-conclusions)]
-         [premisess (map (lambda (eqn)
+(define (inference-rules-pict name all-eqns eqn-names lang)
+  (define all-nts (language-nts lang))
+  (define (wrapper->pict lw) (lw->pict all-nts lw))
+  (define all-conclusions 
+    (map (lambda (eqn) 
+           (wrapper->pict
+            (metafunction-call name (list-ref eqn 0))))
+         all-eqns))
+  (define-values (selected-eqns conclusions selected-eqn-names)
+    (select-jf-cases all-eqns all-conclusions eqn-names))
+  (define premisess (map (lambda (eqn)
                            (append (map wrapper->pict (list-ref eqn 2))
                                    (map (match-lambda
                                           [(struct metafunc-extra-where (lhs rhs))
@@ -1063,18 +1094,29 @@
                                            (wrapper->pict expr)]
                                           [wrapper (wrapper->pict wrapper)])
                                         (list-ref eqn 1))))
-                         eqns)])
-    ((relation-clauses-combine)
-     (for/list ([conclusion (in-list conclusions)]
-                [premises (in-list premisess)])
-       (define top (apply hbl-append 20 premises))
-       (define line-w (max (pict-width top) (pict-width conclusion)))
+                         selected-eqns))
+  ((relation-clauses-combine)
+   (for/list ([conclusion (in-list conclusions)]
+              [premises (in-list premisess)]
+              [name (in-list selected-eqn-names)])
+     (define top (apply hbl-append 20 premises))
+     (define line-w (max (pict-width top) (pict-width conclusion)))
+     (define line (dc (λ (dc dx dy) (send dc draw-line dx dy (+ dx line-w) dy))
+                      line-w 1)) 
+     (define w/out-label
        (vc-append
         (horizontal-bar-spacing)
         top
-        (dc (λ (dc dx dy) (send dc draw-line dx dy (+ dx line-w) dy))
-            line-w 1)
-        conclusion)))))
+        line
+        conclusion))
+     (if name
+         (let ([label (string->bracketed-label name)])
+           (let-values ([(x y) (rc-find w/out-label line)])
+             (hb-append w/out-label 
+                        (vl-append label
+                                   (blank 0 (- (- (pict-height w/out-label) y)
+                                               (/ (pict-height label) 2)))))))
+         w/out-label))))
 
 (define horizontal-bar-spacing (make-parameter 4))
 (define relation-clauses-combine (make-parameter (λ (l) (apply vc-append 20 l))))
@@ -1084,6 +1126,7 @@
   (syntax-property
    #`(inference-rules-pict '#,(judgment-form-name jf)
                            #,(judgment-form-lws jf)
+                           '#,(judgment-form-rule-names jf)
                            #,(judgment-form-lang jf))
    'disappeared-use
    form-name))
diff --git a/collects/redex/private/term-fn.rkt b/collects/redex/private/term-fn.rkt
index 37d03a400b..07bb3cd979 100644
--- a/collects/redex/private/term-fn.rkt
+++ b/collects/redex/private/term-fn.rkt
@@ -27,7 +27,7 @@
        (cond [(syntax-local-value stx (λ () #f)) => p?]
              [else #f])))
 
-(define-struct judgment-form (name mode proc mk-proc lang lws))
+(define-struct judgment-form (name mode proc mk-proc lang lws rule-names))
 
 (define-struct defined-term (value))
 (define (defined-term-id? stx)
diff --git a/collects/redex/scribblings/ref.scrbl b/collects/redex/scribblings/ref.scrbl
index 59784d265f..ebd4954a90 100644
--- a/collects/redex/scribblings/ref.scrbl
+++ b/collects/redex/scribblings/ref.scrbl
@@ -1147,18 +1147,21 @@ and @racket[#f] otherwise.
               [pos-use I
                        O]
               [rule [premise
-                     ...
-                     dashes
+                     ... 
+                     dashes rule-name
                      conclusion]
                     [conclusion 
                      premise 
-                     ...]]
+                     ...
+                     rule-name]]
               [conclusion (form-id pat/term ...)]
               [premise (code:line (judgment-form-id pat/term ...) maybe-ellipsis)
                        (where @#,ttpattern @#,tttterm)
                        (where/hidden @#,ttpattern @#,tttterm)
                        (side-condition @#,tttterm)
                        (side-condition/hidden @#,tttterm)]
+              [rule-name (code:line)
+                         string]
               [pat/term @#,ttpattern
                         @#,tttterm]
               [maybe-ellipsis (code:line)
@@ -1187,11 +1190,11 @@ For example, the following defines addition on natural numbers:
        (define-judgment-form nats
          #:mode (sum I I O)
          #:contract (sum n n n)
-         [-----------
+         [-----------  "zero"
           (sum z n n)]
          
          [(sum n_1 n_2 n_3)
-          -------------------------
+          ------------------------- "add1"
           (sum (s n_1) n_2 (s n_3))])]
 
 The @racket[judgment-holds] form checks whether a relation holds for any 
@@ -1267,11 +1270,11 @@ one.
          #:mode (even I)
          #:contract (even n)
          
-         [--------
+         [-------- "evenz"
           (even z)]
          
          [(even n)
-          ----------------
+          ---------------- "even2"
           (even (s (s n)))])
        
        (define-judgment-form nats
@@ -2546,8 +2549,24 @@ precede ellipses that represent argument sequences; when it is
                                          (or/c zero? positive?)))
                           pair?))]{
 
-This parameter controls which cases in a metafunction are rendered. If it is @racket[#f] (the default), then all of the
+Controls which cases in a metafunction are rendered. If it is @racket[#f] (the default), then all of the
 cases appear. If it is a list of numbers, then only the selected cases appear (counting from @racket[0]).
+
+This parameter also controls how which clauses in judgment forms are rendered, but
+only in the case that @racket[judgment-form-cases] is @racket[#f].
+}
+                                  
+@defparam[judgment-form-cases 
+          cases
+          (or/c #f
+                (and/c (listof (or/c exact-nonnegative-integer?
+                                     string?))
+                       pair?))]{
+   Controls which clauses in a judgment form are rendered. If it is 
+   @racket[#f] (the default), then all of them are rendered. If
+   it is a list, then only the selected clauses appear (numbers
+   count from @racket[0], and strings correspond to the labels
+   in a judgment form).
 }
 
 @deftogether[[
diff --git a/doc/release-notes/redex/HISTORY.txt b/doc/release-notes/redex/HISTORY.txt
index 28009462e7..69fc6b919c 100644
--- a/doc/release-notes/redex/HISTORY.txt
+++ b/doc/release-notes/redex/HISTORY.txt
@@ -2,6 +2,10 @@ v5.3.1
 
   * added optional #:lang keyword to term
 
+  * added the ability to name clauses to define-judgment-form
+
+  * added judgment-form-cases
+
 v5.3
 
   * added the amb tutorial.