# HG changeset patch
# User haftmann
# Date 1204894384 -3600
# Node ID 96b804999ca7ecbeb659a880ffe9aa35f1417f4f
# Parent  1f6e28a8878508562bbf78e26a9505445530ebf4
whitespace tuning

diff -r 1f6e28a88785 -r 96b804999ca7 src/HOL/Wellfounded_Recursion.thy
--- 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"