Lines Matching defs:implementation
11 of proof programming. The first implementation is the obvious one, but
13 implementation produces a much more streamlined proof, but still has a
15 library \ml{taut}. The third implementation replaces the general
17 fourth and final implementation uses an optimised implementation of
26 the so called ``even more efficient implementation'' is actually
57 \section{A simple implementation}
59 A first implementation uses `brute-force' rewriting with
219 The implementation of the special purpose conversion,
438 \section{A more efficient implementation}
618 \section{An even more efficient implementation}\label{bogus-optimization}
620 Although the implementation just given is much faster than the first
1289 Although the optimized implementation is much more efficient, it uses
1290 less general methods. An advantage of the simple implementation based