changeset 39307 | 8d42d668b5b0 |
parent 38058 | e4640c2ceb43 |
child 50630 | 1ea90e8046dc |
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Mon Sep 13 14:54:02 2010 +0200 +++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Mon Sep 13 14:54:05 2010 +0200 @@ -6,7 +6,7 @@ header {* Monadic imperative HOL with examples *} theory Imperative_HOL_ex -imports Imperative_HOL +imports Imperative_HOL Overview "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker" begin