From d09095bec2c136f600edd0039a1cc1eae441d823 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 5 Jun 2018 18:42:54 +0200
Subject: Code formatting

---
 HoTT_Theorems.thy | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'HoTT_Theorems.thy')

diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy
index 1ac4484..52e1b32 100644
--- a/HoTT_Theorems.thy
+++ b/HoTT_Theorems.thy
@@ -141,6 +141,7 @@ consts Ui::Term
 definition Id where "Id \<equiv> \<^bold>\<lambda>A:Ui. \<^bold>\<lambda>x:A. x"
 (* Have to think about universes... *)
 
+(*
 section \<open>Nats\<close>
 
 text "Here's a dumb proof that 2 is a natural number."
@@ -156,5 +157,6 @@ text "We can of course iterate the above for as many applications of \<open>succ
 The next thing to do is to implement induction to automate such proofs.
 
 When we get more stuff working, I'd like to aim for formalizing the encode-decode method to be able to prove the only naturals are 0 and those obtained from it by \<open>succ\<close>."
+*)
 
 end
\ No newline at end of file
-- 
cgit v1.2.3