diff options
Diffstat (limited to '')
| -rw-r--r-- | HoTT_Theorems.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index a3a1f63..79614d3 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -203,4 +203,4 @@ 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 +end |