/src/HOL/HOLCF/FOCUS/ default tip
drwxr-xr-x [up]
-rw-r--r-- 2025-07-23 13:22 +0200 13352 Buffer.thy
-rw-r--r-- 2025-07-23 13:22 +0200 10600 Buffer_adm.thy
-rw-r--r-- 2025-07-23 13:22 +0200 605 FOCUS.thy
-rw-r--r-- 2025-07-23 13:22 +0200 7897 Fstream.thy
-rw-r--r-- 2025-07-23 13:22 +0200 12045 Fstreams.thy
-rw-r--r-- 2025-07-23 13:22 +0200 7677 Stream_adm.thy