fixed proof;
authorwenzelm
Thu Mar 20 16:54:11 2008 +0100 (2008-03-20 ago)
changeset 26365e6d3714b8853
parent 26364 cb6f360ab425
child 26366 5c089f4219c2
fixed proof;
src/HOL/TLA/Memory/MemClerk.thy
     1.1 --- a/src/HOL/TLA/Memory/MemClerk.thy	Thu Mar 20 16:28:23 2008 +0100
     1.2 +++ b/src/HOL/TLA/Memory/MemClerk.thy	Thu Mar 20 16:54:11 2008 +0100
     1.3 @@ -87,9 +87,6 @@
     1.4    by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm MClkFwd_def},
     1.5      @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
     1.6      [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
     1.7 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
     1.8 -    thm "Call_def", thm "caller_def", thm "rtrner_def"]) [exI]
     1.9 -    [thm "base_enabled", Pair_inject] 1 *})
    1.10  
    1.11  lemma MClkFwd_ch_enabled: "|- Enabled (MClkFwd send rcv cst p)  -->   
    1.12           Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"