apply(simp add: three_def numerals) (* FIXME !? *);
authorwenzelm
Tue, 23 Oct 2001 19:13:17 +0200
changeset 11901 e1aa90e4ef4e
parent 11900 f8f37d61fbc2
child 11902 db207d68392c
apply(simp add: three_def numerals) (* FIXME !? *);
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