| changeset 4109 | b131edcfeac3 |
| parent 4091 | 771b1f6422a8 |
| child 4152 | 451104c223e2 |
--- a/src/ZF/ex/misc.ML Mon Nov 03 21:56:59 1997 +0100 +++ b/src/ZF/ex/misc.ML Tue Nov 04 09:26:15 1997 +0100 @@ -14,7 +14,7 @@ by (Blast_tac 1); result(); -set_current_thy"Perm"; +context Perm.thy; (*Example 12 (credited to Peter Andrews) from W. Bledsoe. A Maximal Method for Set Variables in Automatic Theorem-proving.