From dc2730916482bd230f9bd5244b8b2cc9d005f69a Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 7 Aug 2018 12:30:59 +0200
Subject: Old application syntax incompatible with Eisbach

---
 Nat.thy | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

(limited to 'Nat.thy')

diff --git a/Nat.thy b/Nat.thy
index 93b7a2e..bd2c4ca 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -14,33 +14,33 @@ axiomatization
   Nat :: Term   ("\<nat>") and
   zero :: Term  ("0") and
   succ :: "Term \<Rightarrow> Term" and
-  indNat :: "[Typefam, [Term, Term] \<Rightarrow> Term, Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<nat>)")
+  indNat :: "[[Term, Term] \<Rightarrow> Term, Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<nat>)")
 where
-  Nat_form: "\<nat> : U(O)"
+  Nat_form: "\<nat>: U(O)"
 and
-  Nat_intro1: "0 : \<nat>"
+  Nat_intro1: "0: \<nat>"
 and
-  Nat_intro2: "\<And>n. n : \<nat> \<Longrightarrow> succ n : \<nat>"
+  Nat_intro2: "\<And>n. n: \<nat> \<Longrightarrow> succ(n): \<nat>"
 and
   Nat_elim: "\<And>i C f a n. \<lbrakk>
     C: \<nat> \<longrightarrow> U(i);
-    \<And>n c. \<lbrakk>n : \<nat>; c : C n\<rbrakk> \<Longrightarrow> f n c : C (succ n);
-    a : C 0;
-    n : \<nat>
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> C f a n : C n"
+    \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n);
+    a: C(0);
+    n: \<nat>
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(n): C(n)"
 and
   Nat_comp1: "\<And>i C f a. \<lbrakk>
     C: \<nat> \<longrightarrow> U(i);
-    \<And>n c. \<lbrakk>n : \<nat>; c : C n\<rbrakk> \<Longrightarrow> f n c : C (succ n);
-    a : C 0
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> C f a 0 \<equiv> a"
+    \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n);
+    a: C(0)
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(0) \<equiv> a"
 and
   Nat_comp2: "\<And> i C f a n. \<lbrakk>
     C: \<nat> \<longrightarrow> U(i);
-    \<And>n c. \<lbrakk>n : \<nat>; c : C n\<rbrakk> \<Longrightarrow> f n c : C (succ n);
-    a : C 0;
-    n : \<nat>
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> C f a (succ n) \<equiv> f n (ind\<^sub>\<nat> C f a n)"
+    \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n);
+    a: C(0);
+    n: \<nat>
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(succ n) \<equiv> f(n)(ind\<^sub>\<nat> f a n)"
 
 lemmas Nat_rules [intro] = Nat_form Nat_intro1 Nat_intro2 Nat_elim Nat_comp1 Nat_comp2
 lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2
-- 
cgit v1.2.3