diff --git a/collects/redex/private/judgment-form.rkt b/collects/redex/private/judgment-form.rkt
index 75bca90ac7..400a430d48 100644
--- a/collects/redex/private/judgment-form.rkt
+++ b/collects/redex/private/judgment-form.rkt
@@ -4,12 +4,14 @@
          "term.rkt"
          "fresh.rkt"
          "error.rkt"
-         racket/trace)
+         racket/trace
+         racket/stxparam)
 
 (require
  (for-syntax "rewrite-side-conditions.rkt"
              "term-fn.rkt"
              "loc-wrapper-ct.rkt"
+             racket/stxparam-exptime
              racket/base
              racket/syntax
              syntax/id-table
@@ -21,6 +23,20 @@
 (define-struct metafunc-extra-where (lhs rhs))
 (define-struct metafunc-extra-fresh (vars))
 
+(define-for-syntax (judgment-form-id? stx) 
+  (and (identifier? stx)
+       (judgment-form? (syntax-local-value stx (λ () #f)))))
+
+(begin-for-syntax
+  ;; pre: (judgment-form-id? stx) holds
+  (define (lookup-judgment-form-id stx)
+    (define jf-pe (judgment-form-pending-expansion))
+    (if (and jf-pe
+             (free-identifier=? (car jf-pe) stx))
+        (cdr jf-pe)
+        (syntax-local-value stx)))
+  (define judgment-form-pending-expansion (make-parameter #f)))
+
 (define-for-syntax (prune-syntax stx)
   (datum->syntax
    (identifier-prune-lexical-context #'whatever '(#%app #%datum))
@@ -149,7 +165,7 @@
                           (ellipsis? #'maybe-ellipsis)
                           (values #'more #t)]
                          [_ (values #'after #f)])]
-                      [(judgment-form) (syntax-local-value/record #'form-name (λ (_) #t))]
+                      [(judgment-form) (lookup-judgment-form-id #'form-name)]
                       [(mode) (judgment-form-mode judgment-form)]
                       [(judgment-proc) (judgment-form-proc judgment-form)]
                       [(input-template output-pre-pattern) 
@@ -175,6 +191,7 @@
                          (if under-ellipsis?
                              #`(repeated-premise-outputs #,input (λ (x) #,(make-traced #'x)))
                              (make-traced input)))])
+          (record-disappeared-uses (list #'form-name))
           (with-syntax ([(output-name ...) output-names]
                         [(output-name/ellipsis ...) output-names/ellipses]
                         [(temp ...) temporaries]
@@ -231,12 +248,12 @@
                   [(I) (cons (car is) (loop (cdr ms) (cdr is) os))]
                   [(O) (cons (car os) (loop (cdr ms) is (cdr os)))]))))
         (define (wrapped . _)
-          (set! outputs (form-proc input))
+          (set! outputs (form-proc form-proc input))
           (for/list ([output outputs])
             (cons form-name (assemble input output))))
         (apply trace-call form-name wrapped (assemble input spacers))
         outputs)
-      (form-proc input)))
+      (form-proc form-proc input)))
 
 (define (verify-name-ok orig-name the-name)
   (unless (symbol? the-name)
@@ -266,7 +283,7 @@
   (syntax-case judgment ()
     [(form-name pat ...)
      (judgment-form-id? #'form-name)
-     (let ([expected (length (judgment-form-mode (syntax-local-value #'form-name)))]
+     (let ([expected (length (judgment-form-mode (lookup-judgment-form-id #'form-name)))]
            [actual (length (syntax->list #'(pat ...)))])
        (unless (= actual expected)
          (raise-syntax-error 
@@ -303,32 +320,46 @@
   (not-expression-context stx)
   (syntax-case stx ()
     [(def-form-id lang . body)
-     (let ([lang #'lang]
-           [syn-err-name (syntax-e #'def-form-id)])
-       (define nts (definition-nts lang stx syn-err-name))
-       (define-values (judgment-form-name dup-form-names mode position-contracts clauses)
-         (parse-judgment-form-body #'body syn-err-name stx))
-       (define definitions
-         #`(begin
-             (define-syntax #,judgment-form-name 
-               (judgment-form '#,judgment-form-name '#,mode #'judgment-form-proc #'#,lang #'judgment-form-lws))
-             (define judgment-form-proc
-               (compile-judgment-form-proc #,judgment-form-name #,lang #,mode #,clauses #,position-contracts #,stx #,syn-err-name))
-             (define judgment-form-lws
-               (compiled-judgment-form-lws #,clauses))))
-       (syntax-property
-        (prune-syntax
-         (if (eq? 'top-level (syntax-local-context))
-             ; Introduce the names before using them, to allow
-             ; judgment form definition at the top-level.
-             #`(begin 
-                 (define-syntaxes (judgment-form-proc judgment-form-lws) (values))
-                 #,definitions)
-             definitions))
-        'disappeared-use
-        (map syntax-local-introduce dup-form-names)))]))
+     (do-extended-judgment-form #'lang (syntax-e #'def-form-id) #'body #f stx)]))
 
-(define-for-syntax (parse-judgment-form-body body syn-err-name full-stx)
+(define-syntax (define-extended-judgment-form stx)
+  (not-expression-context stx)
+  (syntax-case stx ()
+    [(def-form-id lang original-id . body)
+     (begin
+       (unless (judgment-form-id? #'original-id)
+         (raise-syntax-error 'define-extended-judgment-form 
+                             "expected a judgment form"
+                             stx
+                             #'original-id))
+       (do-extended-judgment-form #'lang 'define-extended-judgment-form #'body #'original-id stx))]))
+
+(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)
+    (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-proc #'mk-judgment-form-proc #'#,lang #'judgment-form-lws))
+        (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-proc (mk-judgment-form-proc #,lang))
+        (define judgment-form-lws
+          (compiled-judgment-form-lws #,clauses))))
+  (syntax-property
+   (prune-syntax
+    (if (eq? 'top-level (syntax-local-context))
+        ; Introduce the names before using them, to allow
+        ; judgment form definition at the top-level.
+        #`(begin 
+            (define-syntaxes (judgment-form-proc judgment-form-lws) (values))
+            #,definitions)
+        definitions))
+   'disappeared-use
+   (map syntax-local-introduce dup-form-names)))
+
+(define-for-syntax (parse-judgment-form-body body syn-err-name full-stx extension?)
   (define-syntax-class pos-mode
     #:literals (I O)
     (pattern I)
@@ -349,7 +380,7 @@
         [(prem ... _:horizontal-line conc)
          #'(conc prem ...)]
         [_ rule])))
-  (define-values (name/mode mode name/contract contract rules)
+  (define-values (name/mode mode-stx name/contract contract rules)
     (syntax-parse body #:context full-stx
       [((~or (~seq #:mode ~! mode:mode-spec)
              (~seq #:contract ~! contract:contract-spec))
@@ -357,10 +388,14 @@
         rule:expr ...)
        (let-values ([(name/mode mode)
                      (syntax-parse #'(mode ...)
-                       [((name . mode)) (values #'name (syntax->list #'mode))]
-                       [_ (raise-syntax-error 
-                           #f "expected definition to include a mode specification"
-                           full-stx)])]
+                       [((name the-mode ...)) (values #'name (car (syntax->list #'(mode ...))))]
+                       [_ 
+                        (raise-syntax-error 
+                         #f
+                         (if (null? (syntax->list #'(mode ...)))
+                             "expected definition to include a mode specification"
+                             "expected definition to include only one mode specification")
+                         full-stx)])]
                     [(name/ctc ctc)
                      (syntax-parse #'(contract ...)
                        [() (values #f #f)]
@@ -372,15 +407,18 @@
          (values name/mode mode name/ctc ctc
                  (parse-rules (syntax->list #'(rule ...)))))]))
   (check-clauses full-stx syn-err-name rules #t)
-  (check-arity-consistency mode contract full-stx)
+  (check-arity-consistency mode-stx contract full-stx)
   (define-values (form-name dup-names)
     (syntax-case rules ()
-      [() (raise-syntax-error #f "expected at least one rule" full-stx)]
+      [() 
+       (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 contract rules))
+  (values form-name dup-names mode-stx contract rules))
 
-(define-for-syntax (check-arity-consistency mode contracts full-def)
-  (when (and contracts (not (= (length mode) (length contracts))))
+(define-for-syntax (check-arity-consistency mode-stx contracts full-def)
+  (when (and contracts (not (= (length (cdr (syntax->datum mode-stx)))
+                               (length contracts))))
     (raise-syntax-error 
      #f "mode and contract specify different numbers of positions" full-def)))
 
@@ -412,7 +450,7 @@
     [(j-h (form-name . pats) tmpl)
      (judgment-form-id? #'form-name)
      (let* ([syn-err-name (syntax-e #'j-h)]
-            [lang (judgment-form-lang (syntax-local-value #'form-name))]
+            [lang (judgment-form-lang (lookup-judgment-form-id #'form-name))]
             [nts (definition-nts lang stx syn-err-name)]
             [judgment (syntax-case stx () [(_ judgment _) #'judgment])])
        (check-judgment-arity stx judgment)
@@ -424,54 +462,93 @@
      (not (judgment-form-id? #'form-name))
      (raise-syntax-error #f "expected a judgment form name" stx #'not-form-name)]))
 
-(define-for-syntax (do-compile-judgment-form-proc name mode clauses contracts nts lang syn-error-name)
+(define-for-syntax (do-compile-judgment-form-proc name mode-stx clauses contracts nts orig stx syn-error-name)
+  (define mode (cdr (syntax->datum mode-stx)))
   (define (compile-clause clause)
     (syntax-case clause ()
       [((_ . conc-pats) . prems)
        (let-values ([(input-pats output-pats) (split-by-mode (syntax->list #'conc-pats) mode)])
-         (define ((rewrite-pattern binds?) pat)
-           (rewrite-side-conditions/check-errs nts syn-error-name binds? pat))
-         (with-syntax ([(lhs (names ...) (names/ellipses ...)) ((rewrite-pattern #t) input-pats)])
+         (with-syntax ([(lhs (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs nts syn-error-name #t input-pats)])
            (define (contracts-compilation ctcs)
              (and ctcs
                   (with-syntax ([(ctc ...) ctcs])
-                    #`(list (compile-pattern #,lang `ctc #f) ...))))
+                    #`(list (compile-pattern lang `ctc #f) ...))))
            (define-values (input-contracts output-contracts)
              (syntax-case contracts ()
                [#f (values #f #f)]
                [(p ...) 
                 (let-values ([(ins outs) (split-by-mode (syntax->list #'(p ...)) mode)])
+                  (define (rewrite-pattern pat)
+                    (rewrite-side-conditions/check-errs nts syn-error-name #f pat))
                   (with-syntax ([((in-pat in-names in-names/ellipses) ...)
-                                 (map (rewrite-pattern #f) ins)]
+                                 (map rewrite-pattern ins)]
                                 [((out-pat out-names out-names/ellipses) ...)
-                                 (map (rewrite-pattern #f) outs)])
-                  (values #'(in-pat ...)
-                          #'(out-pat ...))))]))
+                                 (map rewrite-pattern outs)])
+                    (values #'(in-pat ...)
+                            #'(out-pat ...))))]))
            (define body
-             (bind-withs syn-error-name '() lang nts (syntax->list #'prems) 
-                         'flatten #`(list (term (#,@output-pats))) 
-                         (syntax->list #'(names ...))
-                         (syntax->list #'(names/ellipses ...))
-                         #f))
-           #`(let ([compiled-lhs (compile-pattern #,lang `lhs #t)]
-                   [compiled-input-ctcs #,(contracts-compilation input-contracts)]
-                   [compiled-output-ctcs #,(contracts-compilation output-contracts)])
-               (λ (input)
-                 (check-judgment-form-contract `#,name input compiled-input-ctcs 'I '#,mode)
-                 (combine-judgment-rhses
-                  compiled-lhs
-                  input
-                  (λ (m)
-                    (term-let ([names/ellipses (lookup-binding (mtch-bindings m) 'names)] ...)
-                              #,body))
-                  (λ (output)
-                    (check-judgment-form-contract `#,name output compiled-output-ctcs 'O '#,mode)))))))]))
-  (with-syntax ([(clause-proc ...) (map compile-clause clauses)]
-                [(clause-proc-ids ...) (generate-temporaries clauses)])
-    (with-syntax ([(backwards-ids ...) (reverse (syntax->list #'(clause-proc-ids ...)))])
-      #'(let ([clause-proc-ids clause-proc] ...)
-          (λ (input)
-            (append (backwards-ids input) ...))))))
+             (parameterize ([judgment-form-pending-expansion
+                             (cons name
+                                   (struct-copy judgment-form (lookup-judgment-form-id name)
+                                                [proc #'recur]))])
+               (bind-withs syn-error-name '() #'lang nts (syntax->list #'prems) 
+                           'flatten #`(list (term (#,@output-pats))) 
+                           (syntax->list #'(names ...))
+                           (syntax->list #'(names/ellipses ...))
+                           #f)))
+           (with-syntax ([(compiled-lhs compiled-input-ctcs compiled-output-ctcs)
+                          (generate-temporaries '(compiled-lhs compiled-input-ctcs compiled-output-ctcs))])
+             
+             #`(
+                ;; pieces of a 'let' expression to be combined: first some bindings
+                ([compiled-lhs (compile-pattern lang `lhs #t)]
+                 #,@(if (contracts-compilation input-contracts) 
+                        (list #`[compiled-input-ctcs #,(contracts-compilation input-contracts)])
+                        (list))
+                 #,@(if (contracts-compilation output-contracts)
+                        (list #`[compiled-output-ctcs #,(contracts-compilation output-contracts)])
+                        (list)))
+                ;; and then the body of the let, but expected to be behind a (λ (input) ...).
+                (begin
+                  #,@(if (contracts-compilation input-contracts)
+                         (list #`(check-judgment-form-contract '#,name input compiled-input-ctcs 'I '#,mode))
+                         (list))
+                  (combine-judgment-rhses
+                   compiled-lhs
+                   input
+                   (λ (m)
+                     (term-let ([names/ellipses (lookup-binding (mtch-bindings m) 'names)] ...)
+                               #,body))
+                   #,(if (contracts-compilation output-contracts)
+                         #`(λ (output)
+                             (check-judgment-form-contract '#,name output compiled-output-ctcs 'O '#,mode))
+                         #`void)))))))]))
+  
+  (when (identifier? orig)
+    (define orig-mode (judgment-form-mode (lookup-judgment-form-id orig)))
+    (unless (equal? mode orig-mode)
+      (raise-syntax-error syn-error-name
+                          (format 
+                           "mode for extended judgment form does not match original mode; got ~s for the original and ~s for the extension"
+                           `(,(syntax-e orig) ,@orig-mode)
+                           `(,(syntax-e name) ,@mode))
+                          stx
+                          mode-stx)))
+  
+  (with-syntax ([(((clause-proc-binding ...) clause-proc-body) ...) (map compile-clause clauses)])
+    (with-syntax ([(clause-proc-body-backwards ...) (reverse (syntax->list #'(clause-proc-body ...)))])
+      (if (identifier? orig)
+          (with-syntax ([orig-mk (judgment-form-mk-proc (lookup-judgment-form-id orig))])
+          #`(λ (lang)
+              (let (clause-proc-binding ... ...)
+                (let ([prev (orig-mk lang)])
+                  (λ (recur input)
+                    (append (prev recur input)
+                            clause-proc-body-backwards ...))))))
+          #`(λ (lang)
+              (let (clause-proc-binding ... ...)
+                (λ (recur input)
+                  (append clause-proc-body-backwards ...))))))))
 
 (define (combine-judgment-rhses compiled-lhs input rhs check-output)
   (define mtchs (match-pattern compiled-lhs input))
@@ -539,7 +616,9 @@
   (define (split-body judgment)
     (syntax-case judgment ()
       [(form-name . body)
-       (split-by-mode (syntax->list #'body) (judgment-form-mode (syntax-local-value #'form-name)))]))
+       (split-by-mode (syntax->list #'body) 
+                      (judgment-form-mode
+                       (lookup-judgment-form-id #'form-name)))]))
   (define (drop-ellipses prems)
     (syntax-case prems ()
       [() '()]
@@ -641,7 +720,7 @@
                             (syntax-case clause (where)
                               [(form-name . pieces)
                                (judgment-form-id? #'form-name)
-                               (let*-values ([(mode) (judgment-form-mode (syntax-local-value #'form-name))]
+                               (let*-values ([(mode) (judgment-form-mode (lookup-judgment-form-id #'form-name))]
                                              [(_ outs) (split-by-mode (syntax->list #'pieces) mode)])
                                  (for/fold ([binds binds]) ([out outs])
                                            (append (name-pattern-lws out) binds)))]
@@ -676,17 +755,19 @@
 
 (define-syntax (compile-judgment-form-proc stx)
   (syntax-case stx ()
-    [(_ judgment-form-name lang mode clauses ctcs full-def syn-err-name)
-     (let ([nts (definition-nts #'lang #'full-def (syntax-e #'syn-err-name))])
-       (mode-check (syntax->datum #'mode) (syntax->list #'clauses) nts (syntax-e #'syn-err-name) stx)
-       (do-compile-judgment-form-proc
-        (syntax-e #'judgment-form-name) 
-        (syntax->datum #'mode) 
-        (syntax->list #'clauses) 
-        #'ctcs
-        nts
-        #'lang 
-        (syntax-e #'syn-err-name)))]))
+    [(_ judgment-form-name mode-arg lang clauses ctcs orig full-def syn-err-name)
+     (let ([nts (definition-nts #'lang #'full-def (syntax-e #'syn-err-name))]
+           [clauses (syntax->list #'clauses)]
+           [syn-err-name (syntax-e #'syn-err-name)])
+       (mode-check (cdr (syntax->datum #'mode-arg)) clauses nts syn-err-name stx)
+       (do-compile-judgment-form-proc #'judgment-form-name
+                                      #'mode-arg
+                                      clauses
+                                      #'ctcs
+                                      nts
+                                      #'orig
+                                      #'full-def
+                                      syn-err-name))]))
 
 (define-syntax (compiled-judgment-form-lws stx)
   (syntax-case stx ()
@@ -779,6 +860,7 @@
       (free-identifier=? id #'side-condition/hidden)))
 
 (provide define-judgment-form 
+         define-extended-judgment-form
          judgment-holds
          generate-lws
          (for-syntax extract-term-let-binds
@@ -789,7 +871,9 @@
                      where-keyword?
                      side-condition-keyword?
                      ellipsis?
-                     visible-extras))
+                     visible-extras
+                     judgment-form-id?
+                     lookup-judgment-form-id))
 
 
 (provide --> fresh with I O ;; macro keywords
diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt
index 9bbdff9b66..47d7b246ba 100644
--- a/collects/redex/private/reduction-semantics.rkt
+++ b/collects/redex/private/reduction-semantics.rkt
@@ -260,7 +260,7 @@
   (syntax-case judgment ()
     [(form-name pat ...)
      (judgment-form-id? #'form-name)
-     (let ([expected (length (judgment-form-mode (syntax-local-value #'form-name)))]
+     (let ([expected (length (judgment-form-mode (lookup-judgment-form-id #'form-name)))]
            [actual (length (syntax->list #'(pat ...)))])
        (unless (= actual expected)
          (raise-syntax-error 
@@ -463,7 +463,7 @@
                              (loop (cdr stuffs)
                                    label
                                    computed-label
-                                   (let*-values ([(mode) (judgment-form-mode (syntax-local-value #'form-name))]
+                                   (let*-values ([(mode) (judgment-form-mode (lookup-judgment-form-id #'form-name))]
                                                  [(_ outs) (split-by-mode (syntax->list #'pieces) mode)])
                                      (cons (to-lw/proc #'(form-name . pieces))
                                            (for/fold ([binds scs/withs]) ([out outs])
@@ -1588,12 +1588,15 @@
                                        [(null? anss)
                                         (continue)]
                                        [(not (= 1 (hash-count ht)))
-                                        (redex-error name "~a matched ~s ~a different ways and returned different results" 
+                                        (redex-error name "~a matched ~s ~a returned different results" 
                                                      (if (< num 0)
                                                          "a clause from an extended metafunction"
                                                          (format "clause #~a (counting from 0)" num))
                                                      `(,name ,@exp)
-                                                     (length mtchs))]
+                                                     (if (= 1 (length mtchs))
+                                                         "but"
+                                                         (format "~a different ways and "
+                                                                 (length mtchs))))]
                                        [else
                                         (let ([ans (car anss)])
                                           (unless (ormap (λ (codom-compiled-pattern)
diff --git a/collects/redex/private/term-fn.rkt b/collects/redex/private/term-fn.rkt
index 057e6854f9..bd457f2ab0 100644
--- a/collects/redex/private/term-fn.rkt
+++ b/collects/redex/private/term-fn.rkt
@@ -5,8 +5,9 @@
          term-fn?
          term-fn-get-id
          (struct-out term-id)
+         
          (struct-out judgment-form)
-         judgment-form-id?
+         
          (struct-out defined-term)
          defined-term-id?
          defined-check
@@ -18,18 +19,16 @@
 
 (define-struct term-id (id depth))
 
-(define ((transformer-predicate p?) stx)
+(define (transformer-predicate p? stx)
   (and (identifier? stx)
        (cond [(syntax-local-value stx (λ () #f)) => p?]
              [else #f])))
 
-(define-struct judgment-form (name mode proc lang lws))
-(define judgment-form-id? 
-  (transformer-predicate judgment-form?))
+(define-struct judgment-form (name mode proc mk-proc lang lws))
 
 (define-struct defined-term (value))
-(define defined-term-id?
-  (transformer-predicate defined-term?))
+(define (defined-term-id? stx)
+  (transformer-predicate defined-term? stx))
 
 (define (defined-check id desc #:external [external id])
   (if (eq? (identifier-binding id) 'lexical)
diff --git a/collects/redex/reduction-semantics.rkt b/collects/redex/reduction-semantics.rkt
index 5b83795dec..532d5f3d43 100644
--- a/collects/redex/reduction-semantics.rkt
+++ b/collects/redex/reduction-semantics.rkt
@@ -32,6 +32,7 @@
          define-metafunction/extension
          define-relation
          define-judgment-form
+         define-extended-judgment-form
          judgment-holds
          in-domain?
          caching-enabled?
diff --git a/collects/redex/scribblings/ref.scrbl b/collects/redex/scribblings/ref.scrbl
index 42d14eccca..e7e782131c 100644
--- a/collects/redex/scribblings/ref.scrbl
+++ b/collects/redex/scribblings/ref.scrbl
@@ -1122,20 +1122,20 @@ and @racket[#f] otherwise.
 @defform/subs[#:literals (I O where where/hidden side-condition side-condition/hidden etc.)
              (define-judgment-form language
                option ...
-               rule ...)
+               rule rule ...)
              ([option mode-spec
                       contract-spec]
               [mode-spec (code:line #:mode (form-id pos-use ...))]
               [contract-spec (code:line #:contract (form-id @#,ttpattern ...))]
               [pos-use I
                        O]
-              [rule [conclusion 
-                     premise 
-                     ...]
-                    [premise
+              [rule [premise
                      ...
                      dashes
-                     conclusion]]
+                     conclusion]
+                    [conclusion 
+                     premise 
+                     ...]]
               [conclusion (form-id pat/term ...)]
               [premise (code:line (judgment-form-id pat/term ...) maybe-ellipsis)
                        (where @#,ttpattern @#,tttterm)
@@ -1166,13 +1166,16 @@ For example, the following defines addition on natural numbers:
 @interaction[
 #:eval redex-eval
        (define-language nats
-         (n z (s n)))
+         (n ::= z (s n)))
        (define-judgment-form nats
          #:mode (sum I I O)
          #:contract (sum n n n)
-         [(sum z n n)]
-         [(sum (s n_1) n_2 (s n_3))
-          (sum n_1 n_2 n_3)])]
+         [-----------
+          (sum z n n)]
+         
+         [(sum n_1 n_2 n_3)
+          -------------------------
+          (sum (s n_1) n_2 (s n_3))])]
 
 The @racket[judgment-holds] form checks whether a relation holds for any 
 assignment of pattern variables in output positions.
@@ -1197,9 +1200,12 @@ to compute all pairs with a given sum.
        (define-judgment-form nats
          #:mode (sumr O O I)
          #:contract (sumr n n n)
-         [(sumr z n n)]
-         [(sumr (s n_1) n_2 (s n_3))
-          (sumr n_1 n_2 n_3)])
+         [------------
+          (sumr z n n)]
+         
+         [(sumr n_1 n_2 n_3)
+          --------------------------
+          (sumr (s n_1) n_2 (s n_3))])
        (judgment-holds (sumr n_1 n_2 (s (s z))) (n_1 n_2))]
 
 A rule's @racket[where] and @racket[where/hidden] premises behave as in 
@@ -1209,9 +1215,12 @@ A rule's @racket[where] and @racket[where/hidden] premises behave as in
        (define-judgment-form nats
          #:mode (le I I)
          #:contract (le n n)
-         [(le z n)]
-         [(le (s n_1) (s n_2))
-          (le n_1 n_2)])
+         [--------
+          (le z n)]
+         
+         [(le n_1 n_2)
+          --------------------
+          (le (s n_1) (s n_2))])
        (define-metafunction nats
          pred : n -> n or #f
          [(pred z) #f]
@@ -1219,9 +1228,10 @@ A rule's @racket[where] and @racket[where/hidden] premises behave as in
        (define-judgment-form nats
          #:mode (gt I I)
          #:contract (gt n n)
-         [(gt n_1 n_2)
-          (where n_3 (pred n_1))
-          (le n_2 n_3)])
+         [(where n_3 (pred n_1))
+          (le n_2 n_3)
+          ----------------------
+          (gt n_1 n_2)])
        (judgment-holds (gt (s (s z)) (s z)))
        (judgment-holds (gt (s z) (s z)))]
 
@@ -1239,14 +1249,20 @@ one.
        (define-judgment-form nats
          #:mode (even I)
          #:contract (even n)
-         [(even z)]
-         [(even (s (s n)))
-          (even n)])
+         
+         [--------
+          (even z)]
+         
+         [(even n)
+          ----------------
+          (even (s (s n)))])
+       
        (define-judgment-form nats
          #:mode (all-even I)
          #:contract (all-even (n ...))
-         [(all-even (n ...))
-          (even n) ...])
+         [(even n) ...
+          ------------------
+          (all-even (n ...))])
        (judgment-holds (all-even (z (s (s z)) z)))
        (judgment-holds (all-even (z (s (s z)) (s z))))]
 
@@ -1264,12 +1280,17 @@ non-termination. For example, consider the following definitions:
        (define-judgment-form vertices
          #:mode (path I I)
          #:contract (path v v)
-         [(path v v)]
-         [(path v_1 v_2)
-          (path v_2 v_1)]
-         [(path v_1 v_3)
-          (edge v_1 v_2)
-          (path v_2 v_3)])]
+         [----------
+          (path v v)]
+         
+         [(path v_2 v_1)
+          --------------
+          (path v_1 v_2)]
+         
+         [(edge v_1 v_2)
+          (path v_2 v_3)
+          --------------
+          (path v_1 v_3)])]
 Due to the second @racket[path] rule, the follow query fails to terminate:
 @racketinput[(judgment-holds (path a c))]
 
@@ -1284,7 +1305,18 @@ The @(examples-link "" #t "examples") directory demonstrates three use cases:
       defines an SOS-style semantics in a way that supports mechanized typesetting.}
 @item{@(examples-link "define-judgment-form/multi-val.rkt" #f "multi-val.rkt") ---
       defines a judgment form that serves as a multi-valued metafunction.}]}
+
+@defform[(define-extended-judgment-form language judgment-form-id
+           option ...
+           rule ...)]{
+ Defines a new judgment form that extends @racket[judgment-form-id] 
+ with additional rules. The @racket[option]s and @racket[rule]s
+ are as in @racket[define-judgment-form].
  
+ The mode specification in this judgment form and the original
+ must be the same.
+}
+                             
 @defform*/subs[((judgment-holds judgment)
                 (judgment-holds judgment @#,tttterm))
                ([judgment (judgment-form-id pat/term ...)])]{
diff --git a/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd b/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd
index b6d9a0ec8b..40e6a406e4 100644
--- a/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd
+++ b/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd
@@ -207,3 +207,15 @@
       (K b (use) (name inner-def any))]
      [(K b any K-b-out)])
    (void)))
+
+(#rx"does not match original mode"
+ ([mode2 (J2 I O O)]) ([J2 J2])
+ (let ()
+   (define-language L)
+   (define-judgment-form L
+     #:mode (J1 I I O)
+     [(J1 any_1 any_2 any_2)])
+   (define-extended-judgment-form L J1
+     #:mode mode2
+     [(J2 any_1 17 any_1)])
+   (void)))
diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt
index 13ba50ecdb..46185810e8 100644
--- a/collects/redex/tests/tl-test.rkt
+++ b/collects/redex/tests/tl-test.rkt
@@ -1031,7 +1031,7 @@
     (test (with-handlers ([exn:fail:redex? exn-message])
             (term (f (s (s z))))
             "")
-          #rx"different ways and returned different results"))
+          #rx"returned different results"))
   
   (parameterize ([current-namespace (make-base-namespace)])
     (eval '(require redex/reduction-semantics))
@@ -2254,6 +2254,53 @@
       (test (judgment-holds (R 1 2)) #t)
       (test (judgment-holds (R 1 1)) #f))
     
+    (let ()
+      (define-judgment-form empty-language
+        #:mode (J I O)
+        [(J any_2 any_3)
+         -----------------
+         (J (any_2) any_3)]
+        [---------------------
+         (J variable variable)])
+      
+      
+      (define-extended-judgment-form empty-language J 
+        #:mode (J2 I O)
+        
+        [------------------
+         (J2 number number)]
+        
+        [(J2 any_1 any_3)
+         ------------------------
+         (J2 (any_1 any_2) any_3)])
+      
+      (test (judgment-holds (J (x) any) any) '(x))
+      (test (judgment-holds (J2 (1 y) any) any) '(1))
+      (test (judgment-holds (J2 (x y) any) any) '(x))
+      (test (judgment-holds (J2 ((((x) z) y)) any) any) '(x))
+      (test (judgment-holds (J2 ((((11) z) y)) any) any) '(11)))
+    
+    (let ()
+      
+      (define-language L1
+        (n 1 2 3))
+      
+      (define-extended-language L2 L1
+        (n .... 4 5 6))
+      
+      (define-judgment-form L1
+        #:mode (J1 I O)
+        [-----------
+         (J1 n_1 n_1)])
+      
+      (define-extended-judgment-form L2 J1 
+        #:mode (J2 I O))
+      
+      (test (judgment-holds (J1 1 any) any) '(1))
+      (test (judgment-holds (J2 1 any) any) '(1))
+      (test (judgment-holds (J2 4 any) any) '(4)))
+
+    
     (parameterize ([current-namespace (make-base-namespace)])
       (eval '(require errortrace))
       (eval '(require redex/reduction-semantics))
diff --git a/doc/release-notes/redex/HISTORY.txt b/doc/release-notes/redex/HISTORY.txt
index 12abd6f6c7..4fe659cd88 100644
--- a/doc/release-notes/redex/HISTORY.txt
+++ b/doc/release-notes/redex/HISTORY.txt
@@ -4,6 +4,8 @@ v5.2.2
 
   * added define-union-language
 
+  * added define-extended-judgment-form
+
 v5.2.1
 
   * rewrote the internals of the pattern matcher to be more consistent