equal
deleted
inserted
replaced
72 \noindent |
72 \noindent |
73 For efficiency's sake, this built-in prover ignores quantified formulae and all |
73 For efficiency's sake, this built-in prover ignores quantified formulae and all |
74 arithmetic operations apart from addition. |
74 arithmetic operations apart from addition. |
75 |
75 |
76 The method \methdx{arith} is more general. It attempts to prove |
76 The method \methdx{arith} is more general. It attempts to prove |
77 the first subgoal provided it is a quantifier free \textbf{linear arithmetic} formula. |
77 the first subgoal provided it is a quantifier-free \textbf{linear arithmetic} |
78 Such formulas may involve the |
78 formula. Such formulas may involve the |
79 usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}}, |
79 usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}}, |
80 \isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}}, |
80 \isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}}, |
81 and the operations |
81 and the operations |
82 \isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. |
82 \isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. |
83 For example,% |
83 For example,% |