changeset 61119 | 7beed856816c |
parent 58889 | 5b7a9633cfa8 |
child 63167 | 0909deb8059b |
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Sun Sep 06 13:37:18 2015 +0200 +++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Sun Sep 06 14:51:49 2015 +0200 @@ -8,7 +8,6 @@ theory Imperative_HOL_ex imports Imperative_HOL Overview "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker" - Legacy_Mrec begin definition "everything = (Array.new, Array.of_list, Array.make, Array.len, Array.nth,