# HG changeset patch
# User wenzelm
# Date 1121354495 -7200
# Node ID 581764860c2b8387e7610e05f2b0d7c5e4c1db8b
# Parent  c90a1f450327d99faf8af54a0ae2dd611d112f04
tuned;

diff -r c90a1f450327 -r 581764860c2b src/HOL/Real/Float.ML
--- a/src/HOL/Real/Float.ML	Thu Jul 14 17:16:52 2005 +0200
+++ b/src/HOL/Real/Float.ML	Thu Jul 14 17:21:35 2005 +0200
@@ -17,11 +17,6 @@
 =
 struct
 
-fun fst (a,b) = a
-fun snd (a,b) = b
-
-val filter = List.filter;
-
 exception Destruct_floatstr of string;
 
 fun destruct_floatstr isDigit isExp number = 
diff -r c90a1f450327 -r 581764860c2b src/HOL/Real/ROOT.ML
--- a/src/HOL/Real/ROOT.ML	Thu Jul 14 17:16:52 2005 +0200
+++ b/src/HOL/Real/ROOT.ML	Thu Jul 14 17:21:35 2005 +0200
@@ -7,5 +7,4 @@
 by Jacques Fleuriot
 *)
 
-time_use_thy "Real";
-use_thy "Float";
\ No newline at end of file
+time_use_thy "Float";