src/HOL/Real/Hyperreal/Filter.ML
changeset 6024 cb87f103d114
parent 5979 11cbf236ca16
child 7127 48e235179ffb
     1.1 --- a/src/HOL/Real/Hyperreal/Filter.ML	Fri Dec 11 10:38:51 1998 +0100
     1.2 +++ b/src/HOL/Real/Hyperreal/Filter.ML	Fri Dec 11 10:41:53 1998 +0100
     1.3 @@ -552,6 +552,6 @@
     1.4  
     1.5  val FreeUltrafilter_Ex  = export FreeUltrafilter_ex;
     1.6  
     1.7 -Close_locale();
     1.8 +Close_locale "UFT";
     1.9  
    1.10