On Tuesday, May 22, 2012 at 20:59:28 (+0200), Tobias Nipkow wrote: > > but am at least as confused as you are: > > > [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM: > > atom v ♯ (x1, x2) ⟹ atom v ♯ x1 > > [1]Applying instance of rewrite rule "??.unknown": > > ?a1 ♯ ?x1.1 ⟹ ?a1 ♯ ?x2.1 ⟹ ?a1 ♯ (?x1.1, ?x2.1) ≡ True > > Where does this rewrite rule come from? Its name suggests it was created > during > the simp process, but there is no indication of that. > > > [1]Trying to rewrite: > > atom v ♯ x1 ⟹ atom v ♯ t ⟹ atom v ♯ (x1, x2) ≡ True > > This should be an instance of the above rule, but it is not, there is a > funny t. > I have no idea where that comes from. I'm confused.
Sorry, this was because of my postediting of the trace. It should be a x2. Not sure whether this improves things. Christian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev