Fri, 24 Jul 2009 12:00:02 +0200 wenzelm renamed Pure/tctical.ML to Pure/tactical.ML;
Fri, 24 Jul 2009 11:55:34 +0200 wenzelm eliminated print_goals_without_context -- proper pretty printing;
Fri, 24 Jul 2009 11:50:35 +0200 wenzelm Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip