# HG changeset patch
# User haftmann
# Date 1278945648 -7200
# Node ID df0350f1e7f25b07d67921e481e3bb440a1c3eae
# Parent  7371534297a9c554e57424031888288c45234069
dropped empty theory

diff -r 7371534297a9 -r df0350f1e7f2 src/HOL/Imperative_HOL/Imperative_HOL.thy
--- a/src/HOL/Imperative_HOL/Imperative_HOL.thy	Mon Jul 12 16:38:20 2010 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL.thy	Mon Jul 12 16:40:48 2010 +0200
@@ -5,7 +5,7 @@
 header {* Entry point into monadic imperative HOL *}
 
 theory Imperative_HOL
-imports Array Ref Relational Mrec
+imports Array Ref Mrec
 begin
 
 end
diff -r 7371534297a9 -r df0350f1e7f2 src/HOL/Imperative_HOL/Relational.thy
--- a/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 12 16:38:20 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-theory Relational 
-imports Array Ref
-begin
-
-end
diff -r 7371534297a9 -r df0350f1e7f2 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jul 12 16:38:20 2010 +0200
+++ b/src/HOL/IsaMakefile	Mon Jul 12 16:40:48 2010 +0200
@@ -813,8 +813,7 @@
 $(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Array.thy	\
   Imperative_HOL/Heap.thy Imperative_HOL/Heap_Monad.thy			\
   Imperative_HOL/Imperative_HOL.thy Imperative_HOL/Imperative_HOL_ex.thy\
-  Imperative_HOL/Mrec.thy Imperative_HOL/Relational.thy			\
-  Imperative_HOL/Ref.thy						\
+  Imperative_HOL/Mrec.thy Imperative_HOL/Ref.thy			\
   Imperative_HOL/ex/Imperative_Quicksort.thy				\
   Imperative_HOL/ex/Imperative_Reverse.thy				\
   Imperative_HOL/ex/Linked_Lists.thy					\