| changeset 7839 | 03fd460cb8b8 |
| parent 7499 | 23e090051cb8 |
| child 8067 | 225e3b45b766 |
--- a/src/HOL/UNITY/GenPrefix.ML Tue Oct 12 19:14:06 1999 +0200 +++ b/src/HOL/UNITY/GenPrefix.ML Wed Oct 13 12:03:22 1999 +0200 @@ -226,6 +226,12 @@ by Auto_tac; qed "prefix_less_le"; +(*Monotonicity of "set" operator WRT prefix*) +Goalw [prefix_def] "xs <= ys ==> set xs <= set ys"; +by (etac genPrefix.induct 1); +by Auto_tac; +qed "set_mono"; + (** recursion equations **)