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/Import/HOL4Compat.thy
changeset 20432 07ec57376051
parent 20269 c40070317ab8
child 23389 aaca6a8e5414 
--- a/src/HOL/Import/HOL4Compat.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Import/HOL4Compat.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -221,7 +221,7 @@
   by simp
 
 lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
-  by simp
+  by (simp, arith)
 
 lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
   by (simp add: max_def)
isabelle