src/HOL/Induct/Com.thy
changeset 44174 d1d79f0e1ea6
parent 41818 6d4c3ee8219d
child 44965 9e17d632a9ed
     1.1 --- a/src/HOL/Induct/Com.thy	Fri Aug 12 09:17:30 2011 -0700
     1.2 +++ b/src/HOL/Induct/Com.thy	Fri Aug 12 14:45:50 2011 -0700
     1.3 @@ -84,11 +84,13 @@
     1.4  
     1.5  lemma [pred_set_conv]:
     1.6    "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
     1.7 -  by (auto simp add: le_fun_def le_bool_def mem_def)
     1.8 +  unfolding subset_eq
     1.9 +  by (auto simp add: le_fun_def le_bool_def)
    1.10  
    1.11  lemma [pred_set_conv]:
    1.12    "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
    1.13 -  by (auto simp add: le_fun_def le_bool_def mem_def)
    1.14 +  unfolding subset_eq
    1.15 +  by (auto simp add: le_fun_def le_bool_def)
    1.16  
    1.17  text{*Command execution is functional (deterministic) provided evaluation is*}
    1.18  theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"