# [isabelle] blast works incretable slow at tty mode

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^*";
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.*