| changeset 7713 | f4fe9d620107 |
| parent 7109 | b02c6bdda05b |
| child 9969 | 4753185f1dd2 |
--- a/src/HOL/mono.ML Tue Oct 05 15:25:35 1999 +0200 +++ b/src/HOL/mono.ML Tue Oct 05 15:25:52 1999 +0200 @@ -115,3 +115,11 @@ by (Force_tac 1); by (force_tac (claset() addSIs [order_antisym], simpset()) 1); qed "Least_mono"; + +Goal "[| a = b; c = d; b --> d |] ==> a --> c"; +by (Fast_tac 1); +qed "eq_to_mono"; + +Goal "[| a = b; c = d; ~ b --> ~ d |] ==> ~ a --> ~ c"; +by (Fast_tac 1); +qed "eq_to_mono2";