src/HOL/Lifting.thy
changeset 55604 42e4e8c2e8dc
parent 55563 a64d49f49ca3
child 55610 9066b603dff6
     1.1 --- a/src/HOL/Lifting.thy	Thu Feb 20 13:53:26 2014 +0100
     1.2 +++ b/src/HOL/Lifting.thy	Thu Feb 20 15:14:37 2014 +0100
     1.3 @@ -455,13 +455,13 @@
     1.4    assumes "left_unique T"
     1.5    assumes "R \<le> op="
     1.6    shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
     1.7 -using assms unfolding left_unique_def by fast
     1.8 +using assms unfolding left_unique_def by blast
     1.9  
    1.10  lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
    1.11  unfolding left_total_def OO_def by fast
    1.12  
    1.13  lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
    1.14 -unfolding left_unique_def OO_def by fast
    1.15 +unfolding left_unique_def OO_def by blast
    1.16  
    1.17  lemma invariant_le_eq:
    1.18    "invariant P \<le> op=" unfolding invariant_def by blast