Sun, 10 Dec 2006 20:09:08 +0100 wenzelm fixed term_of_list;
Sun, 10 Dec 2006 19:37:30 +0100 wenzelm Concrete syntax for hex chars and strings.
Sun, 10 Dec 2006 19:37:29 +0100 wenzelm renamed str_of_XXX to print_XXX;
Sun, 10 Dec 2006 19:37:28 +0100 wenzelm HOLogic cleanup;
Sun, 10 Dec 2006 19:37:27 +0100 wenzelm ML_Syntax.print_XXX;
Sun, 10 Dec 2006 19:37:26 +0100 wenzelm misc cleanup -- removed non-HOL operations;
Sun, 10 Dec 2006 19:37:25 +0100 wenzelm moved char/string syntax to Tools/string_syntax.ML;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip