From 9b17aac85aa650a7a9d6463d3d01f1eb228d4572 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 11 Sep 2018 08:59:16 +0200
Subject: Go back to higher-order application notation

---
 Nat.thy | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

(limited to 'Nat.thy')

diff --git a/Nat.thy b/Nat.thy
index 45c3a2e..e879c92 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -17,31 +17,31 @@ axiomatization
   succ :: "Term \<Rightarrow> Term" and
   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_intro_0: "0: \<nat>"
 and
-  Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ(n): \<nat>"
+  Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>"
 and
   Nat_elim: "\<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);
+    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>(f)(a)(n): C(n)"
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a n: C n"
 and
   Nat_comp_0: "\<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>(f)(a)(0) \<equiv> a"
+    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> f a 0 \<equiv> a"
 and
   Nat_comp_succ: "\<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);
+    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>(f)(a)(succ n) \<equiv> f(n)(ind\<^sub>\<nat> f a n)"
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
 
 
 text "Rule attribute declarations:"
-- 
cgit v1.2.3