Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nat_Transfer.thy
changeset 33340 a165b97f3658
parent 33318 ddd97d9dfbfb
child 35551 85aada96578b 
--- a/src/HOL/Nat_Transfer.thy	Thu Oct 29 13:37:55 2009 +0100
+++ b/src/HOL/Nat_Transfer.thy	Thu Oct 29 22:13:09 2009 +0100
@@ -67,8 +67,7 @@
     "(2::int) >= 0"
     "(3::int) >= 0"
     "int z >= 0"
-  apply (auto simp add: zero_le_mult_iff tsub_def)
-done
+  by (auto simp add: zero_le_mult_iff tsub_def)
 
 lemma transfer_nat_int_relations:
     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
isabelle