# HG changeset patch
# User wenzelm
# Date 1206028451 -3600
# Node ID e6d3714b8853cfac5ba2b8d6eb01892b48ed2b7d
# Parent  cb6f360ab425ce538479d4c4b6fd5d0a2dac1848
fixed proof;

diff -r cb6f360ab425 -r e6d3714b8853 src/HOL/TLA/Memory/MemClerk.thy
--- a/src/HOL/TLA/Memory/MemClerk.thy	Thu Mar 20 16:28:23 2008 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy	Thu Mar 20 16:54:11 2008 +0100
@@ -87,9 +87,6 @@
   by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm MClkFwd_def},
     @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
     [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
-  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
-    thm "Call_def", thm "caller_def", thm "rtrner_def"]) [exI]
-    [thm "base_enabled", Pair_inject] 1 *})
 
 lemma MClkFwd_ch_enabled: "|- Enabled (MClkFwd send rcv cst p)  -->   
          Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"