From 4fd7d22b0efb69bc13c43dae4e4c1bd6d392f37d Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Wed, 29 Jun 2022 01:28:53 +0200
Subject: (broken) update hott for Isabelle 2021-1

this just replaces all instance of `this` with instances of `infer`.
Unfortunately, it looks likes something else also broke, and I have
no idea what it is (but the proof for equiv_if_equal fails).

Sadly this means we can't get to univalence for now …
(but rn I'm too tired to try anything else with it)
---
 hott/Nat.thy | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'hott/Nat.thy')

diff --git a/hott/Nat.thy b/hott/Nat.thy
index 33a5d0a..0a38f99 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -115,7 +115,7 @@ Lemma (def) add_comm:
       proof compute
         have "suc (m + n) = suc (n + m)" by (eq ih) refl
         also have ".. = suc n + m" by (rewr eq: suc_add) refl
-        finally show "?" by this
+        finally show "?" by infer
       qed
   done
 
@@ -152,7 +152,7 @@ Lemma (def) zero_mul:
     proof compute
       have "0 + 0 * n = 0 + 0 " by (eq ih) refl
       also have ".. = 0" by compute refl
-      finally show "?" by this
+      finally show "?" by infer
     qed
   done
 
@@ -165,7 +165,7 @@ Lemma (def) suc_mul:
     proof (compute, rewr eq: \<open>ih:_\<close>)
       have "suc m + (m * n + n) = suc (m + ?)" by (rule suc_add)
       also have ".. = suc (m + m * n + n)" by (rewr eq: add_assoc) refl
-      finally show "?" by this
+      finally show "?" by infer
     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 (rewr eq: add_comm) refl
       also have ".. = l * m + (l + l * n)" by (rewr eq: add_assoc) refl
-      finally show "?" by this
+      finally show "?" by infer
     qed
   done
 
@@ -193,7 +193,7 @@ Lemma (def) mul_assoc:
     proof compute
       have "l * (m + m * n) = l * m + l * (m * n)" by (rule mul_dist_add)
       also have ".. = l * m + l * m * n" by (rewr eq: \<open>ih:_\<close>) refl
-      finally show "?" by this
+      finally show "?" by infer
     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 (rewr eq: \<open>ih:_\<close>, rewr eq: add_comm) refl
-      finally show "?" by this
+      finally show "?" by infer
     qed
   done
 
-- 
cgit v1.2.3