### [isabelle-dev] simplifier and subgoaler not transitive

Dear All, Assuming that this is about the bowels of the simplifier, I hope this is the right place to ask the following question. The simplifier has a subgoaler, which helps with rewriting conditional lemmas. This simplifiying/subgoaling process seems to be not transitive (probably is not

### Re: [isabelle-dev] simplifier and subgoaler not transitive

Am 22/05/2012 18:23, schrieb Christian Urban: Dear All, Assuming that this is about the bowels of the simplifier, I hope this is the right place to ask the following question. The simplifier has a subgoaler, which helps with rewriting conditional lemmas. This simplifiying/subgoaling

### Re: [isabelle-dev] simplifier and subgoaler not transitive

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 ♯

### Re: [isabelle-dev] simplifier and subgoaler not transitive

Question: it looks to me like (atom v # (x, y)) = (atom v # x atom v # y) It also looks like what you're trying to do is allow the system to reason with the above equality without actually giving it that equality. It looks like you've provided the equality in one direction as a rewrite rule

### [isabelle-dev] simplifier trace (and jedit)

Dear all, I wanted to write this already a long time ago (prompted by an Isabelle course I gave) but somehow forgot about it. Now I had a look at my slides again and was reminded. 1) The first thing is rather subjective, but maybe you could comment on it. I think the simplifier trace would

### Re: [isabelle-dev] simplifier trace (and jedit)

The _2 v.s. (2) thing is just silly. It's in find_theorems output too. It's just the way theorems get their names - probably one of these decisions made years ago and not compatible with Makarius' decisions about how to fetch theorems in Isar. Adding context information to every reduction