From 36588c4359784c269b4c2859d68d5544d835afa2 Mon Sep 17 00:00:00 2001
From: Andrew Boyton <andrew.boyton@nicta.com.au>
Date: Tue, 22 Jul 2014 14:36:53 +1000
Subject: [PATCH] Minor cleanup of proofs in the Take/Grant security model.

---
 spec/take-grant/System_S.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/spec/take-grant/System_S.thy b/spec/take-grant/System_S.thy
index d43c6260d..d954e3e12 100644
--- a/spec/take-grant/System_S.thy
+++ b/spec/take-grant/System_S.thy
@@ -214,7 +214,7 @@ definition
 lemma takeOperation_def2:
   "takeOperation e c\<^sub>1 c\<^sub>2 R s \<equiv>
   s (e \<mapsto> Entity ({diminish R c\<^sub>2} \<union> direct_caps_of s e))"
-  by (rule eq_reflection, simp add: takeOperation_def caps_of_def)
+  by (clarsimp simp: takeOperation_def caps_of_def)
 
 definition
   grantOperation ::
@@ -225,7 +225,7 @@ definition
 lemma grantOperation_def2:
   "grantOperation e c\<^sub>1 c\<^sub>2 R s \<equiv>
   s (target c\<^sub>1 \<mapsto> Entity ( {diminish R c\<^sub>2} \<union> direct_caps_of s (target c\<^sub>1)))"
-  by (rule eq_reflection, simp add: grantOperation_def caps_of_def)
+  by (clarsimp simp: grantOperation_def caps_of_def)
 
 definition
   copyOperation ::