src/HOL/Nat.thy
changeset 44890 22f665a2e91c
parent 44848 f4d0b060c7ca
child 45231 d85a2fdc586c
     1.1 --- a/src/HOL/Nat.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -320,7 +320,7 @@
     1.4  
     1.5  lemma one_eq_mult_iff [simp,no_atp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
     1.6    apply (rule trans)
     1.7 -  apply (rule_tac [2] mult_eq_1_iff, fastsimp)
     1.8 +  apply (rule_tac [2] mult_eq_1_iff, fastforce)
     1.9    done
    1.10  
    1.11  lemma nat_mult_eq_1_iff [simp]: "m * n = (1::nat) \<longleftrightarrow> m = 1 \<and> n = 1"