diff --git a/examples/compute/examples/increment/ex_incrementScript.sml b/examples/compute/examples/increment/ex_incrementScript.sml index 2cdeb23d5..e5290afe3 100644 --- a/examples/compute/examples/increment/ex_incrementScript.sml +++ b/examples/compute/examples/increment/ex_incrementScript.sml @@ -5,7 +5,7 @@ open HolKernel Parse boolLib bossLib; open birTheory; open bir_computeTheory; - +open bir_metaTheory; val _ = new_theory "ex_increment";