# HG changeset patch
# User wenzelm
# Date 1120250234 -7200
# Node ID 6eeed52043dd9e3cbf49b9b5130a8045fe0c79f3
# Parent  4748b1adad9cb9fdc991c490945be7cd939e1ab7
tuned;

diff -r 4748b1adad9c -r 6eeed52043dd src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Fri Jul 01 22:36:36 2005 +0200
+++ b/src/HOL/Unix/Unix.thy	Fri Jul 01 22:37:14 2005 +0200
@@ -614,14 +614,12 @@
 *}
 
 theorem transitions_type_safe:
-  "root =xs\<Rightarrow> root' \<Longrightarrow> \<exists>att dir. root = Env att dir
-    \<Longrightarrow> \<exists>att dir. root' = Env att dir"
-proof -
-  case rule_context
-  with transition_type_safe show ?thesis
-  proof (rule transitions_invariant)
-    show "\<forall>x \<in> set xs. True" by blast
-  qed
+  assumes "root =xs\<Rightarrow> root'"
+    and "\<exists>att dir. root = Env att dir"
+  shows "\<exists>att dir. root' = Env att dir"
+  using transition_type_safe and prems
+proof (rule transitions_invariant)
+  show "\<forall>x \<in> set xs. True" by blast
 qed