| changeset 12018 | ec054019c910 |
| parent 11868 | 56db9f3a6b3e |
| child 12486 | 0ed8bdd883e0 |
--- a/src/HOL/Integ/IntArith.ML Thu Nov 01 21:12:13 2001 +0100 +++ b/src/HOL/Integ/IntArith.ML Fri Nov 02 17:55:24 2001 +0100 @@ -4,6 +4,11 @@ *) +Goal "x - - y = x + (y::int)"; +by (Simp_tac 1); +qed "int_diff_minus_eq"; +Addsimps [int_diff_minus_eq]; + Goal "abs(abs(x::int)) = abs(x)"; by(arith_tac 1); qed "abs_abs";