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