Mon, 20 Aug 2007 23:41:43 +0200 wenzelm standard_parse_term: added pp/check argument, include disambig here (from sign.ML);
Mon, 20 Aug 2007 23:41:40 +0200 wenzelm inner syntax: added parse_term/prop;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip