Some/many rules can be used both ways. For example, in propositional
logic we have
<verbatim>
  A10 : Impl(x, y) -> Or(Not(x), y)
  A11 : Or(Not(x), y) -> Impl(x, y)
</verbatim>
It would be more attractive to be able to write
<verbatim>
  A10 : Impl(x, y) <-> Or(Not(x), y)
</verbatim>
then, A10L would refer to the first rule and A10R to the second

-- Main.EelcoVisser - 27 Oct 2001 <br>

----
CategoryToDo | LanguageExtensions