From 57d183c7955fb54b3eb6dd431f5aec338131266b Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 22 Feb 2019 23:45:50 +0100
Subject: Cleanups and reorganization

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

(limited to 'HoTT_Methods.thy')

diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 099a73e..c9744e9 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -51,7 +51,7 @@ method cumulativity declares form = (
 
 section \<open>Deriving typing judgments\<close>
 
-method routine uses add = (rule add | assumption | rule)+
+method routine uses add = (assumption | rule add | rule)+
 
 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}.
@@ -65,7 +65,8 @@ The method @{theory_text derive} combines @{method routine} and @{method compute
 It also handles universes using @{method hierarchy} and @{method cumulativity}.
 \<close>
 
-method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
+method derive uses lems =
+  (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
 
 
 section \<open>Additional method combinators\<close>
-- 
cgit v1.2.3