changeset 5132 | 24f992a25adc |
parent 5068 | fb28eaa07e01 |
child 10798 | 0a1446ff6aff |
--- a/src/HOLCF/IOA/meta_theory/Simulations.ML Fri Jul 10 15:24:22 1998 +0200 +++ b/src/HOLCF/IOA/meta_theory/Simulations.ML Sun Jul 12 11:49:17 1998 +0200 @@ -10,7 +10,7 @@ Goal "(A~={}) = (? x. x:A)"; by (safe_tac set_cs); -auto(); +by Auto_tac; qed"set_non_empty"; Goal "(A Int B ~= {}) = (? x. x: A & x:B)";