Sun, 18 Apr 2010 18:01:22 +0200 Christian Urban tuned
Sun, 18 Apr 2010 17:58:45 +0200 Christian Urban moved some general function into nominal_library.ML
Sun, 18 Apr 2010 17:57:27 +0200 Christian Urban tuned; transformation functions now take a context, a thm and return a thm
(0) -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 tip