Theories fully reorganized. Well-formedness rules removed. New methods etc.

1 files changed, 5 insertions, 5 deletions

diff --git a/Equal.thy b/Equal.thy
index f9bc223..7a31e37 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -7,7 +7,7 @@ Equality type
 *)
 
 theory Equal
-imports HoTT_Base HoTT_Methods
+imports HoTT_Base
 
 begin
 
@@ -36,13 +36,13 @@ axiomatization where
     p: x =\<^sub>A y;
     x: A;
     y: A;
-    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i;
-    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and
+    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
+    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and
 
   Equal_comp: "\<lbrakk>
     a: A;
-    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i;
-    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a"
+    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
+    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a"
 
 lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim
 lemmas Equal_comp [comp]