From a5692e0ba36b372b9175d7b356f4b2fd1ee3d663 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 11 Feb 2019 15:37:18 +0100
Subject: Put typing functionality into a .thy and clean up antiquotations,
 which results in some reorganization of the theory import structure.

---
 HoTT_Methods.thy | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'HoTT_Methods.thy')

diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 99f3446..088c1fa 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -9,6 +9,7 @@ imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools"
 
 begin
 
+
 section \<open>Substitution and simplification\<close>
 
 ML_file "~~/src/Tools/misc_legacy.ML"
@@ -25,6 +26,7 @@ Premises of the rule(s) applied are added as new subgoals.
 
 method compute declares comp = (subst comp)
 
+
 section \<open>Handling universes\<close>
 
 text \<open>
@@ -46,6 +48,7 @@ method cumulativity declares form = (
   ((elim U_cumulative | (rule U_cumulative, rule form)), provelt)
 )
 
+
 section \<open>Deriving typing judgments\<close>
 
 method routine uses add = (assumption | rule add | rule)+
@@ -54,6 +57,7 @@ text \<open>
 The method @{method routine} proves typing judgments @{prop "a: A"} using the rules declared @{attribute intro} in the respective theory files, as well as any additional lemmas provided with the modifier @{theory_text add}.
 \<close>
 
+
 section \<open>Derivation search\<close>
 
 text \<open>
@@ -63,6 +67,7 @@ It also handles universes using @{method hierarchy} and @{method cumulativity}.
 
 method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
 
+
 section \<open>Induction\<close>
 
 text \<open>
-- 
cgit v1.2.3