# 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";