changeset 10095 | 16292f1471ad |
parent 10045 | c76b73e16711 |
child 10156 | 9d4d5852eb47 |
--- a/src/HOL/Real/Hyperreal/Star.ML Wed Sep 27 19:36:31 2000 +0200 +++ b/src/HOL/Real/Hyperreal/Star.ML Wed Sep 27 19:37:32 2000 +0200 @@ -5,7 +5,7 @@ *) (*-------------------------------------------------------- - Preamble - Pulling "?" over "!" + Preamble - Pulling "EX" over "ALL" ---------------------------------------------------------*) (* This proof does not need AC and was suggested by the