equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} |
9 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} |
10 |
10 |
11 theory Int |
11 theory Int |
12 imports Equiv_Relations Nat Wellfounded_Relations |
12 imports Equiv_Relations Nat Wellfounded |
13 uses |
13 uses |
14 ("Tools/numeral.ML") |
14 ("Tools/numeral.ML") |
15 ("Tools/numeral_syntax.ML") |
15 ("Tools/numeral_syntax.ML") |
16 ("~~/src/Provers/Arith/assoc_fold.ML") |
16 ("~~/src/Provers/Arith/assoc_fold.ML") |
17 "~~/src/Provers/Arith/cancel_numerals.ML" |
17 "~~/src/Provers/Arith/cancel_numerals.ML" |