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/ex/Fundefs.thy
changeset 23315 df3a7e9ebadb
parent 23117 e2744f32641e
child 23817 ee3ee9ea0d34 
--- a/src/HOL/ex/Fundefs.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/ex/Fundefs.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -149,7 +149,7 @@
     with divmod have "x = 2 * (x div 2) + 1" by simp
     with c2 show "P" .
   qed
-qed presburger+ -- {* solve compatibility with presburger *}
+qed presburger+ -- {* solve compatibility with presburger *} 
 termination by lexicographic_order
 
 thm ev.simps
isabelle