Tue, 03 Aug 2010 18:10:18 +0200 wenzelm find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -1 +1 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip