src/HOL/Real/Hyperreal/Filter.ML
changeset 7127 48e235179ffb
parent 6024 cb87f103d114
child 7219 4e3f386c2e37
     1.1 --- a/src/HOL/Real/Hyperreal/Filter.ML	Wed Jul 28 22:01:58 1999 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/Filter.ML	Thu Jul 29 12:44:57 1999 +0200
     1.3 @@ -4,9 +4,6 @@
     1.4      Description : Filters and Ultrafilter
     1.5  *) 
     1.6  
     1.7 -open Filter;
     1.8 -
     1.9 -
    1.10  (*------------------------------------------------------------------
    1.11        Properties of Filters and Freefilters - 
    1.12        rules for intro, destruction etc.
    1.13 @@ -290,7 +287,7 @@
    1.14               A few properties of freefilters
    1.15   -------------------------------------------------------------------*)
    1.16  
    1.17 -Goal "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int - Y) Int F1)";
    1.18 +Goal "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int (- Y)) Int F1)";
    1.19  by (Auto_tac);
    1.20  qed "lemma_Compl_cancel_eq";
    1.21  
    1.22 @@ -303,7 +300,7 @@
    1.23  qed "finite_IntI2";
    1.24  
    1.25  Goal "[| finite (F1 Int Y); \
    1.26 -\                 finite (F2 Int - Y) \
    1.27 +\                 finite (F2 Int (- Y)) \
    1.28  \              |] ==> finite (F1 Int F2)";
    1.29  by (res_inst_tac [("Y1","Y")] (lemma_Compl_cancel_eq RS ssubst) 1);
    1.30  by (rtac finite_UnI 1);
    1.31 @@ -403,7 +400,7 @@
    1.32     We prove: 1. Existence of maximal filter i.e. ultrafilter
    1.33               2. Freeness property i.e ultrafilter is free
    1.34               Use a locale to prove various lemmas and then 
    1.35 -             export main result- The Ultrafilter Theorem
    1.36 +             export main result: The Ultrafilter Theorem
    1.37   -------------------------------------------------------------------*)
    1.38  Open_locale "UFT"; 
    1.39  
    1.40 @@ -516,8 +513,9 @@
    1.41  by (res_inst_tac [("x","Union c")] bexI 1 THEN Blast_tac 1);
    1.42  by (rtac Un_chain_mem_cofinite_Filter_set 1 THEN REPEAT(assume_tac 1));
    1.43  by (res_inst_tac [("x","frechet (UNIV)")] bexI 1 THEN Blast_tac 1);
    1.44 -by (auto_tac (claset(),simpset() addsimps 
    1.45 -        [thm "superfrechet_def", thm "frechet_def"]));
    1.46 +by (auto_tac (claset(),
    1.47 +	      simpset() addsimps 
    1.48 +	      [thm "superfrechet_def", thm "frechet_def"]));
    1.49  qed "max_cofinite_Filter_Ex";
    1.50  
    1.51  Goal "EX U: superfrechet UNIV. (\