- Finally wrote the translation from Isabelle terms to spider diagrams.
authorMatej Urbas <matej.urbas@gmail.com>
Sun, 22 Apr 2012 11:27:41 +0000 (12:27 +0100)
committerMatej Urbas <matej.urbas@gmail.com>
Sun, 22 Apr 2012 11:27:41 +0000 (12:27 +0100)
commit04091fcb2f62b95899caa0743ee5b166cafaa9a0
tree2b2d579e90a6b0d30ff3ea9d8a75fbc786fc42be
parentba7dfc2ce899770fdcc2a4534547139b74488eb4
- Finally wrote the translation from Isabelle terms to spider diagrams.
- The translation procedure uses formula normalisation for spider habitat specifications. Thus, a much greater freedom is given to the user when specifying habitats of spiders in a unitary spider diagram. We still have to add disjunctive habitat-specifying terms (but this should be extremely easy).
devel/SpeedithIsabelle/src/speedith/diabelli/isabelle/NormalForms.scala [new file with mode: 0644]
devel/SpeedithIsabelle/src/speedith/diabelli/isabelle/Translations.scala