--- 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
--- 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
--- 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 \