# HG changeset patch
# User wenzelm
# Date 1002319132 -7200
# Node ID 6e5de8d4290a2b4ef96e50630dedcf9d00b237d8
# Parent  ebfe5ba905b04b49637ed6acf988fd3f2a0da09d
tuned;

diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Action.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -71,5 +71,3 @@
 
   enabled_def   "s |= Enabled A  ==  EX u. (s,u) |= A"
 end
-
-
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Inc/Inc.thy
--- a/src/HOL/TLA/Inc/Inc.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -9,7 +9,7 @@
     Lamport's "increment" example.
 *)
 
-Inc  =  TLA + Nat +
+Inc  =  TLA +
 
 (* program counter as an enumeration type *)
 datatype pcount = a | b | g
@@ -67,5 +67,3 @@
   PsiInv_def   "PsiInv   == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
   
 end
-
-ML
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Inc/Pcount.thy
--- a/src/HOL/TLA/Inc/Pcount.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Inc/Pcount.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -11,10 +11,8 @@
 and case distinction tactics.
 *)
 
-Pcount  =  Datatype +
+Pcount  =  Main +
 
 datatype pcount = a | b | g
 
 end
-
-ML
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Inc/ROOT.ML
--- a/src/HOL/TLA/Inc/ROOT.ML	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Inc/ROOT.ML	Fri Oct 05 23:58:52 2001 +0200
@@ -1,2 +1,3 @@
 
+time_use_thy "Pcount";
 time_use_thy "Inc";
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Init.thy
--- a/src/HOL/TLA/Init.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Init.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -42,5 +42,3 @@
   fw_stp_def  "first_world == st1"
   fw_act_def  "first_world == %sigma. (st1 sigma, st2 sigma)"
 end
-
-ML
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Memory/MIParameters.thy
--- a/src/HOL/TLA/Memory/MIParameters.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Memory/MIParameters.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -9,9 +9,8 @@
     RPC-Memory example: Parameters of the memory implementation.
 *)
 
-MIParameters = Datatype +
+MIParameters = Main +
 
 datatype  histState  =  histA | histB
 
 end
-
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Memory/MemClerk.thy
--- a/src/HOL/TLA/Memory/MemClerk.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Memory/MemClerk.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -65,5 +65,3 @@
       "MClkISpec send rcv cst == TEMP (ALL p. MClkIPSpec send rcv cst p)"
 
 end
-
-
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Memory/MemClerkParameters.thy
--- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -28,4 +28,3 @@
     "MClkReplyVal v == if v = RPCFailure then MemFailure else v"
 
 end
-
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Memory/Memory.thy
--- a/src/HOL/TLA/Memory/Memory.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Memory/Memory.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -133,6 +133,3 @@
 
   MemInv_def        "MemInv mm l == PRED  #l : #MemLoc --> mm!l : #MemVal"
 end
-
-
-
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -175,4 +175,3 @@
 			   (mm!l, rtrner rmCh!p, ires!p))"
 
 end
-
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Memory/ProcedureInterface.thy
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -83,5 +83,3 @@
   LegalReturner_def     "LegalReturner ch == TEMP (! p. PLegalReturner ch p)"
 
 end
-
-
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Memory/RPC.thy
--- a/src/HOL/TLA/Memory/RPC.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Memory/RPC.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -75,6 +75,3 @@
   RPCISpec_def      "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)"
 
 end
-
-
-
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Memory/RPCMemoryParams.thy
--- a/src/HOL/TLA/Memory/RPCMemoryParams.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -9,20 +9,16 @@
     Basic declarations for the RPC-memory example.
 *)
 
-RPCMemoryParams = HOL +
+theory RPCMemoryParams = Main:
 
 types
   bit = "bool"   (* Signal wires for the procedure interface.
                     Defined as bool for simplicity. All I should really need is
                     the existence of two distinct values. *)
-  Locs           (* "syntactic" value type *)
-  Vals           (* "syntactic" value type *)
-  PrIds          (* process id's *)
 
 (* all of these are simple (HOL) types *)
-arities
-  Locs   :: term
-  Vals   :: term
-  PrIds  :: term
+typedecl Locs    (* "syntactic" value type *)
+typedecl Vals    (* "syntactic" value type *)
+typedecl PrIds   (* process id's *)
 
 end
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Memory/RPCParameters.thy
--- a/src/HOL/TLA/Memory/RPCParameters.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Memory/RPCParameters.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -43,5 +43,3 @@
 		         case ra of (memcall m) => m
 		                  | (othercall v) => arbitrary"
 end
-
-
diff -r ebfe5ba905b0 -r 6e5de8d4290a src/HOL/TLA/Stfun.thy
--- a/src/HOL/TLA/Stfun.thy	Fri Oct 05 23:58:17 2001 +0200
+++ b/src/HOL/TLA/Stfun.thy	Fri Oct 05 23:58:52 2001 +0200
@@ -61,5 +61,3 @@
   unit_base "basevars (v::unit stfun)"
 
 end
-
-ML