Thu, 11 Aug 2011 12:24:10 +0200 | wenzelm | some trimming; | changeset | files |
Thu, 11 Aug 2011 12:11:50 +0200 | wenzelm | prefix of Pure/ROOT.ML required for concurrency within the ML runtime; | changeset | files |
Thu, 11 Aug 2011 11:40:25 +0200 | wenzelm | redundant use of misc_legacy.ML; | changeset | files |
Thu, 11 Aug 2011 10:36:34 +0200 | krauss | eliminated use of recdef | changeset | files |
Thu, 11 Aug 2011 09:41:21 +0200 | krauss | removed obsolete recdef-related examples | changeset | files |
Thu, 11 Aug 2011 09:15:45 +0200 | krauss | removed unused material, which does not really belong here | changeset | files |