move theorems away from Ott file

kth-step · Oct 14, 2024 · cd2e242 · cd2e242
1 parent e97e561
commit cd2e242
Show file tree

Hide file tree

Showing 11 changed files with 711 additions and 1,380 deletions.
diff --git a/examples/compute/ott/bir.ott b/examples/compute/ott/bir.ott
diff --git a/examples/compute/src/shared/cv/bir_cv_binexpScript.sml b/examples/compute/src/shared/cv/bir_cv_binexpScript.sml
@@ -3,7 +3,7 @@
 (* ------------------------------------------------------------------------- *)
 
 open HolKernel Parse bossLib boolLib;
-open birTheory bir_cv_basicTheory;
+open birTheory bir_computeTheory bir_cv_basicTheory;
 open wordsTheory;
 
 

diff --git a/examples/compute/src/shared/cv/bir_cv_binpredScript.sml b/examples/compute/src/shared/cv/bir_cv_binpredScript.sml
@@ -4,7 +4,7 @@
 
 open HolKernel Parse boolLib bossLib;
 open bir_cv_basicTheory;
-open birTheory;
+open birTheory bir_computeTheory;
 
 
 val _ = new_theory "bir_cv_binpred";

diff --git a/examples/compute/src/shared/cv/bir_cv_envScript.sml b/examples/compute/src/shared/cv/bir_cv_envScript.sml
@@ -3,7 +3,7 @@
 (* ------------------------------------------------------------------------- *)
 
 open HolKernel Parse bossLib boolLib;
-open birTheory bir_cv_basicTheory;
+open birTheory bir_metaTheory bir_cv_basicTheory;
 open alistTheory;
 
 val _ = new_theory "bir_cv_env";

diff --git a/examples/compute/src/shared/cv/bir_cv_ifthenelseScript.sml b/examples/compute/src/shared/cv/bir_cv_ifthenelseScript.sml
@@ -3,7 +3,7 @@
 (* ------------------------------------------------------------------------- *)
 
 open HolKernel Parse bossLib boolLib;
-open birTheory bir_cv_basicTheory;
+open birTheory bir_computeTheory bir_cv_basicTheory;
 
 
 val _ = new_theory "bir_cv_ifthenelse";

diff --git a/examples/compute/src/shared/cv/bir_cv_memScript.sml b/examples/compute/src/shared/cv/bir_cv_memScript.sml
@@ -3,7 +3,7 @@
 (* ------------------------------------------------------------------------- *)
 
 open HolKernel Parse boolLib bossLib;
-open birTheory bir_cv_basicTheory;
+open birTheory bir_computeTheory bir_cv_basicTheory;
 open bitstringTheory numeral_bitTheory numposrepTheory;
 
 

diff --git a/examples/compute/src/shared/cv/bir_cv_unaryexpScript.sml b/examples/compute/src/shared/cv/bir_cv_unaryexpScript.sml
@@ -4,7 +4,7 @@
 
 open HolKernel Parse bossLib boolLib;
 open bir_cv_basicTheory;
-open birTheory;
+open birTheory bir_computeTheory;
 open wordsTheory;