diff -r a207114007c6 -r 83afe527504d src/HOL/ex/Arith_Examples.thy
--- a/src/HOL/ex/Arith_Examples.thy	Sat Aug 18 17:42:39 2007 +0200
+++ b/src/HOL/ex/Arith_Examples.thy	Sat Aug 18 19:25:28 2007 +0200
@@ -130,6 +130,12 @@
   apply (tactic {* lin_arith_pre_tac @{context} 1 *})
 oops
 
+lemma "-(i::int) * 1 = 0 ==> i = 0"
+  by (tactic {* fast_arith_tac @{context} 1 *})
+
+lemma "[| (0::int) < abs i; abs i * 1 < abs i * j |] ==> 1 < abs i * j"
+  by (tactic {* fast_arith_tac @{context} 1 *})
+
 
 subsection {* Meta-Logic *}