# HG changeset patch
# User nipkow
# Date 1113583415 -7200
# Node ID d63e7a65b2d0a95f9fadd43c2eb5d592c7133a9a
# Parent  bb2acfed8212bcf9f2c581eb62bc47e41b06c572
rermoved pointless example

diff -r bb2acfed8212 -r d63e7a65b2d0 doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Fri Apr 15 18:16:05 2005 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Fri Apr 15 18:43:35 2005 +0200
@@ -236,10 +236,6 @@
 *};
 oops
 
-lemma "(3/4) * (10^15) < (x :: real)"
-apply simp 
-oops
-
 text{*
 Ring and Field