# HG changeset patch
# User wenzelm
# Date 1208360459 -7200
# Node ID 6a91e368590da3b9d4d2a56cdb86ab1f2458a83d
# Parent  fda7b0aff79835da25f4c78f52ade9156a59c4a4
removed unused TLA/Memory/MIParameters.thy;

diff -r fda7b0aff798 -r 6a91e368590d src/HOL/IsaMakefile
--- 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 \
diff -r fda7b0aff798 -r 6a91e368590d src/HOL/TLA/Memory/MIParameters.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