/src/HOL/Tools/Old_Datatype/
drwxr-xr-x [up]
-rw-r--r-- 2017-09-26 15:29 -0300 34864 old_datatype.ML
-rw-r--r-- 2017-09-26 15:29 -0300 14255 old_datatype_aux.ML
-rw-r--r-- 2017-09-26 15:29 -0300 743 old_datatype_codegen.ML
-rw-r--r-- 2017-09-26 15:29 -0300 8681 old_datatype_data.ML
-rw-r--r-- 2017-09-26 15:29 -0300 15823 old_datatype_prop.ML
-rw-r--r-- 2017-09-26 15:29 -0300 12730 old_primrec.ML
-rw-r--r-- 2017-09-26 15:29 -0300 28707 old_rep_datatype.ML
-rw-r--r-- 2017-09-26 15:29 -0300 10116 old_size.ML