# [isabelle] 2007->2008 conversion problems: Introduction rules for set membership

```And more problems with the new set definition:

I have a lemma that is as follows, for S:: "'a => 'b set"
```
lemma mp_antimonoD: "\<lbrakk>mp_antimono S; mc\<subseteq>mc'\<rbrakk> \<Longrightarrow> S mc \<supseteq> S mc'" by (unfold mp_antimono_def) blast
```

```
at some point in a scripted proof (where I definitely DO NOT want to start an Isar-proof), I have the subgoal "[| mp_antimono S; mc<=mc'; (qs, qsh, csh) : S mc'; ... |] ==> (qs,qsh,csh) : S mc"
```
I usually would say: by (blast intro: set_rev_mp[OF _ mp_antimonoD])
In Isabelle2007, this instantly terminates.
```
In Isabelle2008, this also terminates, but, depending on the other facts around, after several second of spitting some strange output to the trace buffer, many thousands of lines of
```
Enter MATCH

```
\<lambda>mc mc' a aa b qs qsh csh qs' cs' c d. d =?= \<lambda>mc mc' a aa b qs qsh csh qs' cs'. ?S146 mc mc' a aa b qs qsh csh qs' cs' (\<lambda>a. a)
```
(auto intro: set_rev_mp[OF _ mp_antimonoD]) gives manies of:
### Unification bound exceeded
and also needs very long to terminate.

```
What is going wrong there, and how can I get back my short proof scripts ? In the 2007-version, auto and blast were even able to use the facts derived from mp_antimonoD as input for other introduction rules, thus doing really many work with one auto-step.
```

Regards,
Peter

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.