Tue, 11 Mar 1997 14:21:10 +0100 wenzelm tr is (again) type abbrev;
Tue, 11 Mar 1997 13:05:40 +0100 wenzelm added THIS_IS_ISABELLE_BUILD;
Tue, 11 Mar 1997 13:05:11 +0100 wenzelm added THIS_IS_ISABELLE_BUILD discrimination;
(0) -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip