Mon, 15 Jul 2002 10:41:34 +0200 fix latex output
schirmer [Mon, 15 Jul 2002 10:41:34 +0200] rev 13358
fix latex output
Sun, 14 Jul 2002 19:59:55 +0200 Removal of mono.thy
paulson [Sun, 14 Jul 2002 19:59:55 +0200] rev 13357
Removal of mono.thy
Sun, 14 Jul 2002 15:14:43 +0200 improved presentation markup
paulson [Sun, 14 Jul 2002 15:14:43 +0200] rev 13356
improved presentation markup
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip