[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.