/src/Doc/Tutorial/ToyList/ default tip
drwxr-xr-x [up]
-rw-r--r-- 2024-04-17 23:22 +0200 14047 ToyList.thy
-rw-r--r-- 2024-04-17 23:22 +0200 525 ToyList1.txt
-rw-r--r-- 2024-04-17 23:22 +0200 358 ToyList2.txt
-rw-r--r-- 2024-04-17 23:22 +0200 281 ToyList_Test.thy