src/HOL/Nat_Transfer.thy
changeset 33340 a165b97f3658
parent 33318 ddd97d9dfbfb
child 35551 85aada96578b
     1.1 --- a/src/HOL/Nat_Transfer.thy	Thu Oct 29 13:37:55 2009 +0100
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Thu Oct 29 22:13:09 2009 +0100
     1.3 @@ -67,8 +67,7 @@
     1.4      "(2::int) >= 0"
     1.5      "(3::int) >= 0"
     1.6      "int z >= 0"
     1.7 -  apply (auto simp add: zero_le_mult_iff tsub_def)
     1.8 -done
     1.9 +  by (auto simp add: zero_le_mult_iff tsub_def)
    1.10  
    1.11  lemma transfer_nat_int_relations:
    1.12      "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>