--- a/src/HOL/IsaMakefile Wed Apr 16 17:40:43 2008 +0200
+++ b/src/HOL/IsaMakefile Wed Apr 16 17:40:59 2008 +0200
@@ -778,7 +778,7 @@
TLA-Memory: TLA $(LOG)/TLA-Memory.gz
-$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MIParameters.thy \
+$(LOG)/TLA-Memory.gz: $(OUT)/TLA \
TLA/Memory/MemClerk.thy TLA/Memory/MemClerkParameters.thy \
TLA/Memory/Memory.thy TLA/Memory/MemoryImplementation.thy \
TLA/Memory/MemoryParameters.thy TLA/Memory/ProcedureInterface.thy \
--- a/src/HOL/TLA/Memory/MIParameters.thy Wed Apr 16 17:40:43 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*
- File: MIParameters.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1997 University of Munich
-
- Theory Name: MIParameters
- Logic Image: TLA
-
- RPC-Memory example: Parameters of the memory implementation.
-*)
-
-MIParameters = Main +
-
-datatype histState = histA | histB
-
-end