# Re: [isabelle] No blast_trace anymore; assumption trace?

```On 10/9/2013 11:32 PM, Gottfried Barrow wrote:
```
I use that as an excuse to point out that these traces can help educate a man, and I ask here if there's some kind of trace that will give me some details about what the "assumption" method is doing.
```
```
I'll state the obvious again, but the more traces the better, though there's already a lot of tools to give feedback.
```
```
blast_trace looked like it was going to be useful to me. It's main use was that it was telling me when auto was resorting to something more than simplification, but I would try some to understand the details it was returning.
```
```
I've searched in NEWS and in isar-ref.pdf, but I didn't find anything about what would replace blast_trace.
```
```
Doing these simple exercises can help make obvious simple things that aren't obvious at first, and it's the feedback tools that help out. Talking to myself is fine when I have tools to eventually lead me to the answers.
```
```
In the proof of (*2*) that I gave, the simp trace was doing some substitution of "True", and that contributed to my impression that my false, "(!!(P::prop). PROP P)" was actually important. But then when I used "assumption", it eventually became clear that I was simply doing:
```
theorem "(P ==> (Q ==> ((P ==> (Q ==> R)) ==> R)))"

```
Modus ponens came to mind, and "Auto solve_direct", for the unexpanded formula, says "meta_impE" can be used, which is based on "meta_mp", but not quite the same, because of "meta_impE = meta_mp [elim_format]".
```
```
All that to say, one thing leads to another, and all the different routes can lead to a better understanding. I could assume I know what "assumption" is doing, but assuming I know the details when I don't, even with something simple, leads to being wrong a significant number of times.
```
```
I guess it's not a big deal, but the more access we have to the low-level details, to try and understand them and verify what we think is happening, the better. As I said, there's already a lot of feedback.
```
Regards,
GB

```

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