src/HOL/Unix/Unix.thy
changeset 49077 154f25a162e3
parent 47215 ca516aa5b6ce
child 49086 835fd053d17d
equal deleted inserted replaced
49073:88fe93ae61cf 49077:154f25a162e3
     5 header {* Unix file-systems \label{sec:unix-file-system} *}
     5 header {* Unix file-systems \label{sec:unix-file-system} *}
     6 
     6 
     7 theory Unix
     7 theory Unix
     8 imports
     8 imports
     9   Nested_Environment
     9   Nested_Environment
    10   "~~/src/HOL/Library/List_Prefix"
    10   "~~/src/HOL/Library/Sublist"
    11 begin
    11 begin
    12 
    12 
    13 text {*
    13 text {*
    14   We give a simple mathematical model of the basic structures
    14   We give a simple mathematical model of the basic structures
    15   underlying the Unix file-system, together with a few fundamental
    15   underlying the Unix file-system, together with a few fundamental