From da03bc717dc2221701868b4ff367f22f2799d722 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Sat, 7 Oct 2023 18:08:27 +0200 Subject: [PATCH] Fix a broken proof (in an unused file) --- .../backend/languages/properties/env_cexp_lemmasScript.sml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/compiler/backend/languages/properties/env_cexp_lemmasScript.sml b/compiler/backend/languages/properties/env_cexp_lemmasScript.sml index 853edf92..9b2c90a8 100644 --- a/compiler/backend/languages/properties/env_cexp_lemmasScript.sml +++ b/compiler/backend/languages/properties/env_cexp_lemmasScript.sml @@ -7,6 +7,8 @@ open pure_miscTheory env_cexpTheory ; val _ = new_theory "env_cexp_lemmas"; val freevars_def = envLangTheory.freevars_def; +val Lams_def = envLangTheory.Lams_def; +val Apps_def = envLangTheory.Apps_def; Theorem freevars_Lams[simp]: ∀vs e. freevars (Lams vs e) = freevars e DIFF set vs @@ -106,4 +108,3 @@ QED *) val _ = export_theory(); -