From f46df86db9308dde29e0e5f97f54546ea1dc34bf Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 18 Jan 2021 23:49:13 +0000
Subject: Swapped notation for metas (now ?) and holes (now {}), other notation
 and name changes.

---
 hott/Nat.thy | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'hott/Nat.thy')

diff --git a/hott/Nat.thy b/hott/Nat.thy
index f45387c..1aa7932 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -115,7 +115,7 @@ Lemma (def) add_comm:
       proof reduce
         have "suc (m + n) = suc (n + m)" by (eq ih) refl
         also have ".. = suc n + m" by (transport eq: suc_add) refl
-        finally show "{}" by this
+        finally show "?" by this
       qed
   done
 
@@ -152,7 +152,7 @@ Lemma (def) zero_mul:
     proof reduce
       have "0 + 0 * n = 0 + 0 " by (eq ih) refl
       also have ".. = 0" by reduce refl
-      finally show "{}" by this
+      finally show "?" by this
     qed
   done
 
@@ -163,9 +163,9 @@ Lemma (def) suc_mul:
   \<^item> by reduce refl
   \<^item> vars n ih
     proof (reduce, transport eq: \<open>ih:_\<close>)
-      have "suc m + (m * n + n) = suc (m + {})" by (rule suc_add)
+      have "suc m + (m * n + n) = suc (m + ?)" by (rule suc_add)
       also have ".. = suc (m + m * n + n)" by (transport eq: add_assoc) refl
-      finally show "{}" by this
+      finally show "?" by this
     qed
   done
 
@@ -180,7 +180,7 @@ Lemma (def) mul_dist_add:
       also have ".. = l + l * m + l * n" by (rule add_assoc)
       also have ".. = l * m + l + l * n" by (transport eq: add_comm) refl
       also have ".. = l * m + (l + l * n)" by (transport eq: add_assoc) refl
-      finally show "{}" by this
+      finally show "?" by this
     qed
   done
 
@@ -193,7 +193,7 @@ Lemma (def) mul_assoc:
     proof reduce
       have "l * (m + m * n) = l * m + l * (m * n)" by (rule mul_dist_add)
       also have ".. = l * m + l * m * n" by (transport eq: \<open>ih:_\<close>) refl
-      finally show "{}" by this
+      finally show "?" by this
     qed
   done
 
@@ -207,7 +207,7 @@ Lemma (def) mul_comm:
       have "suc n * m = n * m + m" by (rule suc_mul)
       also have ".. = m + m * n"
         by (transport eq: \<open>ih:_\<close>, transport eq: add_comm) refl
-      finally show "{}" by this
+      finally show "?" by this
     qed
   done
 
-- 
cgit v1.2.3