Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
whitespace tuning
authorhaftmann
Fri, 07 Mar 2008 13:53:04 +0100
changeset 26235 96b804999ca7
parent 26234 1f6e28a88785
child 26236 0490a5dddd27
whitespace tuning
src/HOL/Wellfounded_Recursion.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Wellfounded_Recursion.thy	Fri Mar 07 13:53:03 2008 +0100
+++ b/src/HOL/Wellfounded_Recursion.thy	Fri Mar 07 13:53:04 2008 +0100
@@ -530,7 +530,7 @@
   "pred_nat = {(m, n). n = Suc m}"
 
 definition
-  less_than :: "(nat * nat)set" where
+  less_than :: "(nat * nat) set" where
   "less_than = pred_nat^+"
 
 lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n"
isabelle