src/HOL/TLA/Memory/MIParameters.thy
changeset 3807 82a99b090d9d
child 5184 9b8547a9496a
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TLA/Memory/MIParameters.thy	Wed Oct 08 11:50:33 1997 +0200
@@ -0,0 +1,17 @@
+(*
+    File:        MIParameters.thy
+    Author:      Stephan Merz
+    Copyright:   1997 University of Munich
+
+    Theory Name: MIParameters
+    Logic Image: TLA
+
+    RPC-Memory example: Parameters of the memory implementation.
+*)
+
+MIParameters = Arith +
+
+datatype  histState  =  histA | histB
+
+end
+