src/HOL/Unix/Unix.thy
changeset 16417 9bc16273c2d4
parent 15213 4aa219600e5e
child 16670 6eeed52043dd
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     3     Author:     Markus Wenzel, TU Muenchen
     3     Author:     Markus Wenzel, TU Muenchen
     4 *)
     4 *)
     5 
     5 
     6 header {* Unix file-systems \label{sec:unix-file-system} *}
     6 header {* Unix file-systems \label{sec:unix-file-system} *}
     7 
     7 
     8 theory Unix = Nested_Environment + List_Prefix:
     8 theory Unix imports Nested_Environment List_Prefix begin
     9 
     9 
    10 text {*
    10 text {*
    11   We give a simple mathematical model of the basic structures
    11   We give a simple mathematical model of the basic structures
    12   underlying the Unix file-system, together with a few fundamental
    12   underlying the Unix file-system, together with a few fundamental
    13   operations that could be imagined to be performed internally by the
    13   operations that could be imagined to be performed internally by the