# HG changeset patch
# User haftmann
# Date 1174913584 -7200
# Node ID 8c000a2ea2f28fba6df2c434b8483fbe65108252
# Parent  ebe95b0242b36d97da5d6373fc36018faecb3b9f
Eval theory

diff -r ebe95b0242b3 -r 8c000a2ea2f2 src/HOL/ex/ExecutableContent.thy
--- a/src/HOL/ex/ExecutableContent.thy	Mon Mar 26 14:53:03 2007 +0200
+++ b/src/HOL/ex/ExecutableContent.thy	Mon Mar 26 14:53:04 2007 +0200
@@ -7,6 +7,7 @@
 theory ExecutableContent
 imports
   Main
+  Eval
   "~~/src/HOL/ex/Records"
   AssocList
   Binomial
@@ -23,7 +24,6 @@
   State_Monad
   While_Combinator
   Word
-  "~~/src/HOL/ex/CodeEval"
 begin
 
 definition