# HG changeset patch
# User wenzelm
# Date 1315151419 -7200
# Node ID f2bfe19239bcc015e16ec98f99f5cceb075a02d2
# Parent  eb00752507c7be3085b391ccfe111e6cb6e55028
tuned document;

diff -r eb00752507c7 -r f2bfe19239bc src/HOL/Unix/Nested_Environment.thy
--- a/src/HOL/Unix/Nested_Environment.thy	Sun Sep 04 17:35:34 2011 +0200
+++ b/src/HOL/Unix/Nested_Environment.thy	Sun Sep 04 17:50:19 2011 +0200
@@ -9,7 +9,7 @@
 begin
 
 text {*
-  Consider a partial function @{term [source] "e :: 'a => 'b option"};
+  Consider a partial function @{term [source] "e :: 'a \<Rightarrow> 'b option"};
   this may be understood as an \emph{environment} mapping indexes
   @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
   @{text Map} of Isabelle/HOL).  This basic idea is easily generalized
@@ -21,7 +21,7 @@
 
 datatype ('a, 'b, 'c) env =
     Val 'a
-  | Env 'b  "'c => ('a, 'b, 'c) env option"
+  | Env 'b  "'c \<Rightarrow> ('a, 'b, 'c) env option"
 
 text {*
   \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
@@ -43,14 +43,14 @@
   @{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"
+primrec lookup :: "('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
+  and lookup_option :: "('a, 'b, 'c) env option \<Rightarrow> 'c list \<Rightarrow> ('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
-        [] => Some (Env b es)
-      | y # ys => lookup_option (es y) ys)"
+        [] \<Rightarrow> Some (Env b es)
+      | y # ys \<Rightarrow> lookup_option (es y) ys)"
   | "lookup_option None xs = None"
   | "lookup_option (Some e) xs = lookup e xs"
 
@@ -70,8 +70,8 @@
 theorem lookup_env_cons:
   "lookup (Env b es) (x # xs) =
     (case es x of
-      None => None
-    | Some e => lookup e xs)"
+      None \<Rightarrow> None
+    | Some e \<Rightarrow> lookup e xs)"
   by (cases "es x") simp_all
 
 lemmas lookup_lookup_option.simps [simp del]
@@ -80,14 +80,14 @@
 theorem lookup_eq:
   "lookup env xs =
     (case xs of
-      [] => Some env
-    | x # xs =>
+      [] \<Rightarrow> Some env
+    | x # xs \<Rightarrow>
       (case env of
-        Val a => None
-      | Env b es =>
+        Val a \<Rightarrow> None
+      | Env b es \<Rightarrow>
           (case es x of
-            None => None
-          | Some e => lookup e xs)))"
+            None \<Rightarrow> None
+          | Some e \<Rightarrow> lookup e xs)))"
   by (simp split: list.split env.split)
 
 text {*
@@ -245,18 +245,18 @@
   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"
+primrec update :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
+    ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"
+  and update_option :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
+    ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env option"
 where
   "update xs opt (Val a) =
-    (if xs = [] then (case opt of None => Val a | Some e => e)
+    (if xs = [] then (case opt of None \<Rightarrow> Val a | Some e \<Rightarrow> 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))))"
+      [] \<Rightarrow> (case opt of None \<Rightarrow> Env b es | Some e \<Rightarrow> e)
+    | y # ys \<Rightarrow> 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) =
@@ -286,8 +286,8 @@
   "update (x # y # ys) opt (Env b es) =
     Env b (es (x :=
       (case es x of
-        None => None
-      | Some e => Some (update (y # ys) opt e))))"
+        None \<Rightarrow> None
+      | Some e \<Rightarrow> Some (update (y # ys) opt e))))"
   by (cases "es x") simp_all
 
 lemmas update_update_option.simps [simp del]
@@ -297,21 +297,21 @@
 lemma update_eq:
   "update xs opt env =
     (case xs of
-      [] =>
+      [] \<Rightarrow>
         (case opt of
-          None => env
-        | Some e => e)
-    | x # xs =>
+          None \<Rightarrow> env
+        | Some e \<Rightarrow> e)
+    | x # xs \<Rightarrow>
         (case env of
-          Val a => Val a
-        | Env b es =>
+          Val a \<Rightarrow> Val a
+        | Env b es \<Rightarrow>
             (case xs of
-              [] => Env b (es (x := opt))
-            | y # ys =>
+              [] \<Rightarrow> Env b (es (x := opt))
+            | y # ys \<Rightarrow>
                 Env b (es (x :=
                   (case es x of
-                    None => None
-                  | Some e => Some (update (y # ys) opt e)))))))"
+                    None \<Rightarrow> None
+                  | Some e \<Rightarrow> Some (update (y # ys) opt e)))))))"
   by (simp split: list.split env.split option.split)
 
 text {*