From 23e8afe152a84551491594aea133488523525410 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Mon, 21 Mar 2022 16:50:55 +0000
Subject: Add all-in-one import for Hoare logic semantics.

---
 Everything.agda | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'Everything.agda')

diff --git a/Everything.agda b/Everything.agda
index 1bebcbe..8245737 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -84,6 +84,9 @@ import Helium.Instructions.Core
 -- Implementation of Barrett reduction.
 import Helium.Instructions.Instances.Barrett
 
+-- Semantics for the Armv8-M pseudocode using Hoare triples.
+import Helium.Semantics.Axiomatic
+
 -- Definition of assertions used in correctness triples
 import Helium.Semantics.Axiomatic.Assertion
 
-- 
cgit v1.2.3