# HG changeset patch
# User wenzelm
# Date 876158009 -7200
# Node ID 1ecbaca6560a36d3de6ce758251abcd27523247d
# Parent  c5db2c87a646351cfe12127a8286c3258b05b59b
TODO: handle internal / external names;

diff -r c5db2c87a646 -r 1ecbaca6560a src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Mon Oct 06 19:11:56 1997 +0200
+++ b/src/HOL/datatype.ML	Mon Oct 06 19:13:29 1997 +0200
@@ -3,6 +3,9 @@
    Author:      Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker,
                 Konrad Slind
    Copyright 1995 TU Muenchen
+
+TODO:
+  - handle internal / external names
 *)
 
 (** Information about datatypes **)