equal
deleted
inserted
replaced
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header {* Binary arithmetic examples *} |
7 header {* Binary arithmetic examples *} |
8 |
8 |
9 theory BinEx = Main: |
9 theory BinEx imports Main begin |
10 |
10 |
11 subsection {* Regression Testing for Cancellation Simprocs *} |
11 subsection {* Regression Testing for Cancellation Simprocs *} |
12 |
12 |
13 (*taken from HOL/Integ/int_arith1.ML *) |
13 (*taken from HOL/Integ/int_arith1.ML *) |
14 |
14 |