remove find_theorems squash

Signed-off-by: Michael McInerney <[email protected]>
seL4 · May 8, 2024 · ad270c3 · ad270c3
1 parent 6133838
commit ad270c3
Show file tree

Hide file tree

Showing 5 changed files with 0 additions and 5 deletions.
diff --git a/proof/crefine/AARCH64/Finalise_C.thy b/proof/crefine/AARCH64/Finalise_C.thy
@@ -316,7 +316,6 @@ lemma cancel_all_ccorres_helper:
         Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread\<rbrace>
          (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (Ptr &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']) :: tcb_C ptr ptr))
        OD)"
-find_theorems ccorres_underlying name: cross
   unfolding whileAnno_def
 proof (induct ts)
   case Nil

diff --git a/proof/crefine/ARM/Finalise_C.thy b/proof/crefine/ARM/Finalise_C.thy
@@ -314,7 +314,6 @@ lemma cancel_all_ccorres_helper:
         Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread\<rbrace>
          (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (Ptr &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']) :: tcb_C ptr ptr))
        OD)"
-find_theorems ccorres_underlying name: cross
   unfolding whileAnno_def
 proof (induct ts)
   case Nil

diff --git a/proof/crefine/ARM_HYP/Finalise_C.thy b/proof/crefine/ARM_HYP/Finalise_C.thy
@@ -314,7 +314,6 @@ lemma cancel_all_ccorres_helper:
         Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread\<rbrace>
          (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (Ptr &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']) :: tcb_C ptr ptr))
        OD)"
-find_theorems ccorres_underlying name: cross
   unfolding whileAnno_def
 proof (induct ts)
   case Nil

diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy
@@ -333,7 +333,6 @@ lemma cancel_all_ccorres_helper:
         Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread\<rbrace>
          (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (Ptr &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']) :: tcb_C ptr ptr))
        OD)"
-find_theorems ccorres_underlying name: cross
   unfolding whileAnno_def
 proof (induct ts)
   case Nil

diff --git a/proof/crefine/X64/Finalise_C.thy b/proof/crefine/X64/Finalise_C.thy
@@ -315,7 +315,6 @@ lemma cancel_all_ccorres_helper:
         Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread\<rbrace>
          (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (Ptr &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']) :: tcb_C ptr ptr))
        OD)"
-find_theorems ccorres_underlying name: cross
   unfolding whileAnno_def
 proof (induct ts)
   case Nil