# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 10bd5ba8c9e6abc8eb5f73b3fdacd9c36eb75e32
# Parent  c96e511bfb7901d9e6fc5957126fe3e355009393
ported Unix to new datatypes

diff -r c96e511bfb79 -r 10bd5ba8c9e6 src/HOL/Unix/Nested_Environment.thy
--- a/src/HOL/Unix/Nested_Environment.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Unix/Nested_Environment.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -19,7 +19,7 @@
   position within the structure.
 *}
 
-datatype_new ('a, 'b, 'c) env =
+datatype_new (dead 'a, dead 'b, dead 'c) env =
     Val 'a
   | Env 'b  "'c \<Rightarrow> ('a, 'b, 'c) env option"
 
@@ -74,7 +74,7 @@
     | Some e \<Rightarrow> lookup e xs)"
   by (cases "es x") simp_all
 
-lemmas lookup_lookup_option.simps [simp del]
+lemmas lookup.simps [simp del] lookup_option.simps [simp del]
   and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons
 
 theorem lookup_eq:
@@ -290,7 +290,7 @@
       | Some e \<Rightarrow> Some (update (y # ys) opt e))))"
   by (cases "es x") simp_all
 
-lemmas update_update_option.simps [simp del]
+lemmas update.simps [simp del] update_option.simps [simp del]
   and update_simps [simp] = update_nil_none update_nil_some
     update_cons_val update_cons_nil_env update_cons_cons_env