--- a/src/ZF/Induct/Brouwer.thy Fri Dec 03 20:26:57 2010 +0100
+++ b/src/ZF/Induct/Brouwer.thy Fri Dec 03 20:38:58 2010 +0100
@@ -39,7 +39,7 @@
done
-subsection {* The Martin-Löf wellordering type *}
+subsection {* The Martin-Löf wellordering type *}
consts
Well :: "[i, i => i] => i"