--- a/doc-src/TutorialI/Misc/fakenat.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/fakenat.thy Sun Aug 06 15:26:53 2000 +0200
@@ -7,7 +7,7 @@
numbers is predefined and behaves like
*}
-datatype nat = "0" | Suc nat
+datatype nat = 0 | Suc nat
(*<*)
end
(*>*)