# Re: [isabelle] blast works incretable slow at tty mode

Li, Chanjuan wrote:
> hi,all:
> I use isabelle in tty mode instead of emacs for my gentoo machine
> update the emacs to 23, isabelle can not work well with emacs 23.
> today I duplicate a simple example of tutorial of isabelle as follows:
> $ isabelle tty -l HOL
>
>> lemma "(x,y) : (-r)^* ==> (y,x) : r^*";
Your problem is that this is not a theorem. You mistyped it: instead of
-r it should be r^-1.
If you were using Isabelle2009-1 via emacs I would recommend to switch
on Auto Nitpick (under Isabelle > Settings). It would have found a
counterexample right away, automatically.
Tobias
> proof (prove): step 0
>
> goal (1 subgoal):
> 1. (x, y) : (- r)^* ==> (y, x) : r^*
>
>> apply(erule rtrancl_induct);
>
> proof (prove): step 1
>
> goal (2 subgoals):
> 1. (x, x) : r^*
> 2. !!y z.
> [| (x, y) : (- r)^*; (y, z) : - r; (y, x) : r^* |] ==> (z, x) :
> r^*
>
>> apply(rule rtrancl_refl);
> proof (prove): step 2
>
> goal (1 subgoal):
> 1. !!y z.
> [| (x, y) : (- r)^*; (y, z) : - r; (y, x) : r^* |] ==> (z, x) :
> r^*
>> apply(blast intro: rtrancl_trans);
> Search depth = 0
> Search depth = 1
> Search depth = 2
> Search depth = 3
> Search depth = 4
> Search depth = 5
>
> it seems the proof procedure stalled. I wait for about 20 minutes, there
> is nothing happened. I use isabelle2009 and polyml-5.2.1.
> Is anyone know the reason blast stalled? thanks for helping me.
>
>
> lily
>
>
>
>

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