# HG changeset patch
# User wenzelm
# Date 1314718572 -7200
# Node ID 04f64e602fa66dc1eddfc721986e6d79639b16f1
# Parent  426834f253c80ec30fc031bf027a7eb7a676eec1
tuned document;

diff -r 426834f253c8 -r 04f64e602fa6 src/HOL/Unix/Nested_Environment.thy
--- a/src/HOL/Unix/Nested_Environment.thy	Tue Aug 30 17:02:06 2011 +0200
+++ b/src/HOL/Unix/Nested_Environment.thy	Tue Aug 30 17:36:12 2011 +0200
@@ -43,9 +43,9 @@
   @{term None}.
 *}
 
-primrec
-  lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
-  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" where
+primrec lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
+  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
+where
     "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
   | "lookup (Env b es) xs =
       (case xs of
@@ -245,22 +245,22 @@
   environment is left unchanged.
 *}
 
-primrec
-  update :: "'c list => ('a, 'b, 'c) env option
-    => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
-  and update_option :: "'c list => ('a, 'b, 'c) env option
-    => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" where
-    "update xs opt (Val a) =
-      (if xs = [] then (case opt of None => Val a | Some e => e)
-      else Val a)"
-  | "update xs opt (Env b es) =
-      (case xs of
-        [] => (case opt of None => Env b es | Some e => e)
-      | y # ys => Env b (es (y := update_option ys opt (es y))))"
-  | "update_option xs opt None =
-      (if xs = [] then opt else None)"
-  | "update_option xs opt (Some e) =
-      (if xs = [] then opt else Some (update xs opt e))"
+primrec update :: "'c list => ('a, 'b, 'c) env option =>
+    ('a, 'b, 'c) env => ('a, 'b, 'c) env"
+  and update_option :: "'c list => ('a, 'b, 'c) env option =>
+    ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
+where
+  "update xs opt (Val a) =
+    (if xs = [] then (case opt of None => Val a | Some e => e)
+     else Val a)"
+| "update xs opt (Env b es) =
+    (case xs of
+      [] => (case opt of None => Env b es | Some e => e)
+    | y # ys => Env b (es (y := update_option ys opt (es y))))"
+| "update_option xs opt None =
+    (if xs = [] then opt else None)"
+| "update_option xs opt (Some e) =
+    (if xs = [] then opt else Some (update xs opt e))"
 
 hide_const update_option
 
diff -r 426834f253c8 -r 04f64e602fa6 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Tue Aug 30 17:02:06 2011 +0200
+++ b/src/HOL/Unix/Unix.thy	Tue Aug 30 17:36:12 2011 +0200
@@ -302,8 +302,7 @@
   to all kinds of system-calls.
 *}
 
-primrec
-  uid_of :: "operation \<Rightarrow> uid"
+primrec uid_of :: "operation \<Rightarrow> uid"
 where
     "uid_of (Read uid text path) = uid"
   | "uid_of (Write uid text path) = uid"
@@ -314,8 +313,7 @@
   | "uid_of (Rmdir uid path) = uid"
   | "uid_of (Readdir uid names path) = uid"
 
-primrec
-  path_of :: "operation \<Rightarrow> path"
+primrec path_of :: "operation \<Rightarrow> path"
 where
     "path_of (Read uid text path) = path"
   | "path_of (Write uid text path) = path"
@@ -349,11 +347,9 @@
   involved here).
 *}
 
-inductive
-  transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
-    ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
+inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
+  ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
 where
-
   read:
     "access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow>
       root \<midarrow>(Read uid text path)\<rightarrow> root" |
@@ -500,9 +496,8 @@
   amount of time.
 *}
 
-inductive
-  transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
-    ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
+inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
+  ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
 where
     nil: "root =[]\<Rightarrow> root"
   | cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''"
@@ -630,8 +625,7 @@
   transition.
 *}
 
-definition
-  "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')"
+definition "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')"
 
 lemma can_exec_nil: "can_exec root []"
   unfolding can_exec_def by (blast intro: transitions.intros)