diff --git a/docrefs/sec5.1.2.md b/docrefs/sec5.1.2.md
new file mode 100644
index 0000000..dfe21f8
--- /dev/null
+++ b/docrefs/sec5.1.2.md
@@ -0,0 +1 @@
+[Section 5.1.2](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/05-rewriting-strategies.html#attempt-2-functionalization)
\ No newline at end of file
diff --git a/mkdocs.yml b/mkdocs.yml
index 2cbe8f2..41a15dd 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -12,6 +12,7 @@ nav:
 - syntax/Spoofax-Propositional-Language.md
 - trans/prop-eval-rules.md
 - trans/prop-dnf-rules.md
+- trans/prop-dnf3.md
 theme:
   name: readthedocs
 markdown_extensions:
diff --git a/trans/prop-dnf-rules.str b/trans/prop-dnf-rules.str
index bbce794..42e32ea 100644
--- a/trans/prop-dnf-rules.str
+++ b/trans/prop-dnf-rules.str
@@ -35,7 +35,7 @@ Now just importing `prop-dnf` in `trans/spoofax-propositional-language.str`
 and adding a menu item to `editor/Manual.esv`:
 ```ESV
  ...
-{! ../editor/Manual.esv extract: {start: menus} !}
+{! ../editor/Manual.esv extract: {start: menus, stop: dnf3} !}
 ```
 should suffice to make the dnf strategy available in the "Spoofax > Manual"
 menu.
diff --git a/trans/prop-dnf3.str b/trans/prop-dnf3.str
index 6583969..6b9d0a3 100644
--- a/trans/prop-dnf3.str
+++ b/trans/prop-dnf3.str
@@ -1,3 +1,24 @@
+/** md
+Title: Running a Strategy: the command line
+
+## Functionalizing reduction rules
+
+The {! ../docrefs/manual.md !} next goes on, in Chapter 5, to consider ways to
+add the ability to also compute conjunctive normal forms for propositional
+ASTs. The rules for this form cannot simply be added to those from the prior
+chapter for disjunctive normal form, as they would produce a non-terminating
+rewrite system.
+
+The first method for which working examples are provided is the method of
+"functionalization" in {! ../docrefs/sec5.1.2.md !}. Although an anti-pattern
+in the views of the Spoofax designers, the examples are still instructive and
+of course we want to implement them here.
+
+So, we can grab the Stratego code given in the section as our
+`trans/prop-dnf3.str`:
+```Stratego
+**/
+/** md  Include this code in docs: */
 module prop-dnf3
 imports libstrategolib signatures/-
 signature
@@ -28,4 +49,64 @@ strategies
   // Interface dnf3 strategy with editor services and file system
   do-dnf3: (selected, _, _, path, project-path) -> (filename, result)
     with filename := <guarantee-extension(|"dnf.aterm")> path
-       ; result   := <dnf3> selected
\ No newline at end of file
+       ; result   := <dnf3> selected
+/* End of code inclusion **/
+/** md  Conclusion of documentation:
+```
+
+Notice the few minor differences from the manual. We import `signatures/-` as
+before. We've used a fresh identifier for the `E` and `D` rules, because unlike
+in the manual, all of our Stratego files are imported into the same main
+`trans/spoofax_propositional_language.str` module. So they must live together,
+but as noted in the manual, these functionalized rules do not "play together"
+nicely with the evaluation `E` rules introduced [earlier](prop-eval-rules.md).
+And we've renamed the `dnf` rule to `make-nf` -- for a reason that will
+become clear in a moment -- but incorporated the wrapping by `Dnf` of the AST
+we want to compute the DNF of into the `dnf3` strategy, since our concrete
+syntax has no way of specifying such a wrapping.
+
+Also as before, we've created a `syntax/examples/sec_5_1_2_test1.spl`
+(which it turns out is just the same as `sec_4_2_test3.spl`)
+and a menu item and a `test/manual-suite.spt` case called `sec5_1_2_test1_ex` to
+see that all is working well. Applying `dnf3` to the test file produces
+```
+{! ../syntax/examples/sec5.1.2_test1.dnf.aterm !}
+```
+which is correct. (Note the contrast with what's shown in
+{! ../docrefs/sec5.1.2.md !} as the output of the `prop-dnf3` program,
+in which the recurring "ATom" typo has blocked
+the reductive elimination of some of the occurrences of the Dnf function
+symbol. Of course, as the manual itself points out, in proper operation of
+this functionalization approach, all of the function symbols must reduce away
+to end up back in an AST of the subject language.)
+
+So now we can move on to the conjunctive normal form. The Stratego code
+for the CNF is not given explicitly in the manual, but it consists of:
+```
+{! prop-cnf3.str !}
+```
+
+Note in particular we have not repeated the `make-nf` strategy -- that's the
+entire point of functionalization; we can use the same top-level reduction
+scheme because the introduced function symbols keep track of what operations
+are being performed. We also introduce a strategy `dcnf` for the simultaneous
+construction of DNF and CNF, as noted in the manual.
+
+Again, there are menu items and SPT cases for the `cnf3` and `dcnf` strategies
+as well. There's one caveat here, though. The test case for `dcnf`:
+```SPT
+{! ../test/manual-suite.spt extract:
+  start: '^(.*test.*both.*\n?)$'
+!}
+```
+does not actually work, because of what appears to be a bug in SPT: the `to`
+in the expectation line is interpreted as part of the expected AST. However,
+the error message does show that the transformation is operating properly.
+
+We can now use this example to show yet another way to try Stratego stragies
+with the Spoofax IDE implementation.
+
+### Command-line Utilities
+
+[HERE]
+**/
\ No newline at end of file
diff --git a/trans/prop-eval-rules.str b/trans/prop-eval-rules.str
index c36d88f..5ee5638 100644
--- a/trans/prop-eval-rules.str
+++ b/trans/prop-eval-rules.str
@@ -114,7 +114,8 @@ by importing the `prop-eval` module in the main Stratego file for our language,
 in this case `trans/spoofax_propositional_language.str`:
 ```Stratego
 {! spoofax_propositional_language.str extract:
-  replace: ['prop-dnf']
+  - stop: 'prop-dnf'
+  - start: '^(.*rule.*)$'
 terminate: debug-show
 !}
   [ ... rest of file suppressed. ]