From d172f9d35a9a1680ec15e4c61e5becbbc92d2ce7 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 14 Aug 2020 11:21:59 +0200
Subject: reorganize

---
 spartan/core/Spartan.thy | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'spartan/core/Spartan.thy')

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 412881b..411eedd 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -184,6 +184,7 @@ axiomatization where
 section \<open>Infrastructure\<close>
 
 ML_file \<open>lib.ML\<close>
+ML_file \<open>context_facts.ML\<close>
 ML_file \<open>context_tactical.ML\<close>
 
 subsection \<open>Type-checking/inference\<close>
@@ -202,6 +203,7 @@ lemmas
   [comp] = beta Sig_comp and
   [cong] = Pi_cong lam_cong Sig_cong
 
+\<comment> \<open>Type-checking\<close>
 ML_file \<open>types.ML\<close>
 
 method_setup typechk =
@@ -214,7 +216,6 @@ method_setup known =
 
 subsection \<open>Statement commands\<close>
 
-ML_file \<open>context_facts.ML\<close>
 ML_file \<open>focus.ML\<close>
 ML_file \<open>elaboration.ML\<close>
 ML_file \<open>elaborated_statement.ML\<close>
-- 
cgit v1.2.3