From f12983b1b53c71fc416155ac4b7e2b11ed8ca9ef Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 27 May 2020 22:16:42 +0200
Subject: change variable name in elim rules and fix small mistake

---
 spartan/data/Maybe.thy | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'spartan/data/Maybe.thy')

diff --git a/spartan/data/Maybe.thy b/spartan/data/Maybe.thy
index dc3ad04..98f5283 100644
--- a/spartan/data/Maybe.thy
+++ b/spartan/data/Maybe.thy
@@ -1,8 +1,12 @@
+chapter \<open>Maybe type\<close>
+
 theory Maybe
 imports More_Types
 
 begin
 
+text \<open>Defined as a sum.\<close>
+
 definition "Maybe A \<equiv> A \<or> \<top>"
 definition "none A \<equiv> inr A \<top> tt"
 definition "some A a \<equiv> inl A \<top> a"
-- 
cgit v1.2.3