Wed, 02 Apr 1997 17:28:27 +0200 wenzelm changed signature of dummy goal from proto_pure to pure;
Wed, 02 Apr 1997 15:39:44 +0200 paulson Converted to call blast_tac.
Wed, 02 Apr 1997 15:37:35 +0200 paulson Uses ZF.thy again, to make that theory usable
(0) -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip