# [isabelle] No blast_trace anymore; assumption trace?

```Hi,

```
It was using "declare[[blast_trace=false]]" and "declare[[blast_stats=false]]" with Isabelle2013 that showed me that auto sometimes calls blast, but those traces cause an error now. Did anything replace them?
```
```
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 give here two proofs of the same statement:

(*1*)
```
theorem "(P ==> (Q ==> ((P ==> (Q ==> (!!(P::prop). PROP P))) ==> (!!(P::prop). PROP P))))"
```  by(assumption)
(*2*)
```
theorem "(P ==> (Q ==> ((P ==> (Q ==> (!!(P::prop). PROP P))) ==> (!!(P::prop). PROP P))))"
```  apply(simp del: True_implies_equals)
by(simp only: True_implies_equals)
(* lemma True_implies_equals: "(True ==> PROP P) == PROP P"  *)

```
The formula "(P ==> (Q ==> (!!(P::prop). PROP P))) ==> (!!(P::prop). PROP P)))" is a conjunction, and I'm having to work hard to try and prevent the automatic proof methods from proving things using too much HOL.
```
```
The proof for (*2*) is undesirable, but the proof for (*1*) seems okay because it doesn't look like it's resorting to any HOL other than some Trueprop coercion.
```
However, I don't know the details of what's happening, so I could be wrong.

What I'm guessing is something like this:

```
There's 3 assumptions: P, Q, and "(P ==> (Q ==> (!!(P::prop). PROP P)))". The assumption method starts by using P and Q to reduce the third assumption to "(!!(P::prop). PROP P))", which can then be used as an assumption for the final conclusion.
```
```
If I had a trace to tell me what the assumption method is doing, I might could stare at it a long time, and figure out what "assumption" is doing, and also do that with future problems.
```
Regards,
GB

```

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