src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
changeset 47108 2a1953f0d20d
parent 44890 22f665a2e91c
child 50630 1ea90e8046dc
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  theory Imperative_Quicksort
     1.6  imports
     1.7 -  Imperative_HOL
     1.8 +  "~~/src/HOL/Imperative_HOL/Imperative_HOL"
     1.9    Subarray
    1.10    "~~/src/HOL/Library/Multiset"
    1.11    "~~/src/HOL/Library/Efficient_Nat"
    1.12 @@ -593,8 +593,8 @@
    1.13  proof (induct a l r p arbitrary: h rule: part1.induct)
    1.14    case (1 a l r p)
    1.15    thus ?case unfolding part1.simps [of a l r]
    1.16 -  apply (auto intro!: success_intros del: success_ifI simp add: not_le)
    1.17 -  apply (auto intro!: effect_intros effect_swapI)
    1.18 +  apply (auto intro!: success_intros simp add: not_le)
    1.19 +  apply (auto intro!: effect_intros)
    1.20    done
    1.21  qed
    1.22