src/HOL/Unix/Unix.thy
changeset 41413 64cd30d6b0b8
parent 39224 39e0d3b86112
child 41579 4031fb078acc
equal deleted inserted replaced
41412:35f30e07fe0d 41413:64cd30d6b0b8
     3 *)
     3 *)
     4 
     4 
     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 Main Nested_Environment List_Prefix
     8 imports
       
     9   Main
       
    10   "~~/src/HOL/Library/Nested_Environment"
       
    11   "~~/src/HOL/Library/List_Prefix"
     9 begin
    12 begin
    10 
    13 
    11 text {*
    14 text {*
    12   We give a simple mathematical model of the basic structures
    15   We give a simple mathematical model of the basic structures
    13   underlying the Unix file-system, together with a few fundamental
    16   underlying the Unix file-system, together with a few fundamental