equal
deleted
inserted
replaced
5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 header{*Arithmetic with simplification*} |
8 header{*Arithmetic with simplification*} |
9 |
9 |
10 theory ArithSimp = Arith |
10 theory ArithSimp |
11 files "arith_data.ML": |
11 imports Arith |
|
12 files "~~/src/Provers/Arith/cancel_numerals.ML" |
|
13 "~~/src/Provers/Arith/combine_numerals.ML" |
|
14 "arith_data.ML" |
|
15 |
|
16 begin |
12 |
17 |
13 subsection{*Difference*} |
18 subsection{*Difference*} |
14 |
19 |
15 lemma diff_self_eq_0 [simp]: "m #- m = 0" |
20 lemma diff_self_eq_0 [simp]: "m #- m = 0" |
16 apply (subgoal_tac "natify (m) #- natify (m) = 0") |
21 apply (subgoal_tac "natify (m) #- natify (m) = 0") |