--- 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