# HG changeset patch
# User wenzelm
# Date 1003857197 -7200
# Node ID e1aa90e4ef4ee6abbf3998209d7c05797516ca02
# Parent  f8f37d61fbc223175d33e4f991bb2daad38f953e
apply(simp add: three_def numerals)   (* FIXME !? *);

diff -r f8f37d61fbc2 -r e1aa90e4ef4e doc-src/TutorialI/Types/Typedefs.thy
--- a/doc-src/TutorialI/Types/Typedefs.thy	Tue Oct 23 19:12:58 2001 +0200
+++ b/doc-src/TutorialI/Types/Typedefs.thy	Tue Oct 23 19:13:17 2001 +0200
@@ -203,7 +203,7 @@
 @{prop"n=2"} which are trivial for simplification:
 *}
 
-apply(simp add: three_def numerals)
+apply(simp add: three_def numerals)   (* FIXME !? *)
 apply((erule le_SucE)+)
 apply simp_all
 done