tuned;
authorwenzelm
Fri Oct 05 23:58:52 2001 +0200 (2001-10-05)
changeset 117036e5de8d4290a
parent 11702 ebfe5ba905b0
child 11704 3c50a2cd6f00
tuned;
src/HOL/TLA/Action.thy
src/HOL/TLA/Inc/Inc.thy
src/HOL/TLA/Inc/Pcount.thy
src/HOL/TLA/Inc/ROOT.ML
src/HOL/TLA/Init.thy
src/HOL/TLA/Memory/MIParameters.thy
src/HOL/TLA/Memory/MemClerk.thy
src/HOL/TLA/Memory/MemClerkParameters.thy
src/HOL/TLA/Memory/Memory.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/Memory/ProcedureInterface.thy
src/HOL/TLA/Memory/RPC.thy
src/HOL/TLA/Memory/RPCMemoryParams.thy
src/HOL/TLA/Memory/RPCParameters.thy
src/HOL/TLA/Stfun.thy
     1.1 --- a/src/HOL/TLA/Action.thy	Fri Oct 05 23:58:17 2001 +0200
     1.2 +++ b/src/HOL/TLA/Action.thy	Fri Oct 05 23:58:52 2001 +0200
     1.3 @@ -71,5 +71,3 @@
     1.4  
     1.5    enabled_def   "s |= Enabled A  ==  EX u. (s,u) |= A"
     1.6  end
     1.7 -
     1.8 -
     2.1 --- a/src/HOL/TLA/Inc/Inc.thy	Fri Oct 05 23:58:17 2001 +0200
     2.2 +++ b/src/HOL/TLA/Inc/Inc.thy	Fri Oct 05 23:58:52 2001 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4      Lamport's "increment" example.
     2.5  *)
     2.6  
     2.7 -Inc  =  TLA + Nat +
     2.8 +Inc  =  TLA +
     2.9  
    2.10  (* program counter as an enumeration type *)
    2.11  datatype pcount = a | b | g
    2.12 @@ -67,5 +67,3 @@
    2.13    PsiInv_def   "PsiInv   == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
    2.14    
    2.15  end
    2.16 -
    2.17 -ML
     3.1 --- a/src/HOL/TLA/Inc/Pcount.thy	Fri Oct 05 23:58:17 2001 +0200
     3.2 +++ b/src/HOL/TLA/Inc/Pcount.thy	Fri Oct 05 23:58:52 2001 +0200
     3.3 @@ -11,10 +11,8 @@
     3.4  and case distinction tactics.
     3.5  *)
     3.6  
     3.7 -Pcount  =  Datatype +
     3.8 +Pcount  =  Main +
     3.9  
    3.10  datatype pcount = a | b | g
    3.11  
    3.12  end
    3.13 -
    3.14 -ML
     4.1 --- a/src/HOL/TLA/Inc/ROOT.ML	Fri Oct 05 23:58:17 2001 +0200
     4.2 +++ b/src/HOL/TLA/Inc/ROOT.ML	Fri Oct 05 23:58:52 2001 +0200
     4.3 @@ -1,2 +1,3 @@
     4.4  
     4.5 +time_use_thy "Pcount";
     4.6  time_use_thy "Inc";
     5.1 --- a/src/HOL/TLA/Init.thy	Fri Oct 05 23:58:17 2001 +0200
     5.2 +++ b/src/HOL/TLA/Init.thy	Fri Oct 05 23:58:52 2001 +0200
     5.3 @@ -42,5 +42,3 @@
     5.4    fw_stp_def  "first_world == st1"
     5.5    fw_act_def  "first_world == %sigma. (st1 sigma, st2 sigma)"
     5.6  end
     5.7 -
     5.8 -ML
     6.1 --- a/src/HOL/TLA/Memory/MIParameters.thy	Fri Oct 05 23:58:17 2001 +0200
     6.2 +++ b/src/HOL/TLA/Memory/MIParameters.thy	Fri Oct 05 23:58:52 2001 +0200
     6.3 @@ -9,9 +9,8 @@
     6.4      RPC-Memory example: Parameters of the memory implementation.
     6.5  *)
     6.6  
     6.7 -MIParameters = Datatype +
     6.8 +MIParameters = Main +
     6.9  
    6.10  datatype  histState  =  histA | histB
    6.11  
    6.12  end
    6.13 -
     7.1 --- a/src/HOL/TLA/Memory/MemClerk.thy	Fri Oct 05 23:58:17 2001 +0200
     7.2 +++ b/src/HOL/TLA/Memory/MemClerk.thy	Fri Oct 05 23:58:52 2001 +0200
     7.3 @@ -65,5 +65,3 @@
     7.4        "MClkISpec send rcv cst == TEMP (ALL p. MClkIPSpec send rcv cst p)"
     7.5  
     7.6  end
     7.7 -
     7.8 -
     8.1 --- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Fri Oct 05 23:58:17 2001 +0200
     8.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Fri Oct 05 23:58:52 2001 +0200
     8.3 @@ -28,4 +28,3 @@
     8.4      "MClkReplyVal v == if v = RPCFailure then MemFailure else v"
     8.5  
     8.6  end
     8.7 -
     9.1 --- a/src/HOL/TLA/Memory/Memory.thy	Fri Oct 05 23:58:17 2001 +0200
     9.2 +++ b/src/HOL/TLA/Memory/Memory.thy	Fri Oct 05 23:58:52 2001 +0200
     9.3 @@ -133,6 +133,3 @@
     9.4  
     9.5    MemInv_def        "MemInv mm l == PRED  #l : #MemLoc --> mm!l : #MemVal"
     9.6  end
     9.7 -
     9.8 -
     9.9 -
    10.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Oct 05 23:58:17 2001 +0200
    10.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Oct 05 23:58:52 2001 +0200
    10.3 @@ -175,4 +175,3 @@
    10.4  			   (mm!l, rtrner rmCh!p, ires!p))"
    10.5  
    10.6  end
    10.7 -
    11.1 --- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Oct 05 23:58:17 2001 +0200
    11.2 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Oct 05 23:58:52 2001 +0200
    11.3 @@ -83,5 +83,3 @@
    11.4    LegalReturner_def     "LegalReturner ch == TEMP (! p. PLegalReturner ch p)"
    11.5  
    11.6  end
    11.7 -
    11.8 -
    12.1 --- a/src/HOL/TLA/Memory/RPC.thy	Fri Oct 05 23:58:17 2001 +0200
    12.2 +++ b/src/HOL/TLA/Memory/RPC.thy	Fri Oct 05 23:58:52 2001 +0200
    12.3 @@ -75,6 +75,3 @@
    12.4    RPCISpec_def      "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)"
    12.5  
    12.6  end
    12.7 -
    12.8 -
    12.9 -
    13.1 --- a/src/HOL/TLA/Memory/RPCMemoryParams.thy	Fri Oct 05 23:58:17 2001 +0200
    13.2 +++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy	Fri Oct 05 23:58:52 2001 +0200
    13.3 @@ -9,20 +9,16 @@
    13.4      Basic declarations for the RPC-memory example.
    13.5  *)
    13.6  
    13.7 -RPCMemoryParams = HOL +
    13.8 +theory RPCMemoryParams = Main:
    13.9  
   13.10  types
   13.11    bit = "bool"   (* Signal wires for the procedure interface.
   13.12                      Defined as bool for simplicity. All I should really need is
   13.13                      the existence of two distinct values. *)
   13.14 -  Locs           (* "syntactic" value type *)
   13.15 -  Vals           (* "syntactic" value type *)
   13.16 -  PrIds          (* process id's *)
   13.17  
   13.18  (* all of these are simple (HOL) types *)
   13.19 -arities
   13.20 -  Locs   :: term
   13.21 -  Vals   :: term
   13.22 -  PrIds  :: term
   13.23 +typedecl Locs    (* "syntactic" value type *)
   13.24 +typedecl Vals    (* "syntactic" value type *)
   13.25 +typedecl PrIds   (* process id's *)
   13.26  
   13.27  end
    14.1 --- a/src/HOL/TLA/Memory/RPCParameters.thy	Fri Oct 05 23:58:17 2001 +0200
    14.2 +++ b/src/HOL/TLA/Memory/RPCParameters.thy	Fri Oct 05 23:58:52 2001 +0200
    14.3 @@ -43,5 +43,3 @@
    14.4  		         case ra of (memcall m) => m
    14.5  		                  | (othercall v) => arbitrary"
    14.6  end
    14.7 -
    14.8 -
    15.1 --- a/src/HOL/TLA/Stfun.thy	Fri Oct 05 23:58:17 2001 +0200
    15.2 +++ b/src/HOL/TLA/Stfun.thy	Fri Oct 05 23:58:52 2001 +0200
    15.3 @@ -61,5 +61,3 @@
    15.4    unit_base "basevars (v::unit stfun)"
    15.5  
    15.6  end
    15.7 -
    15.8 -ML