src/HOL/Hyperreal/NSA.ML

--- a/src/HOL/Hyperreal/NSA.ML	Tue Dec 16 23:24:17 2003 +0100
+++ b/src/HOL/Hyperreal/NSA.ML	Wed Dec 17 16:23:52 2003 +0100
@@ -1967,8 +1967,6 @@
 by (dres_inst_tac [("x","u")] spec 1 THEN
     REPEAT(dtac FreeUltrafilterNat_Compl_mem 1));
 by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
-
-
 by (asm_full_simp_tac (simpset() addsimps [lemma_Compl_eq,
     lemma_Compl_eq2,lemma_Int_eq1]) 1);
 by (auto_tac (claset() addDs [FreeUltrafilterNat_const_Finite],