equal
deleted
inserted
replaced
793 |
793 |
794 \item @{method atomize} (as a method) rewrites any non-atomic |
794 \item @{method atomize} (as a method) rewrites any non-atomic |
795 premises of a sub-goal, using the meta-level equations declared via |
795 premises of a sub-goal, using the meta-level equations declared via |
796 @{attribute atomize} (as an attribute) beforehand. As a result, |
796 @{attribute atomize} (as an attribute) beforehand. As a result, |
797 heavily nested goals become amenable to fundamental operations such |
797 heavily nested goals become amenable to fundamental operations such |
798 as resolution (cf.\ the @{method rule} method). Giving the ``@{text |
798 as resolution (cf.\ the @{method (Pure) rule} method). Giving the ``@{text |
799 "(full)"}'' option here means to turn the whole subgoal into an |
799 "(full)"}'' option here means to turn the whole subgoal into an |
800 object-statement (if possible), including the outermost parameters |
800 object-statement (if possible), including the outermost parameters |
801 and assumptions as well. |
801 and assumptions as well. |
802 |
802 |
803 A typical collection of @{attribute atomize} rules for a particular |
803 A typical collection of @{attribute atomize} rules for a particular |