From e1be5f97bb2a42b3179bc24b118d69af137f8e5d Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 21:28:21 +0200
Subject: Regrouping type rules

---
 tests/Test.thy | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'tests/Test.thy')

diff --git a/tests/Test.thy b/tests/Test.thy
index 433039c..c0dc0dd 100644
--- a/tests/Test.thy
+++ b/tests/Test.thy
@@ -6,8 +6,8 @@ This is an old "test suite" from early implementations of the theory.
 It is not always guaranteed to be up to date, or reflect most recent versions of the theory.
 *)
 
-theory HoTT_Test
-  imports HoTT
+theory Test
+  imports "../HoTT"
 begin
 
 
@@ -31,14 +31,14 @@ text "
   Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following.
 "
 
-proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" using assms ..
+proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" by (simple lems: assms)
 
 proposition
   assumes "A : U(i)" and "A \<equiv> B"
   shows "\<^bold>\<lambda>x. x : B \<rightarrow> A"
 proof -
-  have "A\<rightarrow>A \<equiv> B\<rightarrow>A" using assms by simp
-  moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" using assms(1) ..
+  have "A \<rightarrow> A \<equiv> B \<rightarrow> A" using assms by simp
+  moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" by (simple lems: assms)
   ultimately show "\<^bold>\<lambda>x. x : B \<rightarrow> A" by simp
 qed
 
@@ -102,7 +102,7 @@ lemma curried_type_judgment:
 
 
 text "
-  Polymorphic identity function. Trivial due to lambda expression polymorphism.
+  Polymorphic identity function is now trivial due to lambda expression polymorphism.
   (Was more involved in previous monomorphic incarnations.)
 "
 
-- 
cgit v1.2.3