From e6473c383b479610cee4c0119e5811a12a938cf9 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 14 Aug 2018 17:43:03 +0200
Subject: Well-formation rules are back in the methods; new theory synthesizing
 the natural number predecessor function.

---
 Equal.thy | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'Equal.thy')

diff --git a/Equal.thy b/Equal.thy
index 93f623f..9fc478a 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -46,17 +46,21 @@ and
     a: A
     \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(refl(a)) \<equiv> f(a)"
 
+
 text "Admissible inference rules for equality type formation:"
-(*
+
 axiomatization where
   Equal_form_cond1: "a =\<^sub>A b: U(i) \<Longrightarrow> A: U(i)"
 and
   Equal_form_cond2: "a =\<^sub>A b: U(i) \<Longrightarrow> a: A"
 and
   Equal_form_cond3: "a =\<^sub>A b: U(i) \<Longrightarrow> b: A"
-*)
+
+
+text "Rule declarations:"
+
 lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp
-(*lemmas Equal_wellform [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3*)
+lemmas Equal_wellform [wellform] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3
 lemmas Equal_comps [comp] = Equal_comp
 
 
-- 
cgit v1.2.3

