src/HOL/NSA/Filter.thy
changeset 28823 dcbef866c9e2
parent 27681 8cedebf55539
child 36176 3fe7e97ccca8
     1.1 --- a/src/HOL/NSA/Filter.thy	Mon Nov 17 17:00:27 2008 +0100
     1.2 +++ b/src/HOL/NSA/Filter.thy	Mon Nov 17 17:00:55 2008 +0100
     1.3 @@ -77,10 +77,9 @@
     1.4  apply (simp add: singleton)
     1.5  done
     1.6  
     1.7 -lemma (in freeultrafilter) filter: "filter F" by unfold_locales
     1.8 +lemma (in freeultrafilter) filter: "filter F" ..
     1.9  
    1.10 -lemma (in freeultrafilter) ultrafilter: "ultrafilter F"
    1.11 -  by unfold_locales
    1.12 +lemma (in freeultrafilter) ultrafilter: "ultrafilter F" ..
    1.13  
    1.14  
    1.15  subsection {* Collect properties *}