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);