# HG changeset patch
# User bulwahn
# Date 1315823617 -7200
# Node ID 95a53c01ed61b9bd1404c164a4fd7307ef25a062
# Parent  ec3f30b8c78cfe1a7a29c3c6e2f161f37726440e
correcting imports after splitting and renaming AssocList

diff -r ec3f30b8c78c -r 95a53c01ed61 src/HOL/ex/Execute_Choice.thy
--- a/src/HOL/ex/Execute_Choice.thy	Mon Sep 12 10:59:38 2011 +0200
+++ b/src/HOL/ex/Execute_Choice.thy	Mon Sep 12 12:33:37 2011 +0200
@@ -3,7 +3,7 @@
 header {* A simple cookbook example how to eliminate choice in programs. *}
 
 theory Execute_Choice
-imports Main "~~/src/HOL/Library/AssocList"
+imports Main "~~/src/HOL/Library/AList_Mapping"
 begin
 
 text {*