From 2119182166f73c5a03bea6c516741e7d819b6175 Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Mon, 30 Jan 2023 11:47:24 +1030
Subject: [PATCH] clib: move ccorresG abbreviation

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
---
 lib/clib/CCorresLemmas.thy | 3 ---
 lib/clib/Corres_UL_C.thy   | 3 +++
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy
index ee723426c..559c5e55c 100644
--- a/lib/clib/CCorresLemmas.thy
+++ b/lib/clib/CCorresLemmas.thy
@@ -345,9 +345,6 @@ lemma ccorres_expand_while_iff:
   apply (auto elim!: exec_Normal_elim_cases intro: exec.intros)
   done
 
-abbreviation
-  "ccorresG rf_sr \<Gamma> r xf \<equiv> ccorres_underlying rf_sr \<Gamma> r xf r xf"
-
 lemma exec_handlers_Hoare_call_Basic:
   "\<lbrakk> \<forall>s' t x. s' \<in> P \<longrightarrow> g s' t (ret s' t) \<in> Q; UNIV \<subseteq> A \<rbrakk> \<Longrightarrow>
     exec_handlers_Hoare \<Gamma> P (call initfn p ret (\<lambda>x y. Basic (g x y)) # hs) Q A"
diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy
index b3caa4333..486201dd1 100644
--- a/lib/clib/Corres_UL_C.thy
+++ b/lib/clib/Corres_UL_C.thy
@@ -86,6 +86,9 @@ where
                             \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'')
        | _ \<Rightarrow> False))"
 
+abbreviation
+  "ccorresG rf_sr \<Gamma> r xf \<equiv> ccorres_underlying rf_sr \<Gamma> r xf r xf"
+
 declare isNormal_simps [simp]
 
 lemma ccorresI [case_names fail nofail]: