# HG changeset patch
# User wenzelm
# Date 1316347797 -7200
# Node ID 9e17d632a9edfa658c35fcde5f1fb693278e25cd
# Parent  23dbab7f8cf4aabff5d8cd2ad3c106b89be40e8f
tuned proofs;

diff -r 23dbab7f8cf4 -r 9e17d632a9ed src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Sun Sep 18 13:56:06 2011 +0200
+++ b/src/HOL/Induct/Com.thy	Sun Sep 18 14:09:57 2011 +0200
@@ -85,12 +85,12 @@
 lemma [pred_set_conv]:
   "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
   unfolding subset_eq
-  by (auto simp add: le_fun_def le_bool_def)
+  by (auto simp add: le_fun_def)
 
 lemma [pred_set_conv]:
   "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
   unfolding subset_eq
-  by (auto simp add: le_fun_def le_bool_def)
+  by (auto simp add: le_fun_def)
 
 text{*Command execution is functional (deterministic) provided evaluation is*}
 theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
@@ -133,15 +133,14 @@
 
 
 lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))"
-by (rule fun_upd_same [THEN subst], fast)
+  by (rule fun_upd_same [THEN subst]) fast
 
 
 text{* Make the induction rule look nicer -- though @{text eta_contract} makes the new
     version look worse than it is...*}
 
-lemma split_lemma:
-     "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
-by auto
+lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
+  by auto
 
 text{*New induction rule.  Note the form of the VALOF induction hypothesis*}
 lemma eval_induct