feat: Implement Sec 5.3.1 tests

And put in generic documentation for all the remaining tests.
  If any particular tests need individual commentary, it can always be
  added later.

trans/prop-dnf-rules.str

@@ -66,7 +66,9 @@ trying our different Stratego transformations.
 So, we can just take our `test3` expression above and make it a part of
 an SPT test suite, which we will call `test/manual-suite.spt`:
 ```SPT
-{! ../test/manual-suite.spt terminate: '(.*run dnf)' !}
+{! ../test/manual-suite.spt extract:
+  start: '\*\*/'
+terminate: '(.*run dnf)' !}
 ```
 
 Once we have saved this file, the tests run automatically. What does this mean?
@@ -83,7 +85,9 @@ If we use an AST like `Atom("x")` that can't possibly be the actual output
 what the transformation actually produced. So we add just a bit to
 `test/manual-suite.spt`:
 ```SPT
-{! ../test/manual-suite.spt terminate: '(.*run dnf.*)$' !}
+{! ../test/manual-suite.spt extract:
+  start: '\*\*/'
+terminate: '(.*run dnf.*)$' !}
 ```
 
 and now sure enough a little error symbol appears next to the test. If you hover

trans/prop-laws.str

@@ -0,0 +1,22 @@
+module prop-laws
+imports libstrategolib signatures/-
+rules
+
+  DefI : Impl(x, y) -> Or(Not(x), y)
+  DefE : Eq(x, y)   -> And(Impl(x, y), Impl(y, x))
+
+  DN   : Not(Not(x)) -> x
+
+  DMA  : Not(And(x, y)) -> Or(Not(x), Not(y))
+  DMO  : Not(Or(x, y))  -> And(Not(x), Not(y))
+
+  DAOL : And(Or(x, y), z) -> Or(And(x, z), And(y, z))
+  DAOR : And(z, Or(x, y)) -> Or(And(z, x), And(z, y))
+
+  DOAL : Or(And(x, y), z) -> And(Or(x, z), Or(y, z))
+  DOAR : Or(z, And(x, y)) -> And(Or(z, x), Or(z, y))
+
+strategies
+
+  dnf4 = innermost(DefI <+ DefE <+ DAOL <+ DAOR <+ DN <+ DMA <+ DMO)
+  cnf4 = innermost(DefI <+ DefE <+ DOAL <+ DOAR <+ DN <+ DMA <+ DMO)

trans/spoofax_propositional_language.str

@@ -10,6 +10,7 @@ imports
   prop-dnf
   prop-dnf3
   prop-cnf3
+  prop-laws
 
 rules // Debugging