equal
deleted
inserted
replaced
3 Copyright 1994 University of Cambridge |
3 Copyright 1994 University of Cambridge |
4 |
4 |
5 Examples of performing binary arithmetic by simplification. |
5 Examples of performing binary arithmetic by simplification. |
6 *) |
6 *) |
7 |
7 |
8 theory BinEx imports Main begin |
8 theory BinEx imports ZF begin |
9 (*All runtimes below are on a 300MHz Pentium*) |
9 (*All runtimes below are on a 300MHz Pentium*) |
10 |
10 |
11 lemma "#13 $+ #19 = #32" |
11 lemma "#13 $+ #19 = #32" |
12 by simp (*0 secs*) |
12 by simp (*0 secs*) |
13 |
13 |