src/HOL/TLA/Memory/MemClerkParameters.ML
changeset 3807 82a99b090d9d
child 6255 db63752140c7
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TLA/Memory/MemClerkParameters.ML	Wed Oct 08 11:50:33 1997 +0200
@@ -0,0 +1,11 @@
+(* 
+    File:        MemClerkParameters.ML
+    Author:      Stephan Merz
+    Copyright:   1997 University of Munich
+
+    RPC-Memory example: Memory clerk parameters (ML file)
+*)
+
+val CP_simps = RP_simps @ mClkState.simps;
+
+