From 8319fcba7a1df11e332d30d4e27e3e4ee55a1a5c Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Mon, 14 Oct 2024 21:55:25 +0200 Subject: [PATCH] fix increment example --- examples/compute/examples/increment/ex_incrementScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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";