/ex/
drwxr-xr-x [up]
-rw-r--r-- 1996-01-19 12:27 +0100 3290 Finite.ML
-rw-r--r-- 1996-01-19 12:27 +0100 125 Finite.thy
-rw-r--r-- 1996-01-19 12:27 +0100 10824 PL.ML
-rw-r--r-- 1996-01-19 12:27 +0100 1482 PL.thy
-rw-r--r-- 1996-01-19 12:27 +0100 285 PL0.ML
-rw-r--r-- 1996-01-19 12:27 +0100 248 PL0.thy
-rw-r--r-- 1996-01-19 12:27 +0100 3290 finite.ML
-rw-r--r-- 1996-01-19 12:27 +0100 125 finite.thy
-rw-r--r-- 1996-01-19 12:27 +0100 1533 insort.ML
-rw-r--r-- 1996-01-19 12:27 +0100 470 insort.thy
-rw-r--r-- 1996-01-19 12:27 +0100 760 lexprod.ML
-rw-r--r-- 1996-01-19 12:27 +0100 387 lexprod.thy
-rw-r--r-- 1996-01-19 12:27 +0100 13532 meson-test.ML
-rw-r--r-- 1996-01-19 12:27 +0100 27077 mt.ML
-rw-r--r-- 1996-01-19 12:27 +0100 7902 mt.thy
-rw-r--r-- 1996-01-19 12:27 +0100 869 natsum.ML
-rw-r--r-- 1996-01-19 12:27 +0100 331 natsum.thy
-rw-r--r-- 1996-01-19 12:27 +0100 273 natsum.thy~
-rw-r--r-- 1996-01-19 12:27 +0100 11215 pl.ML
-rw-r--r-- 1996-01-19 12:27 +0100 1386 pl.thy
-rw-r--r-- 1996-01-19 12:27 +0100 285 pl0.ML
-rw-r--r-- 1996-01-19 12:27 +0100 318 pl0.thy
-rw-r--r-- 1996-01-19 12:27 +0100 1843 puzzle.ML
-rw-r--r-- 1996-01-19 12:27 +0100 241 puzzle.thy
-rw-r--r-- 1996-01-19 12:27 +0100 2711 qsort.ML
-rw-r--r-- 1996-01-19 12:27 +0100 583 qsort.thy
-rw-r--r-- 1996-01-19 12:27 +0100 127 rec.ML
-rw-r--r-- 1996-01-19 12:27 +0100 258 rec.thy
-rw-r--r-- 1996-01-19 12:27 +0100 10814 simult.ML
-rw-r--r-- 1996-01-19 12:27 +0100 3170 simult.thy
-rw-r--r-- 1996-01-19 12:27 +0100 837 sorting.ML
-rw-r--r-- 1996-01-19 12:27 +0100 823 sorting.thy
-rw-r--r-- 1996-01-19 12:27 +0100 6084 term.ML
-rw-r--r-- 1996-01-19 12:27 +0100 1625 term.thy