src/HOL/Real/Hyperreal/Filter.ML
changeset 8856 435187ffc64e
parent 7958 f531589c9fc1
child 9108 9fff97d29837
     1.1 --- a/src/HOL/Real/Hyperreal/Filter.ML	Wed May 10 21:04:16 2000 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/Filter.ML	Wed May 10 22:34:30 2000 +0200
     1.3 @@ -552,5 +552,3 @@
     1.4  val FreeUltrafilter_Ex  = export FreeUltrafilter_ex;
     1.5  
     1.6  Close_locale "UFT";
     1.7 -
     1.8 -