1.1 --- a/src/HOL/Unix/Unix.thy	Tue Aug 30 17:02:06 2011 +0200
     1.2 +++ b/src/HOL/Unix/Unix.thy	Tue Aug 30 17:36:12 2011 +0200
     1.3 @@ -302,8 +302,7 @@
     1.4    to all kinds of system-calls.
     1.5  *}
     1.6  
     1.7 -primrec
     1.8 -  uid_of :: "operation \<Rightarrow> uid"
     1.9 +primrec uid_of :: "operation \<Rightarrow> uid"
    1.10  where
    1.11      "uid_of (Read uid text path) = uid"
    1.12    | "uid_of (Write uid text path) = uid"
    1.13 @@ -314,8 +313,7 @@
    1.14    | "uid_of (Rmdir uid path) = uid"
    1.15    | "uid_of (Readdir uid names path) = uid"
    1.16  
    1.17 -primrec
    1.18 -  path_of :: "operation \<Rightarrow> path"
    1.19 +primrec path_of :: "operation \<Rightarrow> path"
    1.20  where
    1.21      "path_of (Read uid text path) = path"
    1.22    | "path_of (Write uid text path) = path"
    1.23 @@ -349,11 +347,9 @@
    1.24    involved here).
    1.25  *}
    1.26  
    1.27 -inductive
    1.28 -  transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
    1.29 -    ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
    1.30 +inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
    1.31 +  ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
    1.32  where
    1.33 -
    1.34    read:
    1.35      "access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow>
    1.36        root \<midarrow>(Read uid text path)\<rightarrow> root" |
    1.37 @@ -500,9 +496,8 @@
    1.38    amount of time.
    1.39  *}
    1.40  
    1.41 -inductive
    1.42 -  transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
    1.43 -    ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
    1.44 +inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
    1.45 +  ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
    1.46  where
    1.47      nil: "root =[]\<Rightarrow> root"
    1.48    | cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''"
    1.49 @@ -630,8 +625,7 @@
    1.50    transition.
    1.51  *}
    1.52  
    1.53 -definition
    1.54 -  "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')"
    1.55 +definition "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')"
    1.56  
    1.57  lemma can_exec_nil: "can_exec root []"
    1.58    unfolding can_exec_def by (blast intro: transitions.intros)