equal
deleted
inserted
replaced
6 |
6 |
7 theory Imperative_Quicksort |
7 theory Imperative_Quicksort |
8 imports |
8 imports |
9 "~~/src/HOL/Imperative_HOL/Imperative_HOL" |
9 "~~/src/HOL/Imperative_HOL/Imperative_HOL" |
10 Subarray |
10 Subarray |
11 "~~/src/HOL/Library/Multiset" |
11 "HOL-Library.Multiset" |
12 "~~/src/HOL/Library/Code_Target_Numeral" |
12 "HOL-Library.Code_Target_Numeral" |
13 begin |
13 begin |
14 |
14 |
15 text \<open>We prove QuickSort correct in the Relational Calculus.\<close> |
15 text \<open>We prove QuickSort correct in the Relational Calculus.\<close> |
16 |
16 |
17 definition swap :: "'a::heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" |
17 definition swap :: "'a::heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" |