src/HOL/TLA/Memory/MemClerk.ML
changeset 4089 96fba19bcbe2
parent 3807 82a99b090d9d
child 6255 db63752140c7
     1.1 --- a/src/HOL/TLA/Memory/MemClerk.ML	Mon Nov 03 12:12:10 1997 +0100
     1.2 +++ b/src/HOL/TLA/Memory/MemClerk.ML	Mon Nov 03 12:13:18 1997 +0100
     1.3 @@ -18,14 +18,14 @@
     1.4  
     1.5  qed_goal "MClkidle" MemClerk.thy
     1.6     ".~ $(Calling send p) .& ($(cst@p) .= #clkA) .-> .~ MClkNext send rcv cst p"
     1.7 -   (fn _ => [ auto_tac (!claset,
     1.8 -                        !simpset addsimps (MC_action_defs @ [Return_def]))
     1.9 +   (fn _ => [ auto_tac (claset(),
    1.10 +                        simpset() addsimps (MC_action_defs @ [Return_def]))
    1.11              ]);
    1.12  
    1.13  qed_goal "MClkbusy" MemClerk.thy
    1.14     "$(Calling rcv p) .-> .~ MClkNext send rcv cst p"
    1.15 -   (fn _ => [ auto_tac (!claset,
    1.16 -                        !simpset addsimps (MC_action_defs @ [Call_def]))
    1.17 +   (fn _ => [ auto_tac (claset(),
    1.18 +                        simpset() addsimps (MC_action_defs @ [Call_def]))
    1.19              ]);
    1.20  
    1.21  (* unlifted versions as introduction rules *)
    1.22 @@ -39,14 +39,14 @@
    1.23     "!!p. base_var <rtrner send @ p, caller rcv @ p, cst@p> ==> \
    1.24  \        $(Calling send p) .& .~ $(Calling rcv p) .& ($(cst@p) .= #clkA)  \
    1.25  \        .-> $(Enabled (MClkFwd send rcv cst p))"
    1.26 -   (fn _ => [action_simp_tac (!simpset addsimps [MClkFwd_def,Call_def,caller_def,rtrner_def])
    1.27 +   (fn _ => [action_simp_tac (simpset() addsimps [MClkFwd_def,Call_def,caller_def,rtrner_def])
    1.28                               [] [base_enabled,Pair_inject] 1]);
    1.29  
    1.30  qed_goal "MClkFwd_ch_enabled" MemClerk.thy
    1.31     "Enabled (MClkFwd send rcv cst p) s  \
    1.32  \   ==> Enabled (<MClkFwd send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>) s"
    1.33 -   (fn [prem] => [auto_tac (!claset addSIs [prem RS enabled_mono],
    1.34 -			    !simpset addsimps [angle_def,MClkFwd_def])
    1.35 +   (fn [prem] => [auto_tac (claset() addSIs [prem RS enabled_mono],
    1.36 +			    simpset() addsimps [angle_def,MClkFwd_def])
    1.37  		 ]);
    1.38  
    1.39  qed_goal "MClkReply_change" MemClerk.thy
    1.40 @@ -59,13 +59,13 @@
    1.41     "!!p. base_var <rtrner send @ p, caller rcv @ p, cst@p> ==> \
    1.42  \        $(Calling send p) .& .~ $(Calling rcv p) .& ($(cst@p) .= #clkB)  \
    1.43  \        .-> $(Enabled (<MClkReply send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>))"
    1.44 -   (fn _ => [action_simp_tac (!simpset) [MClkReply_change RSN (2,enabled_mono)] [] 1,
    1.45 -	     action_simp_tac (!simpset addsimps [MClkReply_def,Return_def,caller_def,rtrner_def])
    1.46 +   (fn _ => [action_simp_tac (simpset()) [MClkReply_change RSN (2,enabled_mono)] [] 1,
    1.47 +	     action_simp_tac (simpset() addsimps [MClkReply_def,Return_def,caller_def,rtrner_def])
    1.48                               [] [base_enabled,Pair_inject] 1
    1.49  	    ]);
    1.50  
    1.51  qed_goal "MClkReplyNotRetry" MemClerk.thy
    1.52     "MClkReply send rcv cst p .-> .~(MClkRetry send rcv cst p)"
    1.53 -   (fn _ => [ auto_tac (!claset,
    1.54 -			!simpset addsimps [MClkReply_def,MClkRetry_def]) 
    1.55 +   (fn _ => [ auto_tac (claset(),
    1.56 +			simpset() addsimps [MClkReply_def,MClkRetry_def]) 
    1.57  	    ]);